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 C\ca{C} be a category, MM be a monad on C\ca{C}, and FF be a J\ca{J}-shaped diagram of MM-algebras (that is, a functor F:JCMF : \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 C\ca{C} which underlies FF, but they have not (being evil and all) told you whether limF\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 GG, HH, considered as a discrete diagram, then the limit our evil wizard would give us is the product U(G)×U(H)U(G) \times U(H) in Sets\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:CMCU : \ca{C}^M \to \ca{C} both preserves and reflects limits, in that KK is a limiting cone if, and only if, U(K)U(K) is.

module _ {jo jℓ} {J : Precategory jo jℓ} (F : Functor J (Eilenberg-Moore C M)) where
  private module F = Functor F

    : (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 LL be a cone over FF: Since U(K)U(K) is a limiting cone, then we have a unique map of U(L)U(K)U(L) \to U(K), which we must show extends to a map of algebras LKL \to K, which by definition means !ν=νM1(!)! \nu = \nu M_1(!). But those are maps M0(L)U(K)M_0(L) \to U(K) — so if M0(L)M_0(L) was a cone over UFU \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 M0(L)M_0(L) is given by composites ψxν\psi_x \nu, which commute because ψ\psi is also a cone structure. More explicitly, what we must show is F1(o)ψxν=ψyνF_1(o) \psi_x \nu = \psi_y \nu, which follows immediately.

        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)U(K)U(L) \to U(K) is unique, and that the functor UU is faithful.

    unique :  x  !  x
    unique x = Cone-hom-path _ $ Algebra-hom-path _ $
      ap hom (uniq (F-map-cone (Forget _ M) other) .paths hom′)
        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 KK. 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 UFU \circ F has a limit, then so does FF.

  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⊤)
      open Terminal
      module cone = Cone (lim-over .top)

What we must do, essentially, is prove that lim(UF)\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 UFU \circ F, one with underlying object given by M(lim(UF))M(\lim (U \circ F)) and one by M2(lim(UF))M^2(\lim (U \circ F)). We construct the one with a single MM first, and re-use its maps in the construction of the one with M2M^2.

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

M0(lim(UF))M1(ψx)M0(F0(x))νF0(x) 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 MM’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(UF)\lim (U \circ F). It’s very tedious, but the multiplication is uniquely defined since it’s a map M(lim(UF))lim(UF)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 = ; 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 CM\ca{C}^M are given by the cone maps we started with — specialising again to groups, we’re essentially showing that the projection map π1:G×HG\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 C\ca{C} is a complete category, then so is CM\ca{C}^M, with no assumptions on MM.

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