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 $\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 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 auxiliary 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)) {\xrightarrow{M_1(\psi_x)}} M_0 (F_0(x)) {\xrightarrow{\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 $\mathcal{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 $\mathcal{C}$ is a complete category, then so is $\mathcal{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 _)