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

Limits in categories of algebrasπŸ”—

Suppose that C\mathcal{C} be a category, MM be a monad on C\mathcal{C}, and FF be a J\mathcal{J}-shaped diagram of MM-algebras (that is, a functor F:Jβ†’CMF : \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 C\mathcal{C} which underlies FF, but they have not (being evil and all) told you whether lim⁑F\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\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:CMβ†’CU : \mathcal{C}^M \to \mathcal{C} both preserves and reflects limits, in that KK is a limiting cone if, and only if, U(K)U(K) is.

We begin with the following key lemma: Write K:CK : \mathcal{C} for the limit of a diagram Jβ†’FCMβ†’UC\mathcal{J} \xrightarrow{F} \mathcal{C}^M \xrightarrow{U} \mathcal{C}. If KK carries an MM-algebra structure Ξ½\nu, and the limit projections ψ:Kβ†’F(j)\psi : K \to F(j) are MM-algebra morphisms, then (K,Ξ½)(K, \nu) is the limit of FF in CM\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 KK was already the limit of FF. However, with this more β€œelementary” rephrasing, we gain a bit of extra control which will be necessary for constructing limits in CM\mathcal{C}^M out of limits in C\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 UU 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 UU 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⁑jUF(j)\lim_j UF(j), then show that the projection maps ψj:(lim⁑jUF(j))β†’UF(j)\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⁑jUF(j))β†’lim⁑jUF(j)M(\lim_j UF(j)) \to \lim_j UF(j): a map into the limit. Maps into limits are the happy case, since lim⁑jUF(j)\lim_j UF(j) is essentially defined by a (natural) isomorphism between the sets Hom(X,lim⁑jUF(j))\mathbf{Hom}(X, \lim_j UF(j)) and lim⁑jHom(X,UF(j))\lim_j \mathbf{Hom}(X, UF(j)), the latter limit being computed in Sets\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 Ξ½j:M(UF(j))β†’UF(j)\nu_j : M(UF(j)) \to UF(j), coming from the algebra structures on each F(j)F(j), we can β€œtuple” them into a big map Ξ½=⟨νjψj⟩j\nu = \langle \nu_j \psi_j \rangle _j. Abusing notation slightly, we’re defining Ξ½(a,b,...)\nu(a, b, ...) to be (Ξ½a(a),Ξ½b(b),...)(\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 Ξ½(Ξ·a,Ξ·b,...)\nu(\eta_a, \eta_b, ...) is the identity map: but we can compute

ν(ηa,ηb,...)=(νaηa,νbηb,...)=(id⁑,id⁑,...)=id⁑! \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 MM’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 C\mathcal{C} is a complete category, then so is CM\mathcal{C}^M, regardless of how ill-behaved the monad MM 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 _)