module Cat.Diagram.Monad.Limits {o β} {C : Precategory o β} {M : Monad C} where

private module EM = Cat.Reasoning (Eilenberg-Moore M) module C = Cat.Reasoning C module M = Monad M open Algebra-on open Total-hom

# Limits in categories of algebrasπ

Suppose that $C$ be a category, $M$ be a monad on $C,$ and $F$ be a $J-shaped$ diagram of $M-algebras$ (that is, a functor $F:JβC_{M}$ into the Eilenberg-Moore category of M). Suppose that an evil wizard has given you a limit for the diagram in $C$ which underlies $F,$ but they have not (being evil and all) told you whether $limF$ admits an algebra structure at all.

Perhaps we can make this situation slightly more concrete, by working
in a category *equivalent to* an Eilenberg-Moore category: If we
have two groups
$G,$
$H,$
considered as a discrete diagram, then the limit our evil wizard would
give us is the product
$U(G)ΓU(H)$
in
$Sets.$
But we already
know we can equip this product with a βpointwiseβ group structure!
Does this result generalise?

The answer is positive, though this is one of those cases where
abstract nonsense can not help us: gotta roll up our sleeves and
calculate away. Suppose we have a diagram as in the setup β weβll show
that the functor
$U:C_{M}βC$
both preserves and *reflects* limits, in that
$K$
is a limiting cone if, and only if,
$U(K)$
is.

module _ {jo jβ} {J : Precategory jo jβ} (F : Functor J (Eilenberg-Moore M)) where private module J = Precategory J module F = Functor F module FAlg j = Algebra-on (F.β j .snd) open Functor open _=>_

That $U$ preserves limits follows immediately from the fact that it is a right adjoint: the non-trivial part is showing that it reflects them.

Forget-EM-preserves-limits : preserves-limit Forget-EM F Forget-EM-preserves-limits = right-adjoint-is-continuous Free-EMβ£Forget-EM

We begin with the following key lemma: Write $K:C$ for the limit of a diagram $JFβC_{M}UβC.$ If $K$ carries an $M-algebra$ structure $Ξ½,$ and the limit projections $Ο:KβF(j)$ are $M-algebra$ morphisms, then $(K,Ξ½)$ is the limit of $F$ in $C_{M}.$

make-algebra-limit : β {K : Functor β€Cat C} {eps : K Fβ !F => Forget-EM Fβ F} β (lim : is-ran !F (Forget-EM Fβ F) K eps) β (nu : Algebra-on C M (K .Fβ tt)) β (β j β is-limit.Ο lim j C.β nu .Ξ½ β‘ FAlg.Ξ½ j C.β M.Mβ (is-limit.Ο lim j)) β make-is-limit F (K .Fβ tt , nu) make-algebra-limit lim apex-alg comm = em-lim where module lim = is-limit lim open make-is-limit module apex = Algebra-on apex-alg open _=>_

The assumptions to this lemma are actually rather hefty: they pretty
much directly say that
$K$
was already the limit of
$F.$
However, with this more βelementaryβ rephrasing, we gain a bit of extra
control which will be necessary for *constructing* limits in
$C_{M}$
out of limits in
$C$
later.

em-lim : make-is-limit F _ em-lim .Ο j .hom = lim.Ο j em-lim .Ο j .preserves = comm j em-lim .commutes f = ext (lim.commutes f) em-lim .universal eps p .hom = lim.universal (Ξ» j β eps j .hom) (Ξ» f i β p f i .hom) em-lim .factors eps p = ext (lim.factors _ _) em-lim .unique eps p other q = ext (lim.unique _ _ _ Ξ» j i β q j i .hom) em-lim .universal eps p .preserves = lim.uniqueβ _ (Ξ» f β C.pulll (F.Fβ f .preserves) β C.pullr (sym (M.M-β _ _) β ap M.Mβ (ap hom (p f)))) (Ξ» j β C.pulll (lim.factors _ _) β eps j .preserves) (Ξ» j β C.pulll (comm j) β C.pullr (sym (M.M-β _ _) β ap M.Mβ (lim.factors _ _)))

This key lemma also doubles as a proof that the underlying object functor $U$ reflects limits: We already had an algebra structure βupstairsβ!

Forget-reflects-limits : reflects-limit Forget-EM F Forget-reflects-limits {K} {eps} lim = to-is-limitp (make-algebra-limit lim (K .Fβ tt .snd) (Ξ» j β eps .Ξ· j .preserves)) trivial!

Having shown that
$U$
reflects the property of *being a limit*, we now turn to showing
it reflects limits in general. Using our key lemma, it will suffice to
construct an algebra structure on
$lim_{j}UF(j),$
then show that the projection maps
$Ο_{j}:(lim_{j}UF(j))βUF(j)$
extend to algebra homomorphisms.

Forget-lift-limit : Limit (Forget-EM Fβ F) β Limit F Forget-lift-limit lim-over = to-limit $ to-is-limit $ make-algebra-limit (Limit.has-limit lim-over) apex-algebra (Ξ» j β lim-over.factors _ _) where module lim-over = Limit lim-over module lim = Ran lim-over

An algebra structure consists, centrally, of a map
$M(lim_{j}UF(j))βlim_{j}UF(j):$
a map *into* the limit. Maps into limits are the happy case,
since
$lim_{j}UF(j)$
is essentially defined by a (natural) isomorphism between the sets
$Hom(X,lim_{j}UF(j))$
and
$lim_{j}Hom(X,UF(j)),$
the latter limit being computed in
$Sets.$
We understand limits of sets very well: theyβre (subsets of) sets of
tuples!

Our algebra map is thus defined *componentwise*: Since we have
a bunch of maps
$Ξ½_{j}:M(UF(j))βUF(j),$
coming from the algebra structures on each
$F(j),$
we can βtupleβ them into a big map
$Ξ½=β¨Ξ½_{j}Ο_{j}β©_{j}.$
Abusing notation slightly, weβre defining
$Ξ½(a,b,...)$
to be
$(Ξ½_{a}(a),Ξ½_{b}(b),...).$

apex-algebra : Algebra-on C M lim-over.apex apex-algebra .Ξ½ = lim-over.universal (Ξ» j β FAlg.Ξ½ j C.β M.Mβ (lim-over.Ο j)) comm where abstract comm : β {x y} (f : J.Hom x y) β F.β f .hom C.β FAlg.Ξ½ x C.β M.Mβ (lim-over.Ο x) β‘ FAlg.Ξ½ y C.β M.Mβ (lim-over.Ο y) comm {x} {y} f = F.β f .hom C.β FAlg.Ξ½ x C.β M.Mβ (lim-over.Ο x) β‘β¨ C.extendl (F.β f .preserves) β©β‘ FAlg.Ξ½ y C.β M.Mβ (F.β f .hom) C.β M.Mβ (lim-over.Ο x) β‘Λβ¨ C.reflβ©ββ¨ M.M-β _ _ β©β‘Λ FAlg.Ξ½ y C.β M.Mβ (F.β f .hom C.β lim-over.Ο x) β‘β¨ C.reflβ©ββ¨ ap M.Mβ (lim-over.commutes f) β©β‘ FAlg.Ξ½ y C.β M.Mβ (lim-over.Ο y) β

To show that $Ξ½$ really is an algebra structure, weβll reason componentwise, too: we must show that $Ξ½(Ξ·_{a},Ξ·_{b},...)$ is the identity map: but we can compute

$Ξ½(Ξ·_{a},Ξ·_{b},...)=(Ξ½_{a}Ξ·_{a},Ξ½_{b}Ξ·_{b},...)=(id,id,...)=id!$## The other condition, compatibility with $Mβs$ multiplication, is analogous. Formally, the computation is a bit less pretty, but itβs no more complicated.

apex-algebra .Ξ½-unit = lim-over.uniqueβ _ lim-over.commutes (Ξ» j β C.pulll (lim-over.factors _ _) Β·Β· C.pullr (sym $ M.unit.is-natural _ _ _) Β·Β· C.cancell (FAlg.Ξ½-unit j)) (Ξ» j β C.idr _) apex-algebra .Ξ½-mult = lim-over.uniqueβ _ (Ξ» f β C.pulll $ C.pulll (F.β f .preserves) β C.pullr (sym (M.M-β _ _) β ap M.Mβ (lim-over.commutes f))) (Ξ» j β C.pulll (lim-over.factors _ _) Β·Β· C.pullr (sym (M.M-β _ _) β ap M.Mβ (lim-over.factors _ _) β M.M-β _ _) Β·Β· C.extendl (FAlg.Ξ½-mult j) Β·Β· ap (FAlg.Ξ½ j C.β_) (M.mult.is-natural _ _ _) Β·Β· C.assoc _ _ _) (Ξ» j β C.pulll (lim-over.factors _ _))

Putting our previous results together, we conclude by observing that, if $C$ is a complete category, then so is $C_{M},$ regardless of how ill-behaved the monad $M$ might be.

Eilenberg-Moore-is-complete : β {a b} β is-complete a b C β is-complete a b (Eilenberg-Moore M) Eilenberg-Moore-is-complete complete F = Forget-lift-limit F (complete _)