Skip to content

Commit

Permalink
Minor fixes
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Apr 25, 2024
1 parent 85d9968 commit 05a5a80
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 6 deletions.
14 changes: 12 additions & 2 deletions iii/cat/05_monads.tex
Original file line number Diff line number Diff line change
Expand Up @@ -271,11 +271,21 @@ \subsection{Comparison functors}
\begin{definition}
Let \( \mathbb T = (T, \eta, \mu) \) be a monad on \( \mathcal C \).
Then \( \operatorname{Adj}(\mathbb T) \) is the category of adjunctions \( F \dashv G \) which induce \( \mathbb T \), where the morphisms \( F \dashv G \) to \( F' \dashv G' \) are the functors \( K : \mathcal D \to \mathcal D' \) satisfying \( KF = F' \) and \( G' K = G \).
% https://q.uiver.app/#q=WzAsNCxbMSwwLCJcXG1hdGhjYWwgQyJdLFswLDEsIlxcbWF0aGNhbCBEIl0sWzIsMSwiXFxtYXRoY2FsIEQnIl0sWzEsMiwiXFxtYXRoY2FsIEMiXSxbMCwxLCJGIiwyXSxbMSwyLCJLIl0sWzAsMiwiRiciXSxbMiwzLCJHJyJdLFsxLDMsIkciLDJdXQ==
\[\begin{tikzcd}
& {\mathcal C} \\
{\mathcal D} && {\mathcal D'} \\
& {\mathcal C}
\arrow["F"', from=1-2, to=2-1]
\arrow["{F'}", from=1-2, to=2-3]
\arrow["K", from=2-1, to=2-3]
\arrow["G"', from=2-1, to=3-2]
\arrow["{G'}", from=2-3, to=3-2]
\end{tikzcd}\]
\end{definition}
\begin{theorem}
The Kleisli adjunction \( F_{\mathbb T} \dashv G_{\mathbb T} \) is initial in \( \operatorname{Adj}(\mathbb T) \), and the Eilenberg--Moore adjunction \( F^{\mathbb T} \dashv G^{\mathbb T} \) is terminal in \( \operatorname{Adj}(\mathbb T) \).
\end{theorem}
% TODO: Define the comparison functors
\begin{proof}
We will first do the case of the Eilenberg--Moore adjunction.
Let \( F \dashv G \) be an adjunction inducing \( \mathbb T \).
Expand Down Expand Up @@ -459,7 +469,7 @@ \subsection{Monadic adjunctions}
\arrow["s", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
such that \( hf = hg, hs = 1_C, gt = 1_B, ft = sh \).
That is, \( h \) equalises \( f \) and \( g \), and the following diagrams commute.
That is, \( h \) has equal composites with \( f \) and \( g \), and the following diagrams commute.
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIkMiXSxbMSwxLCJDIl0sWzAsMSwiQiJdLFswLDEsImciXSxbMSwyLCJoIl0sWzMsMSwicyIsMl0sWzMsMiwiMV9DIiwyXSxbNCwwLCJ0Il0sWzQsMSwiMV9CIiwyXV0=
\[\begin{tikzcd}
A & B & C \\
Expand Down
10 changes: 6 additions & 4 deletions iii/cat/06_monoidal_and_enriched_categories.tex
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,9 @@ \subsection{Monoidal categories}
\item In \( \mathbf{Met} \), the different metrics on \( X \times Y \) yield different monoidal structures on \( \mathbf{Met} \).
Each of these have the one-point space, which is the terminal object, as the unit of the monoid.
\item In \( \mathbf{AbGp} \), the tensor product gives a monoidal structure, where \( \mathbb Z \) is the unit.
Recall that if \( A, B, C \) are abelian groups, then morphisms \( A \otimes B \to C \) (that is, \( \mathbb Z \)-linear maps) correspond to \( \mathbb Z \)-bilinear maps \( A \times B \to C \).
Similarly, if \( R \) is a commutative ring, the tensor product \( \otimes_R \) gives a monoidal structure on \( \mathbf{Mod}_R \) with unit \( R \).
The \( R \)-linear maps \( A \otimes B \to C \) correspond to \( R \)-bilinear maps \( A \times B \to C \).
\item For any category \( \mathcal C \), its category of endofunctors \( [\mathcal C, \mathcal C] \) has a monoidal structure given by composition.
The unit is the identity endofunctor \( 1_{\mathcal C} \).
\item For posets with top and bottom elements \( 1 \) and \( 0 \), we can define the \emph{ordinal sum} \( A \ast B \) to be the poset obtained from their disjoint union, by identifying the top element of \( A \) with the bottom element of \( B \).
Expand Down Expand Up @@ -82,13 +84,13 @@ \subsection{The coherence theorem}
\item \( i(w) \) is the number of occurrences of \( I \) in \( w \).
\end{enumerate}
Applying any instance of \( \alpha, \lambda, \rho \) to a word reduces its height.
For example, \( \alpha \dots : w \to w' \), then \( a(w') < a(w) \) and \( i(w') = i(w) \), and correspondingly if \( \lambda\dots w \to w' \), then \( i(w') = i(w) - 1 \) and \( a(w') \leq a(w) \).
For example, if \( \alpha \ldots : w \to w' \), then \( a(w') < a(w) \) and \( i(w') = i(w) \), and correspondingly if \( \lambda\dots w \to w' \), then \( i(w') = i(w) - 1 \) and \( a(w') \leq a(w) \).
In particular, any string of instances of \( \alpha, \lambda, \rho \) starting from \( w \) has length at most \( a(w) + i(w) \).

We say that a word \( w \) is \emph{reduced} if either \( a(w) = i(w) = 0 \) or \( w = I \).
If \( a(w) > 0 \), then \( w \) is the domain of an instance of \( \alpha \), and if \( i(w) > 0 \) and \( w \neq I \), then \( w \) is the domain of an instance of either \( \lambda \) or \( \rho \).
Thus, for any word \( w \), there is a string \( w \to \dots \to w_0 \) where \( w_0 \) is the unique reduced word containing the same variables of \( w \) in the same order.
We must show that any two such strings have the same composite
Thus, for any word \( w \), there is a string \( w \to \cdots \to w_0 \) where \( w_0 \) is the unique reduced word containing the same variables of \( w \) in the same order.
We must show that any two such strings have the same composite.
Given
% https://q.uiver.app/#q=WzAsMyxbMSwwLCJ3Il0sWzAsMSwidyciXSxbMiwxLCJ3JyciXSxbMCwxLCJcXHZhcnBoaSIsMl0sWzAsMiwiXFxwc2kiXV0=
\[\begin{tikzcd}
Expand Down Expand Up @@ -298,7 +300,7 @@ \subsection{Closed monoidal categories}
\subsection{Enriched categories}
\begin{definition}
Let \( (\mathcal E, \otimes, I) \) be a monoidal category.
An \emph{\( \mathcal E \)-enriched category} is
An \emph{\( \mathcal E \)-enriched category} consists of
\begin{enumerate}
\item a collection \( \ob \mathcal C \) of objects;
\item an object \( \mathcal C(A, B) \) of \( \mathcal E \) for each pair of objects \( A, B \in \ob \mathcal C \);
Expand Down

0 comments on commit 05a5a80

Please sign in to comment.