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:Jβ†’CMF : \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 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\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 : \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

  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 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 Lβ†’KL \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 U∘FU \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.

      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)β†’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β€²)
      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 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 U∘FU \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⊀)
           }
    where
      open Terminal
      module cone = Cone (lim-over .top)

What we must do, essentially, is prove that lim⁑(U∘F)\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∘FU \circ F, one with underlying object given by M(lim⁑(U∘F))M(\lim (U \circ F)) and one by M2(lim⁑(U∘F))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⁑(U∘F))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⁑(U∘F))β†’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⁑(U∘F)\lim (U \circ F). It’s very tedious, but the multiplication is uniquely defined since it’s a map M(lim⁑(U∘F))β†’lim⁑(U∘F)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 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Γ—Hβ†’G\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.

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