open import Cat.Functor.Equivalence.Complete
open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Conservative
open import Cat.Functor.Equivalence
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Functor.Kan.Base
open import Cat.Prelude

import Cat.Reasoning

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

private
module EM = Cat.Reasoning (Eilenberg-Moore C M)
module C = Cat.Reasoning C

open Algebra-hom
open Algebra-on


# 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 J = Precategory J
module F = Functor F
module FAlg j = Algebra-on (F.β j .snd)
open Functor
open _=>_


We begin with the following key lemma: Write $K : \mathcal{C}$ for the limit of a diagram $\mathcal{J} \xrightarrow{F} \mathcal{C}^M \xrightarrow{U} \mathcal{C}$. If $K$ carries an $M$-algebra structure $\nu$, and the limit projections $\psi : K \to F(j)$ are $M$-algebra morphisms, then $(K, \nu)$ is the limit of $F$ in $\mathcal{C}^M$.

  make-algebra-limit
: β {K : Functor β€Cat C} {eps : K Fβ !F => Forget C M Fβ F}
β (lim : is-ran !F (Forget C M 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 $\mathcal{C}^M$ out of limits in $\mathcal{C}$ later.

    em-lim : make-is-limit F _
em-lim .Ο j .morphism = lim.Ο j
em-lim .Ο j .commutes = comm j
em-lim .commutes f    = ext (lim.commutes f)
em-lim .universal eta p .morphism =
lim.universal (Ξ» j β eta j .morphism) (Ξ» f i β p f i .morphism)
em-lim .factors eta p =
ext (lim.factors _ _)
em-lim .unique eta p other q =
ext (lim.unique _ _ _ Ξ» j i β q j i .morphism)
em-lim .universal eta p .commutes = lim.uniqueβ _
(Ξ» f β C.pulll (F.Fβ f .commutes)
β C.pullr (sym (M.M-β _ _) β ap M.Mβ (ap morphism (p f))))
(Ξ» j β C.pulll (lim.factors _ _)
β eta j .commutes)
(Ξ» 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 C M) F
Forget-reflects-limits {K} {eps} lim = to-is-limitp
(make-algebra-limit lim (K .Fβ tt .snd) (Ξ» j β eps .Ξ· j .commutes))
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 $\psi_j : (\lim_j UF(j)) \to UF(j)$ extend to algebra homomorphisms.

  Forget-lift-limit : Limit (Forget C M 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)) \to \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 $\mathbf{Hom}(X, \lim_j UF(j))$ and $\lim_j \mathbf{Hom}(X, UF(j))$, the latter limit being computed in $\mathbf{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 $\nu_j : M(UF(j)) \to UF(j)$, coming from the algebra structures on each $F(j)$, we can βtupleβ them into a big map $\nu = \langle \nu_j \psi_j \rangle _j$. Abusing notation slightly, weβre defining $\nu(a, b, ...)$ to be $(\nu_a(a), \nu_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 .morphism C.β FAlg.Ξ½ x C.β M.Mβ (lim-over.Ο x)
β‘ FAlg.Ξ½ y C.β M.Mβ (lim-over.Ο y)
comm {x} {y} f =
F.β f .morphism C.β FAlg.Ξ½ x C.β M.Mβ (lim-over.Ο x)        β‘β¨ C.extendl (F.β f .commutes) β©β‘
FAlg.Ξ½ y C.β M.Mβ (F.β f .morphism) C.β M.Mβ (lim-over.Ο x) β‘Λβ¨ C.reflβ©ββ¨ M.M-β _ _ β©β‘Λ
FAlg.Ξ½ y C.β M.Mβ (F.β f .morphism C.β lim-over.Ο x)        β‘β¨ C.reflβ©ββ¨ ap M.Mβ (lim-over.commutes f) β©β‘
FAlg.Ξ½ y C.β M.Mβ (lim-over.Ο y)                            β


To show that $\nu$ really is an algebra structure, weβll reason componentwise, too: we must show that $\nu(\eta_a, \eta_b, ...)$ is the identity map: but we can compute

$\nu(\eta_a, \eta_b, ...) = (\nu_a\eta_a, \nu_b\eta_b, ...) = (\operatorname{id}_{}, \operatorname{id}_{}, ...) = \operatorname{id}_{}\text{!}$

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 .commutes)
β 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 $\mathcal{C}$ is a complete category, then so is $\mathcal{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 _)