open import Cat.Functor.Kan.Reflection
open import Cat.Functor.Conservative
open import Cat.Diagram.Limit.Base
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Naturality
open import Cat.Functor.Kan.Base
open import Cat.Displayed.Total
open import Cat.Functor.Algebra
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open lifts-limit
module Cat.Functor.Algebra.Limits where

Limits in categories of F-algebras🔗

This short note details the construction of limits in categories of F-algebras from limits in the underlying category; it is similar to the construction of limits in categories of algebras for a monad.

module _
  {o ℓ oj ℓj} {C : Precategory o ℓ}
  (F : Functor C C)
  {J : Precategory oj ℓj} (K : Functor J (FAlg F))
  where
  open Cat.Reasoning C
  private
    module J = Cat.Reasoning J
    module F = Cat.Functor.Reasoning F
    module K = Cat.Functor.Reasoning K
  open ∫Hom

Let be an endofunctor, and be a diagram of If has a limit of then can be equipped with an structure that makes it the limit of in 

  Forget-algebra-lifts-limit : Limit (πᶠ (F-Algebras F) F∘ K) → Limit K
  Forget-algebra-lifts-limit L = to-limit (to-is-limit L') where
    module L = Limit L
    open make-is-limit

As noted earlier, the underlying object of the limit is The algebra is constructed via the universal property of to give a map it suffices to give maps for every which we can construct by composing the projection with the algebra 

    apex : FAlg.Ob F
    apex .fst = L.apex
    apex .snd = L.universal (λ j → K.₀ j .snd ∘ F.₁ (L.ψ j)) comm where abstract
      comm
        : ∀ {i j : J.Ob} (f : J.Hom i j)
        → K.₁ f .fst ∘ K.₀ i .snd ∘ F.₁ (L.ψ i) ≡ K.₀ j .snd ∘ F.₁ (L.ψ j)
      comm {i} {j} f =
        K.₁ f .fst ∘ K.₀ i .snd ∘ F.₁ (L.ψ i)         ≡⟨ pulll (K.₁ f .snd) ⟩
        (K.₀ j .snd ∘ F.₁ (K.₁ f .fst)) ∘ F.₁ (L.ψ i) ≡⟨ F.pullr (L.commutes f) ⟩
        K.₀ j .snd ∘ F.₁ (L.ψ j)                      ∎

A short series of calculations shows that the projections and universal map associated to are homomorphisms.

    L' : make-is-limit K apex
    L' .ψ j .fst = L.ψ j
    L' .ψ j .snd = L.factors _ _
    L' .universal eps p .fst =
      L.universal (λ j → eps j .fst) (λ f → ap fst (p f))
    L' .universal eps p .snd =
      L.unique₂ (λ j → K.F₀ j .snd ∘ F.₁ (eps j .fst))
        (λ f → pulll (K.₁ f .snd) ∙ F.pullr (ap fst (p f)))
        (λ j → pulll (L.factors _ _) ∙ eps j .snd)
        (λ j → pulll (L.factors _ _) ∙ F.pullr (L.factors _ _))

Finally, equality of morphisms of is given by equality on the underlying morphisms, so all of the relevant diagrams in commute.

    L' .commutes f =
      ∫Hom-path (F-Algebras F) (L.commutes f) prop!
    L' .factors eps p =
      ∫Hom-path (F-Algebras F) (L.factors _ _) prop!
    L' .unique eps p other q =
      ∫Hom-path (F-Algebras F) (L.unique _ _ _ λ j → ap fst (q j)) prop!
module _
  {o ℓ oj ℓj} {C : Precategory o ℓ}
  (F : Functor C C)
  {J : Precategory oj ℓj}
  where

Packaging this together, we have that the forgetful functor from the category of to creates limits.

  Forget-algebra-lifts-limits : lifts-limits-of J (πᶠ (F-Algebras F))
  Forget-algebra-lifts-limits lim .lifted = Forget-algebra-lifts-limit F _ lim
  Forget-algebra-lifts-limits lim .preserved = trivial-is-limit! (Ran.has-ran lim)

  Forget-algebra-creates-limits : creates-limits-of J (πᶠ (F-Algebras F))
  Forget-algebra-creates-limits = conservative+lifts→creates-limits
    Forget-algebra-is-conservative Forget-algebra-lifts-limits
module _
  {o ℓ oκ ℓκ} {C : Precategory o ℓ}
  (complete : is-complete oκ ℓκ C)
  where

This gives us the following useful corollary: if is then is also complete.

  FAlg-is-complete : (F : Functor C C) → is-complete oκ ℓκ (FAlg F)
  FAlg-is-complete F = lifts-limits→complete (πᶠ (F-Algebras F))
    (Forget-algebra-lifts-limits F) complete