Skip to content

Commit

Permalink
Some edits
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Nov 17, 2023
1 parent ff97fcd commit f08849f
Show file tree
Hide file tree
Showing 3 changed files with 5 additions and 5 deletions.
4 changes: 2 additions & 2 deletions iii/cat/05_monads.tex
Original file line number Diff line number Diff line change
Expand Up @@ -387,7 +387,7 @@ \subsection{Comparison functors}
\end{remark}

\subsection{Monadic adjunctions}
It can be useful to know, for an arbitrary adjunction, if when the Eilenberg--Moore comparison functor \( K : \mathcal D \to \mathcal C^{\mathbb T} \) is part of an equivalence of categories.
It can be useful to know, for an arbitrary adjunction, if the Eilenberg--Moore comparison functor \( K : \mathcal D \to \mathcal C^{\mathbb T} \) is part of an equivalence of categories.
Note that the Kleisli comparison functor \( H \) is always full and faithful, so is part of an equivalence if and only if it is essentially surjective, and since its action on objects is \( F \), this holds if and only if \( F \) is essentially surjective.
\begin{definition}
An adjunction \( F \dashv G \) is \emph{monadic}, or the right adjoint \( G \) is \emph{monadic}, if \( K \) is part of an equivalence.
Expand Down Expand Up @@ -424,7 +424,7 @@ \subsection{Monadic adjunctions}
\end{tikzcd}\]
For any object \( B \) of \( \mathcal D \), morphisms \( L(A, \alpha) \to B \) correspond to morphisms \( f : FA \to B \) satisfying \( f(F\alpha) = f \epsilon_{FA} \).
If \( \overline f : A \to GB \) is the transpose of \( f \) across \( F \dashv G \), then by naturality, the transpose of \( f(F\alpha) \) is \( \overline f \alpha \), and the transpose of \( f \epsilon_{FA} \) is \( Gf \) since \( \epsilon_{FA} \) transposes to \( 1_{GFA} \).
But we have \( f = \epsilon_B (F\overline f) \), so \( GF = (G \epsilon_B)(GF \overline f) = (G\epsilon_B)(T\overline f) \).
But we have \( f = \epsilon_B (F\overline f) \), so \( (G \epsilon_B)(GF \overline f) = (G\epsilon_B)(T\overline f) \).
Thus \( f(F\alpha) = f(\epsilon_{FA}) \) if and only if \( \overline f \alpha = (G\epsilon_B)(T \overline f) \), which is to say that \( \overline f \) is an algebra homomorphism \( (A, \alpha) \to (GB, G\epsilon_B) = KB \).
Naturality of this bijection follows from the fact that the map \( f \mapsto \overline f \) is natural, so \( L \dashv K \) as required.
\end{proof}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ \subsection{Nakayama's lemma}
This can be applied to find generating sets for \( M \).
\begin{proof}
Note that
\[ \mathfrak a \qty(\faktor{M}{N}) = \faktor{\mathfrak a M + N}{N} = \faktor{M}{N} \]
\[ \mathfrak a \qty(\faktor{M}{N}) = \faktor{(\mathfrak a M + N)}{N} = \faktor{M}{N} \]
so \( \faktor{M}{N} = 0 \) by Nakayama's lemma.
\end{proof}

Expand Down
4 changes: 2 additions & 2 deletions iii/mtncl/02_quantifier_elimination.tex
Original file line number Diff line number Diff line change
Expand Up @@ -389,7 +389,7 @@ \subsection{Characterisations of quantifier elimination}
\emph{(iv) implies (v).}
We proceed by induction on the structure of \( \mathcal L \)-formulae.
We can iteratively convert existential quantifiers to universal quantifiers, noting that (iv) allows us to convert a sequence of existentials to a sequence of universals simultaneously.

\emph{(v) implies (i).}
We use induction on the structure of \( \mathcal L \)-formulae, noting that universal formulae are preserved under extensions, and that every formula and its negation can be represented as a universal formula.
\end{proof}
Expand Down Expand Up @@ -465,7 +465,7 @@ \subsection{Characterisations of quantifier elimination}
We obtain an elementary extension \( \mathcal D \) of \( \mathcal A \).
If \( \abs{\mathcal A} = n < \aleph_0 \), then the theory of \( \mathcal A \) must include a sentence that states this fact.
Thus \( \mathcal D \) models the same sentence, so \( \abs{\mathcal D} = n = \abs{\mathcal A} \).
Thus \( \mathcal A \) and \( \mathcal D \) elementarily equivalent finite structures, so the elementary embedding \( h : \mathcal A \rightarrowtail \mathcal D \) is an isomorphism.
Thus \( \mathcal A \) and \( \mathcal D \) are elementarily equivalent finite structures, so the elementary embedding \( h : \mathcal A \rightarrowtail \mathcal D \) is an isomorphism.
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJcXGxhbmdsZSBcXHZiIGEgXFxyYW5nbGVfe1xcbWF0aGNhbCBBfSJdLFsyLDEsIlxcbGFuZ2xlIFxcdmIgYiBcXHJhbmdsZV97XFxtYXRoY2FsIEF9Il0sWzIsMCwiXFxtYXRoY2FsIEEiXSxbMSwwLCJcXG1hdGhjYWwgRCJdLFswLDAsIlxcbWF0aGNhbCBBIl0sWzAsMSwiXFxzaW0iXSxbMSwyLCIiLDAseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJob29rIiwic2lkZSI6InRvcCJ9fX1dLFszLDIsImheey0xfSJdLFswLDQsIiIsMix7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV0sWzQsMywiZiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Imhvb2siLCJzaWRlIjoidG9wIn19fV1d
\[\begin{tikzcd}
{\mathcal A} & {\mathcal D} & {\mathcal A} \\
Expand Down

0 comments on commit f08849f

Please sign in to comment.