A Universe of Sorts

§ Monads from Riehl

I'm having some trouble enmeshing my haskell intuition for monads with the rigor, so this
A category is said to be monadi is an expository note to bridge the gap.

§ What is a monad

A monad is an endofunctor T: C -> C equipped with two natural transformations:
(1) return/eta: idC => T [yeeta, since we are yeeting into the monad. ]
(2) join/mu: T^2 => T, such that two laws are obeyed:

First law: mu, T commutation:

T^3(x) --T(@mu@x)--> T^2@x
|                   |
mu@(T@x)          mu@x
|                   |
v                   v
T^2(x)---mu@x-----> T(x)

Second law: mu, eta cancellation:

(Tx) --eta@(T@x)--> T^2(x)
|EQ                 |
|                   |
T@(eta@x)         mu@x
|                   |
v                 EQv
T^2(x)---mu@x---> T(x)

mu . eta T = mu . T eta = 1

§ Monad from adjunction

Any adjunction between a Free functor F: L -> H and a forgetfUl/Underlying functor U: H -> LF |- U gives a monad. The categories are named L, H for lo, high in terms of the amount of structure they have. We go from low structure to high structure by the free functor.
The monad on L is given by T := UF.
Recall that an adjunction gives us pullback: (F l -> h) -> (l -> U h) and pushfwd: (l -> U h) -> (F l -> h). The first is termed pullback since it takes a function living in the high space and pulls it back to the low space.
This lets us start with (F l -> F l), peel a F from the left via pullbackto create (l -> U (F l)). That is we have return: l -> T l.
In the other direction, we are able to start with (U h -> U h), peel a U from the right via pushforward to create (F U h -> h). This allows us to create the counit as T^2 l = F U F U l = F (U F) U l -> F U l = T l.

§ Algebra for a monad $C^T$ .

Any monad, given by (T: C -> C, return: 1C => T, join: T^2 => T) has a category of T-algebras associated to it.
The objects of T-alg are morphisms f: Tc -> c.
The morphisms of T-alg between f: Tc -> c and g: Td -> d are commuting squares, determined by an arr: c -> d

Tc -T arr-> Td
|           |
f           g
|           |
v           v
c   -arr->  d

The notation for the category as $C^T$ makes some sense, since it consists of objects of the form Tc -> c which matches somewhat with the function notation. We should have written $C^{TC}$ but maybe that's too unweildy.

§ Factoring of forgetful functor of adjunction

Any adjunction (F: L -> H, U: H -> L) with associated monad T allows us to factor U: H -> L as:

H -Stx-> L^T -forget-> L

So we write elements of H in terms of syntax/"algebra over L". We then forget the algebra structure to keep only the low form.
The way to think about this is that any object in the image of U in fact has a (forgotten) algebra structure, which is why we can first go to L^T and then forget the algebraic structure to go back to L. It might be that this transition from H to L^Tis very lossy. This means that the algebra is unable to encode what is happening in H very well.

§ Monadic adjunction

Let us consider an adjunction (F: L -> H, U: H -> L) with monad T. Factor U via L^T as:

H -Stx-> L^T -forget-> L

The adjunction is said to be monadic if in the factoring of U via L^T, it happens that H ~= L^T. That is, Stx is an equivalence between H and L^T.
The way to think about this is that any object in the image of U in fact has a (forgotten) algebra structure, and this algebra structure actually correctly represents everything that was happening in H.
Another way to say the adjunction F: L -> H: U is monadic is to say that is that F is monadic over U. We imagine the higher category H and the free functor F lying over L and U.
Warning : This is a STRONGER condition than saying that UF is a monad. UF is ALWAYS a monad for ANY adjunction. This says that H ~= L^T, via the factoring H -Stx-> L^T -forget-> L.
We sometimes simply say that U is monadic , to imply that there exists an F such that UF is an adjunction and that U ~= L^T.

§ Category of models for an algebraic theory

A functor is finitary if it preserves filtered colimits.
In particular, a monad T : L -> L is finitary if it preserves filtered colimits in C.
If a right adjoint is finitary, then so is its monad because its left adjoint preserves all colimits. Thus, their composite preserves filtered colimits.
A category H is a category of models for an algebraic theory if there is a finitary monadic functor U : H -> Set.

§ Limits and colimits in categories of algebras

We say that H is monadic over L iff the adjunction F: L -> H: U such that the monad T: L -> L := UFgives rise to an equivalence of categories H ~= L^T.

§ Riehl: Limits and colimits in categories of algebras

Here, we learn theorems about limits and colimits in L^T.

§ Lemma 5.6.1: If `U` is monadic over `F`, then `U` reflects isos

That is, if for some f: h -> h', if Uf: Uh -> Uh' is an iso, then so is f.
Since the adjunction F |- U is a monadic adjunction ( U is monadic over F), we know that H ~= L^T, and U equals the forgetful functor (H = L^T) -> L.
Write the arrow f: h -> h' as an arrow in L^T via the commuting square datum determined by g: h -> h':

Tl-Tg->Tl'
|      |
a      a'
|      |
v      v
l--g-->l'

Since we assume that U(Tg) is iso, this means that g is iso. This means that there exists a g'which is the inverse of g. But this means that the diagram below commutes:

Tl<-Tg'-Tl'
|      |
a      a'
|      |
v      v
l<-g'--l'

For a proof, we see that a' . Tg = g . a'. Composing by g' on left, giving: g' . a' . Tg = a'. Composing by Tg' on the right, we get: g'. a' = a' . Tg'. That's the statement of the above square.
This means we have created an inverse Tg', which reflects g' into L^T.

§ Corollary 5.6.2: Bijective continuous functions in CHaus are isos

When we forget to Set, we see that bijections are the isos. Thus, in CHaus (compact haussdorff spaces) which is monadic over Set, we have that the arrows that forget to become isos in set, ie, continuous bijections are also isos.

§ Corollary 5.6.4: Any bĳective homomorphism arising from a monadic adjunction which forgets to `Set` will be iso

Follow the exact same proof.

§ Thm 5.6.5.i A monadic functor `U: H -> L` creates any limits that `L` has.

Since the equivalence H ~= L^T creates all limits/colimits, it suffices to show the result for U^T: L^T -> L.
Consider a diagram D: J -> C^T with image spanned by (T(D[j]) -f[j]-> D[j]).
Consider the forgotten diagram U^TD: J -> C with image spanned by D[j]. Create the limit cone P (for product, since product is limit) with morphisms pi[j]: P -> D[j]. We know this limit exists since we assume that Lhas this limit that U^T needs to create.
We can reinterpret the diagram D: J -> C^T as a natural transformation between two functors Top, Bot: J -> C. These functors are Top(j) := T(D[j]), Bottom(j) := D[j].
The the natural transformation is given by eta: Top => Bottom, with defn eta(j) := D[j]-f[j]-> D[j] where f[j] is given by the image of (T(D[j]) -f[j]-> D[j]).
So we see that eta: Top => Bot can also be written as eta: TD => D since Top ~= TD and Bot ~= D.
Now consider the composition of natural transformations Const(TL) =Tpi=> TD =gamma=> D all in J -> C. This gives us a cone with summit TL.
This cone with summit TL factors through L via the unique morphism lambda: TL -> L. We wish to show that (TL -lambda-> L) is a T-algebra, and is the limit of D.
Diagram chase. Ugh.

§ Corollary 5.6.6: The inclusion of a reflective subcategory creates all limits

The inclusion of a reflective subcategory is monadic.
This lets us create all limits by the above proposition.

§ Corollary 5.6.7: Any category monadic over `Set` is complete

Set has all limits.
The forgetful functor U: H -> L creates all limits that L=Set has.
Thus H has all limits, ie. is complete.

§ Corollary 5.6.9: `Set` is cocomplete

The contravariant power set functor P: Set^op -> Set is monadic.
Set has all limits, and P creates all limits.
Thus all limits of Set^op exist, ie, all colimits of Set exist.

§ Category of models for alg. theory is complete

TODO

§ Category of algebras has coproducts

We show how to construct the free product of monoids via haskell. The same principle generalizes for any algebraic theory:

import Control.Monad(join)

-- |(a*|b*)* ~~simplify~~> (a|b)*
eval :: Monoid a => Monoid b => [Either [a] [b]] -> [Either a b]
eval = map (either (Left . mconcat) (Right . mconcat))

-- | a*|b* -> (a|b)* with no simplification
transpose :: Either [a] [b] -> [Either a b]
transpose = either (map Left) (map Right)

-- | (a*|b*)* -> (a|b)* with no simplification
flatten :: [Either [a] [b]] -> [Either a b]
flatten = join . map transpose


-- force: eval = flatten | via coequallizer

§ If $T: C \to C$ is finitary and $C$ is complete and cocomplete, then so is $C^T$

We have already seen that if $C$ is complete then so is $C^T$
We have also seen that $C^T$ contains coproducs
So is we show that $C^T$ has coequalizers, then we get cocomplete, since any colimit can be expressed as coproduct-coequalizer.
To show that all coequalizers exists is to show that there is an adjoint to the functor const: [C^T] -> [J -> C^T] where J := [a -f,g-> b]is the diagram category for coequalizers.
Recall that the adjoint sends a diagram [J -> C^T] to the nadir that is the coequalizer in C^T.
See that the constant functor trivially preserves limits.
To show that it possesses an adjunction, we apply an adjoint functor theorem (fuck me). In particular, we apply the general adjoint functor theorem, so we must show that the solution set condition is satisfied.
Recall that the solution set condition for $F: C \to D$ requires that for each $d \in D$ , the comma category $const(d) \downarrow F$ admit weakly initial objects.
Unwrapping that definition: For each $d \in D$ , there is a solution set. Tht is, there exists a small set $I$ and a family of objects $c_I$ and a family of morphisms $f_I: d \to F(c_i)$ such that any morphism $d \to F(c)$ in $D$ can be factored via some $f_i$ as $d \xrightarrow{f_I} F(c_i) \xrightarrow{g} F(c) = d \to F(c)$ .
To apply the theorem, we must produce a solution set for every object in [J -> C^T], that is, for each parallel pair of morphisms $f, g: (A, \alpha) \to (B, \beta)$ .
We will produce a solution set with a single element by creating a fork $(Q, u)$ such that any other fork factors through this fork (perhaps non uniquely!) So we create:

(A, \alpha) \xrightarrow{f, g} (B, \beta) \xrightarrow{q} (Q, u)

If we know how to create coequalizers in $C^T$ , then this would be easy: we literally just create a coequalizer.
Instead, we create some "approximation" of the coequalizer with $(Q, u)$ .
To start with, we define $q_0: B \to Q_0$ in $C$ of the pair $(A \xrightarrow{f, g} B$ ).
If $Tq_0$ would be the coequalizer of $Tf, Tg$ then we are done. But this is unlikely, since a monad need not preserve coequalizers.
Instead, we simply calculate the coequalizer of $Tf, Tg$ and call this $q_1: B \to Q_1=TQ_0$ .
Repeat inductively to form a directed limit (colimit).
Monad preserves filtered colimits, since in $UF$ , $F$ the left adjoint preserves all colimits, and $U$ the right adjoint preserves colimits since it simply forgets the data in

§ Monads from Riehl

§ What is a monad

§ Monad from adjunction

§ Algebra for a monad CTC^TCT.

§ Factoring of forgetful functor of adjunction

§ Monadic adjunction

§ Category of models for an algebraic theory

§ Limits and colimits in categories of algebras

§ Riehl: Limits and colimits in categories of algebras

§ Lemma 5.6.1: If U is monadic over F, then U reflects isos

§ Corollary 5.6.2: Bijective continuous functions in CHaus are isos

§ Corollary 5.6.4: Any bĳective homomorphism arising from a monadic adjunction which forgets to Set will be iso

§ Thm 5.6.5.i A monadic functor U: H -> L creates any limits that L has.

§ Corollary 5.6.6: The inclusion of a reflective subcategory creates all limits

§ Corollary 5.6.7: Any category monadic over Set is complete

§ Corollary 5.6.9: Set is cocomplete

§ Category of models for alg. theory is complete

§ Category of algebras has coproducts

§ If T:C→CT: C \to CT:C→C is finitary and CCC is complete and cocomplete, then so is CTC^TCT

§ Algebra for a monad $C^T$ .

§ Lemma 5.6.1: If `U` is monadic over `F`, then `U` reflects isos

§ Corollary 5.6.4: Any bĳective homomorphism arising from a monadic adjunction which forgets to `Set` will be iso

§ Thm 5.6.5.i A monadic functor `U: H -> L` creates any limits that `L` has.

§ Corollary 5.6.7: Any category monadic over `Set` is complete

§ Corollary 5.6.9: `Set` is cocomplete

§ If $T: C \to C$ is finitary and $C$ is complete and cocomplete, then so is $C^T$