🔍

Equations Inline Footnotes

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 $F:\mathcal{C}\to \mathcal{C}$ be an endofunctor, and $K:\mathcal{J}\to \mathrm{Alg}(F)$ be a diagram of $F\text{-algebras.}$ If $\mathcal{C}$ has a limit $L$ of $\pi \circ K\text{,}$ then $L$ can be equipped with an $F\text{-algebra}$ structure that makes it the limit of $K$ in $\mathrm{Alg}(F)\text{.}$

  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 $L\text{.}$ The algebra $F(L)\to L$ is constructed via the universal property of $L\text{:}$ to give a map $F(L)\to L\text{,}$ it suffices to give maps $F(L)\to K(j)$ for every $j:\mathcal{J}\text{,}$ which we can construct by composing the projection $F({\psi }_j):F(L)\to F(K(j))$ with the algebra $F(K(j))\to K(j)\text{.}$

    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 $L$ are $F\text{-algebra}$ 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 $F\text{-algebras}$ is given by equality on the underlying morphisms, so all of the relevant diagrams in $\mathrm{Alg}(F)$ commute.

    L' .commutes f = ext (L.commutes f)
    L' .factors eps p = ext (L.factors _ _)
    L' .unique eps p other q = ext $ L.unique _ _ _ λ j → ap fst (q j)

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 $F\text{-algebras}$ to $C$ 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 $\mathcal{C}$ is $\kappa \text{-complete,}$ then $\mathrm{Alg}(F)$ is also $\kappa$ 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