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.

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!

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

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

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