module Cat.Diagram.Limit.Finite where

Finitely Complete Categories🔗

A category is said to be finitely complete if it admits limits for every diagram with a finite shape.

  is-finitely-complete : Typeω
  is-finitely-complete = ∀ {o ℓ} {D : Precategory o ℓ} → is-finite-precategory D
                       → (F : Functor D C) → Limit F

Similarly to the case with arbitrary limits, we can get away with only the following common shapes of limits:

  • A terminal object (limit over the empty diagram)
  • Binary products (limits over diagrams of the form ∙∙\bullet\quad\bullet, that is, two points)
  • Binary equalisers (limits over diagrams of the form ∙⇉∙\bullet\rightrightarrows\bullet)
  • Binary pullbacks (limits over diagrams of the form ∙→∙←∙\bullet\to\bullet\leftarrow\bullet)

In reality, the list above has some redundancy. Since we can build products out of pullbacks and a terminal object, and conversely we can build pullbacks out of products and equalisers, either of the following subsets suffices:

  • A terminal object, binary products, binary equalisers;
  • A terminal object and binary pullbacks.

For proving that a thin category is finitely complete, given that equalisers are trivial and pullbacks coincide with products, it suffices to give a terminal object and binary products.

  record Finitely-complete : Type (ℓ ⊔ ℓ') where
      terminal   : Terminal C
      products   : has-products C
      equalisers : has-equalisers C
      pullbacks  : has-pullbacks C

    Eq : ∀ {A B} (f g : Hom A B) → Ob
    Eq f g = equalisers f g .Equaliser.apex

    Pb : ∀ {A B C} (f : Hom A C) (g : Hom B C) → Ob
    Pb f g = pullbacks f g .Pullback.apex

    module Products = Binary-products C products
    open Products using (_⊗₀_) public

  open Finitely-complete

As promised, the two definitions imply each other, assuming that C\mathcal{C} is a univalent category (which is required to go from binary products to finite products).

    : is-category C
    → Finitely-complete → is-finitely-complete
  Finitely-complete→is-finitely-complete cat Flim finite =
      (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Ob))
      (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Mor))
      (Flim .equalisers)

    : is-finitely-complete → Finitely-complete
  is-finitely-complete→Finitely-complete flim = Flim where
    Flim : Finitely-complete
    Flim .terminal = Limit→Terminal C (flim finite-cat _)
    Flim .products a b = Limit→Product C (flim Disc-finite _)
    Flim .equalisers f g = Limit→Equaliser C (flim ·⇉·-finite _)
    Flim .pullbacks f g = Limit→Pullback C {lzero} {lzero} (flim ·→·←·-finite _)

With equalisers🔗

We now prove that having products and equalisers suffices to have all pullbacks; Thus a terminal object, binary products and binary equalisers suffice for finite completeness.

The main result is as follows: Let PP be a (the) product of XX and YY, with its projections called p1p_1 and p2p_2. Letting X→fZ←gYX \xrightarrow{f} Z \xleftarrow{g} Y be a cospan, if the composites fp1fp_1 and gp2gp_2 have an equaliser e:E→Pe : E \to P, then the square

is a pullback. Now, that description is almost entirely abstract-nonsensical, because (for generality) we do not use any “canonical” products X×YX \times Y or equalisers equ(f,g)\mathrm{equ}(f,g). If we work slightly more concretely, then this can be read as building the pullback X×ZYX \times_Z Y as the largest subobject of X×YX \times Y where f,gf, g agree. In particular, the pullback we want is the object X×ZYX \times_Z Y in the commutative diagram below.

    : ∀ {E P X Y Z} {p1 : Hom P X} {p2 : Hom P Y} {f : Hom X Z}
        {g : Hom Y Z} {e : Hom E P}
    → is-product C p1 p2
    → is-equaliser C (f ∘ p1) (g ∘ p2) e
    → is-pullback C (p1 ∘ e) f (p2 ∘ e) g
  product-equaliser→pullback {p1 = p1} {p2} {f} {g} {e} prod eq = pb where
    open is-pullback
    module eq = is-equaliser eq
    module pr = is-product prod

    pb : is-pullback C _ _ _ _
    pb .square = assoc _ _ _ ∙ eq.equal ∙ sym (assoc _ _ _)

To show that this object really is a pullback of ff and gg, note that we can factor any pair of arrows P′→XP' \to X and P′→YP' \to Y through the Cartesian product X×YX \times Y, and use the universal property of equalisers to factor that as a unique arrow P′→X×ZYP' \to X \times_Z Y.

    pb .universal {p₁' = p₁'} {p₂' = p₂'} p =
      eq.universal {e′ = pr.⟨ p₁' , p₂' ⟩pr.} (
        (f ∘ p1) ∘ pr.⟨ p₁' , p₂' ⟩pr. ≡⟨ pullr pr.π₁∘factor ⟩≡
        f ∘ p₁'                     ≡⟨ p ⟩≡
        g ∘ p₂'                     ≡˘⟨ pullr pr.π₂∘factor ⟩≡˘
        (g ∘ p2) ∘ pr.⟨ p₁' , p₂' ⟩pr. ∎
    pb .p₁∘universal = pullr eq.factors ∙ pr.π₁∘factor
    pb .p₂∘universal = pullr eq.factors ∙ pr.π₂∘factor
    pb .unique p q =
      eq.unique ((pr.unique _ (assoc _ _ _ ∙ p) (assoc _ _ _ ∙ q)))

Hence, assuming that a category has a terminal object, binary products and binary equalisers means it also admits pullbacks.

    : Terminal C
    → (∀ A B → Product C A B)
    → (∀ {A B} (f g : Hom A B) → Equaliser C f g)
    → Finitely-complete
  with-equalisers top prod equ .terminal   = top
  with-equalisers top prod equ .products   = prod
  with-equalisers top prod equ .equalisers = equ
  with-equalisers top prod equ .pullbacks {A} {B} {X} f g =
    record { has-is-pb = product-equaliser→pullback Prod.has-is-product Equ.has-is-eq }
      module Prod = Product (prod A B)
      module Equ = Equaliser (equ (f ∘ Prod.π₁) (g ∘ Prod.π₂))

With pullbacks🔗

We’ll now prove the converse: That a terminal object and pullbacks implies having all products, and all equalisers. We’ll start with the products, since those are simpler. Observe that we can complete a product diagram (like the one on the left) to a pullback diagram (like the one on the right) by adding in the unique arrows into the terminal object ∗*.

    : ∀ {P X Y T} {p1 : Hom P X} {p2 : Hom P Y} {f : Hom X T} {g : Hom Y T}
    → is-terminal C T → is-pullback C p1 f p2 g → is-product C p1 p2
  terminal-pullback→product {p1 = p1} {p2} {f} {g} term pb = prod where
    module Pb = is-pullback pb

    prod : is-product C p1 p2
    prod .is-product.⟨_,_⟩ p1' p2' =
      Pb.universal {p₁' = p1'} {p₂' = p2'} (is-contr→is-prop (term _) _ _)
    prod .is-product.π₁∘factor = Pb.p₁∘universal
    prod .is-product.π₂∘factor = Pb.p₂∘universal
    prod .is-product.unique other p q = Pb.unique p q

    : Terminal C
    → (∀ {A B X} (f : Hom A X) (g : Hom B X) → Pullback C f g)
    → Finitely-complete
  with-pullbacks top pb = fc where
    module top = Terminal top
    mkprod : ∀ A B → Product C A B
    mkprod A B = record { has-is-product = terminal-pullback→product top.has⊤ pb′ }
      where pb′ = pb (top.has⊤ A .centre) (top.has⊤ B .centre) .Pullback.has-is-pb

    mkeq : ∀ {A B} (f g : Hom A B) → Equaliser C f g
    mkeq {A = A} {B} f g = eq where

For equalisers, the situation is a bit more complicated. Recall that, by analogy with the case in Set, we can consider the equaliser to be the solution set of f(x)=g(x)f(x) = g(x), for some f,g:A→Bf, g : A \to B. We can consider the two sides of this equation as a single map ⟨f,g⟩:A→B×B\langle f, g \rangle : A \to B \times B; The equation is solved where this pairing map equals some (x,x)(x,x). We can thus build equalisers by pulling back along the diagonal map:

The actual equaliser map is the top, horizontal face (what the code calls Pb.p₂), so we must show that, composed with this map, ff and gg become equal. Here’s where we use the fact that pullback squares, well, commute: We know that ff is π1∘⟨f,g⟩\pi_1 \circ \langle f , g \rangle, and that ⟨f,g⟩∘equ=⟨id⁡,id⁡⟩\langle f , g \rangle \circ \mathrm{equ} = \langle \operatorname{id}_{}, \operatorname{id}_{} \rangle (since the square above is a pullback).

But both projections out of ⟨id⁡,id⁡⟩\langle \operatorname{id}_{}, \operatorname{id}_{} \rangle are equal, so we can apply commutativity of the square above again to conclude that f∘equ=g∘equf \circ \mathrm{equ} = g \circ \mathrm{equ}.

      eq : Equaliser C f g
      eq .apex = Pb.apex
      eq .equ = Pb.p₂
      eq .has-is-eq .equal =
        f ∘ Pb.p₂               ≡˘⟨ pulll Bb.π₁∘factor ⟩≡˘
        Bb.π₁ ∘ ⟨f,g⟩ ∘ Pb.p₂   ≡⟨ ap (Bb.π₁ ∘_) (sym Pb.square) ⟩≡
        Bb.π₁ ∘ ⟨id,id⟩ ∘ Pb.p₁ ≡⟨ pulll Bb.π₁∘factor ∙ sym (pulll Bb.π₂∘factor) ⟩≡
        Bb.π₂ ∘ ⟨id,id⟩ ∘ Pb.p₁ ≡⟨ ap (Bb.π₂ ∘_) Pb.square ⟩≡
        Bb.π₂ ∘ ⟨f,g⟩ ∘ Pb.p₂   ≡⟨ pulll Bb.π₂∘factor ⟩≡
        g ∘ Pb.p₂               ∎

We must now show that if e′e' is another map which equalises ff and gg, then it fits into a commutative diagram like the one below, so that we may conclude the dashed arrow E′→eq(f,g)E' \to \mathrm{eq}(f,g) exists and is unique.

A bit of boring limit-chasing lets us conclude that this diagram does commute, hence the dashed arrow does exist (uniquely!), so that the top face equ:eq(f,g)→A\mathrm{equ} : \mathrm{eq}(f,g) \to A in our pullback diagram is indeed the equaliser of ff and gg.

      eq .has-is-eq .universal {e′ = e′} p =
        Pb.universal (Bb.unique₂ refl refl (sym p1) (sym p2))
          p1 : Bb.π₁ ∘ ⟨id,id⟩ ∘ f ∘ e′ ≡ Bb.π₁ ∘ ⟨f,g⟩ ∘ e′
          p1 =
            Bb.π₁ ∘ ⟨id,id⟩ ∘ f ∘ e′   ≡⟨ cancell Bb.π₁∘factor ⟩≡
            f ∘ e′                     ≡˘⟨ pulll Bb.π₁∘factor ⟩≡˘
            Bb.π₁ ∘ ⟨f,g⟩ ∘ e′         ∎

          p2 : Bb.π₂ ∘ ⟨id,id⟩ ∘ f ∘ e′ ≡ Bb.π₂ ∘ ⟨f,g⟩ ∘ e′
          p2 =
            Bb.π₂ ∘ ⟨id,id⟩ ∘ f ∘ e′   ≡⟨ cancell Bb.π₂∘factor ⟩≡
            f ∘ e′                     ≡⟨ p ⟩≡
            g ∘ e′                     ≡˘⟨ pulll Bb.π₂∘factor ⟩≡˘
            Bb.π₂ ∘ ⟨f,g⟩ ∘ e′         ∎

      eq .has-is-eq .factors = Pb.p₂∘universal
      eq .has-is-eq .unique {F} {e′ = e′} {other = other} p₂∘l=e′ =
        Pb.unique path p₂∘l=e′
          path : Pb.p₁ ∘ other ≡ f ∘ e′
          path =
            Pb.p₁ ∘ other                   ≡⟨ insertl Bb.π₁∘factor ⟩≡
            Bb.π₁ ∘ ⟨id,id⟩ ∘ Pb.p₁ ∘ other ≡⟨ ap (Bb.π₁ ∘_) (extendl Pb.square) ⟩≡
            Bb.π₁ ∘ ⟨f,g⟩ ∘ Pb.p₂ ∘ other   ≡⟨ ap (Bb.π₁ ∘_) (ap (⟨f,g⟩ ∘_) p₂∘l=e′) ⟩≡
            Bb.π₁ ∘ ⟨f,g⟩ ∘ e′              ≡⟨ pulll Bb.π₁∘factor ⟩≡
            f ∘ e′                          ∎

Putting it all together into a record we get our proof of finite completeness:

    fc : Finitely-complete
    fc .terminal = top
    fc .products = mkprod
    fc .equalisers = mkeq
    fc .pullbacks = pb

Lex functors🔗

A functor is said to be left exact, abbreviated lex, when it preserves finite limits. These functors aren’t called “finite-limit-preserving functors” by historical accident, and for brevity. By the characterisations above, it suffices for a functor to preserve the terminal object and pullbacks.

  record is-lex (F : Functor C D) : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
    private module F = Functor F

      pres-⊤ : ∀ {T} → is-terminal C T → is-terminal D (F.₀ T)
        : ∀ {P X Y Z} {p1 : C.Hom P X} {p2 : C.Hom P Y}
            {f : C.Hom X Z} {g : C.Hom Y Z}
        → is-pullback C p1 f p2 g
        → is-pullback D (F.₁ p1) (F.₁ f) (F.₁ p2) (F.₁ g)

Since (if a terminal object exists), products A×BA \times B can be identified with pullbacks A×⊤BA \times_\top B, if C\mathcal{C} has a terminal object, then a lex functor F:C→DF : \mathcal{C} \to \mathcal{D} also preserves products.

      : ∀ {P A B T} {p1 : C.Hom P A} {p2 : C.Hom P B}
      → is-terminal C T
      → is-product C p1 p2
      → is-product D (F.₁ p1) (F.₁ p2)
    pres-product term pr = terminal-pullback→product D (pres-⊤ term)
      (pres-pullback {f = term _ .centre} {g = term _ .centre}
        (product→terminal-pullback C term pr))

Since f:A→Bf : A \to B being a monomorphism is equivalent to certain squares being pullbacks, a lex functor F:C→DF : \mathcal{C} \to \mathcal{D} preserves monomorphisms.

    pres-monos : ∀ {A B} {f : C.Hom A B} → f → (F.₁ f)
    pres-monos {f = f} mono = is-pullback→is-monic
      (subst (λ x → is-pullback D x _ x _) F.F-id
          (is-monic→is-pullback mono)))