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!
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 oκ ℓκ (FAlg F) FAlg-is-complete F = lifts-limits→complete (πᶠ (F-Algebras F)) (Forget-algebra-lifts-limits F) complete