open import Cat.Functor.Equivalence.Complete open import Cat.Functor.Conservative open import Cat.Functor.Equivalence open import Cat.Diagram.Limit.Base open import Cat.Diagram.Terminal open import Cat.Diagram.Monad open import Cat.Prelude import Cat.Reasoning module Cat.Diagram.Monad.Limits {o β} {C : Precategory o β} {M : Monad C} where

# Limits in categories of algebrasπ

Suppose that $\mathcal{C}$ be a category, $M$ be a monad on $\mathcal{C}$, and $F$ be a $\mathcal{J}$-shaped diagram of $M$-algebras (that is, a functor $F : \mathcal{J} \to \mathcal{C}^M$ into the Eilenberg-Moore category of M). Suppose that an evil wizard has given you a limit for the diagram in $\mathcal{C}$ which underlies $F$, but they have not (being evil and all) told you whether $\lim F$ 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) \times U(H)$
in
${{\mathbf{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 : \mathcal{C}^M \to \mathcal{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 C M)) where private module F = Functor F Forget-reflects-limits : (K : Cone F) β is-limit (Forget C M Fβ F) (F-map-cone (Forget C M) K) β is-limit F K Forget-reflects-limits K uniq other = contr ! unique where !β² = uniq (F-map-cone (Forget C M) other) .centre

Let
$L$
be a cone over
$F$:
Since
$U(K)$
is a limiting cone, then we have a unique map of
$U(L) \to U(K)$,
which we must show extends to a map of *algebras*
$L \to K$,
which by definition means
$! \nu = \nu M_1(!)$.
But those are maps
$M_0(L) \to U(K)$
β so if
$M_0(L)$
was a cone over
$U \circ F$,
and those two were maps of cones, then they would be equal!

! : Cone-hom _ other K ! .hom .morphism = !β² .hom ! .hom .commutes = ap hom $ is-contrβis-prop (uniq coneβ²) (record { hom = !β² .hom C.β apex other .snd .Ξ½ ; commutes = Ξ» o β C.pulll (!β² .commutes o) }) (record { hom = apex K .snd .Ξ½ C.β M.Mβ (!β² .hom) ; commutes = Ξ» o β C.pulll (K .Ο o .commutes) Β·Β· C.pullr (sym (M.M-β _ _) β ap M.Mβ (!β² .commutes o)) Β·Β· sym (other .Ο o .commutes) })

The cone structure on $M_0(L)$ is given by composites $\psi_x \nu$, which commute because $\psi$ is also a cone structure. More explicitly, what we must show is $F_1(o) \psi_x \nu = \psi_y \nu$, which follows immediately.

where coneβ² : Cone (Forget C M Fβ F) coneβ² .apex = M.Mβ (apex other .fst) coneβ² .Ο x = morphism (Ο other x) C.β apex other .snd .Ξ½ coneβ² .commutes o = C.pulll (ap morphism (commutes other o)) ! .commutes o = Algebra-hom-path _ (uniq (F-map-cone (Forget C M) other) .centre .commutes o)

For uniqueness, we use that the map $U(L) \to U(K)$ is unique, and that the functor $U$ is faithful.

unique : β x β ! β‘ x unique x = Cone-hom-path _ $ Algebra-hom-path _ $ ap hom (uniq (F-map-cone (Forget _ M) other) .paths homβ²) where homβ² : Cone-hom _ _ _ homβ² .hom = hom x .morphism homβ² .commutes o = ap morphism (x .commutes o)

I hope you like appealing to uniqueness of maps into limits, by the
way. We now relax the conditions on the theorem above, which relies on
the pre-existence of a cone
$K$.
In fact, what we have shown is that `Forget`

reflects the
property of *being a limit* β what we now show is that it
reflects limit *objects*, too: if
$U \circ F$
has a limit, then so does
$F$.

Forget-lift-limit : Limit (Forget _ M Fβ F) β Limit F Forget-lift-limit lim-over = record { top = coneβ² ; hasβ€ = Forget-reflects-limits coneβ² $ subst (is-limit _) (sym U$Lβ‘L) (lim-over .hasβ€) } where open Terminal module cone = Cone (lim-over .top)

What we must do, essentially, is prove that $\lim (U \circ F)$ admits an algebra structure, much like we did for products of groups. In this, weβll use two auxiliary cones over $U \circ F$, one with underlying object given by $M(\lim (U \circ F))$ and one by $M^2(\lim (U \circ F))$. We construct the one with a single $M$ first, and re-use its maps in the construction of the one with $M^2$.

The maps out of $M_0(\lim (U \circ F))$ are given by the composite below, which assembles into a cone since $F_1(f)$ is a map of algebras and $\psi$ is a cone.

$M_0 (\lim (U \circ F)) {\xrightarrow{M_1(\psi_x)}} M_0 (F_0(x)) {\xrightarrow{\nu}} F_0(x)$

coneβ : Cone (Forget _ M Fβ F) coneβ .apex = M.Mβ cone.apex coneβ .Ο x = F.β x .snd .Ξ½ C.β M.Mβ (cone.Ο x) coneβ .commutes {x} {y} f = F.β f .morphism C.β F.β x .snd .Ξ½ C.β M.Mβ (cone.Ο x) β‘β¨ C.pulll (F.β f .commutes) β©β‘ (F.β y .snd .Ξ½ C.β M.Mβ (F.β f .morphism)) C.β M.Mβ (cone.Ο x) β‘β¨ C.pullr (sym (M.M-β _ _) β ap M.Mβ (cone.commutes f)) β©β‘ F.β y .snd .Ξ½ C.β M.Mβ (cone.Ο y) β

Below, we can reuse the work we did above by precomposing with $M$βs multiplication $\mu$.

coneΒ² : Cone (Forget _ M Fβ F) coneΒ² .apex = M.Mβ (M.Mβ cone.apex) coneΒ² .Ο x = coneβ .Ο x C.β M.mult.Ξ· _ coneΒ² .commutes f = C.pulll (coneβ .commutes f)

We now define the algebra structure on $\lim (U \circ F)$. Itβs very tedious, but the multiplication is uniquely defined since itβs a map $M(\lim (U \circ F)) \to \lim (U \circ F)$ into a limit, and the algebraic identities follow from again from limits being terminal.

coneβ² : Cone F coneβ² .apex = cone.apex , alg where

alg : Algebra-on _ M cone.apex alg .Ξ½ = lim-over .hasβ€ coneβ .centre .hom alg .Ξ½-unit = ap hom $ is-contrβis-prop (lim-over .hasβ€ (lim-over .top)) (record { hom = alg .Ξ½ C.β M.unit.Ξ· cone.apex ; commutes = comm1 }) (record { hom = C.id ; commutes = Ξ» _ β C.idr _ }) alg .Ξ½-mult = ap hom $ is-contrβis-prop (lim-over .hasβ€ coneΒ²) (record { hom = alg .Ξ½ C.β M.Mβ (alg .Ξ½) ; commutes = comm2 }) (record { hom = alg .Ξ½ C.β M.mult.Ξ· cone.apex ; commutes = Ξ» o β C.pulll (lim-over .hasβ€ coneβ .centre .commutes o) })

The cone maps in
$\mathcal{C}^M$
are given by the cone maps we started with β specialising again to
groups, weβre essentially showing that the projection map
$\pi_1 : G \times H \to G$
*between sets* is actually a group homomorphism.

coneβ² .Ο x .morphism = cone.Ο x coneβ² .Ο x .commutes = lim-over .hasβ€ coneβ .centre .commutes x coneβ² .commutes f = Algebra-hom-path _ (cone.commutes f) U$Lβ‘L : F-map-cone (Forget _ M) coneβ² β‘ lim-over .top U$Lβ‘L = Cone-path _ refl Ξ» o β refl

We conclude by saying that, if $\mathcal{C}$ is a complete category, then so is $\mathcal{C}^M$, with no assumptions on $M$.

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 _)