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.Prelude

import Cat.Reasoning

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


# Limits in categories of algebras🔗

Suppose that $\ca{C}$ be a category, $M$ be a monad on $\ca{C}$, and $F$ be a $\ca{J}$-shaped diagram of $M$-algebras (that is, a functor $F : \ca{J} \to \ca{C}^M$ into the Eilenberg-Moore category of M). Suppose that an evil wizard has given you a limit for the diagram in $\ca{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 $\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 : \ca{C}^M \to \ca{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 auxilliary 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)) \xto{M_1(\psi_x)} M_0 (F_0(x)) \xto{\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 $\ca{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 $\ca{C}$ is a complete category, then so is $\ca{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 _)