§ Monads from Riehl

§ What is a monad

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

§ Monad from adjunction

§ Algebra for a monad CTC^T.

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

§ Factoring of forgetful functor of adjunction

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

§ Monadic adjunction

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

§ Category of models for an algebraic theory

§ Limits and colimits in categories of algebras

§ 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

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

§ Corollary 5.6.2: Bijective continuous functions in CHaus are isos

§ Corollary 5.6.4: Any bijective 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

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:CCT: C \to C is finitary and CC is complete and cocomplete, then so is CTC^T

  • We have already seen that if CC is complete then so is CTC^T
  • We have also seen that CTC^T contains coproducs
  • So is we show that CTC^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:CDF: C \to D requires that for each dDd \in D, the comma category const(d)Fconst(d) \downarrow F admit weakly initial objects.
  • Unwrapping that definition: For each dDd \in D, there is a solution set. Tht is, there exists a small set IIand a family of objects cIc_I and a family of morphisms fI:dF(ci)f_I: d \to F(c_i) such that any morphism dF(c)d \to F(c) in DD can be factored via some fif_i as dfIF(ci)gF(c)=dF(c)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,α)(B,β)f, g: (A, \alpha) \to (B, \beta).
  • We will produce a solution set with a single element by creating a fork (Q,u)(Q, u) such that any other fork factors through this fork (perhaps non uniquely!) So we create:
(A,α)f,g(B,β)q(Q,u) (A, \alpha) \xrightarrow{f, g} (B, \beta) \xrightarrow{q} (Q, u)
  • If we know how to create coequalizers in CTC^T, then this would be easy: we literally just create a coequalizer.
  • Instead, we create some "approximation" of the coequalizer with (Q,u)(Q, u).
  • To start with, we define q0:BQ0q_0: B \to Q_0 in CC of the pair (Af,gB(A \xrightarrow{f, g} B).
  • If Tq0Tq_0 would be the coequalizer of Tf,TgTf, Tg then we are done. But this is unlikely, since a monad need not preserve coequalizers.
  • Instead, we simply calculate the coequalizer of Tf,TgTf, Tg and call this q1:BQ1=TQ0q_1: B \to Q_1=TQ_0.
  • Repeat inductively to form a directed limit (colimit).
  • Monad preserves filtered colimits, since in UFUF, FF the left adjoint preserves all colimits, and UUthe right adjoint preserves colimits since it simply forgets the data in