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 $∙ ∙,$ that is, two points)
Binary equalisers (limits over diagrams of the form $∙ ⇉ ∙)$
Binary pullbacks (limits over diagrams of the form $∙ \to ∙ \leftarrow ∙)$

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
    field
      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$ is a univalent category (which is required to go from binary products to finite products).

  Finitely-complete→is-finitely-complete
    : is-category C
    → Finitely-complete → is-finitely-complete
  Finitely-complete→is-finitely-complete cat Flim finite =
    limit-as-equaliser-of-product
      (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Ob))
      (Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Arrows))
      (Flim .equalisers)

  is-finitely-complete→Finitely-complete
    : 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 $P$ be a (the) product of $X$ and $Y,$ with its projections called $p_{1}$ and $p_{2} .$ Letting $X f Z g Y$ be a cospan, if the composites $f p_{1}$ and $g p_{2}$ have an equaliser $e : 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 \times Y$ or equalisers $equ (f, g) .$ If we work slightly more concretely, then this can be read as building the pullback $X \times_{Z} Y$ as the largest subobject of $X \times Y$ where $f, g$ agree. In particular, the pullback we want is the object $X \times_{Z} Y$ in the commutative diagram below.

  product-equaliser→pullback
    : ∀ {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 $f$ and $g,$ note that we can factor any pair of arrows $P^{'} \to X$ and $P^{'} \to Y$ through the Cartesian product $X \times Y,$ and use the universal property of equalisers to factor that as a unique arrow $P^{'} \to X \times_{Z} Y .$

    pb .universal {p₁' = p₁'} {p₂' = p₂'} p =
      eq.universal {e' = pr.⟨ p₁' , p₂' ⟩} (
        (f ∘ p1) ∘ pr.⟨ p₁' , p₂' ⟩ ≡⟨ pullr pr.π₁∘factor ⟩
        f ∘ p₁'                     ≡⟨ p ⟩
        g ∘ p₂'                     ≡˘⟨ pullr pr.π₂∘factor ⟩
        (g ∘ p2) ∘ pr.⟨ p₁' , p₂' ⟩ ∎
      )
    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.

  with-equalisers
    : 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 }
    where
      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 $* .$

  terminal-pullback→product
    : ∀ {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

  with-pullbacks
    : 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),$ for some $f, g : A \to B .$ We can consider the two sides of this equation as a single map $⟨ f, g ⟩ : A \to B \times B;$ The equation is solved where this pairing map equals some $(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, $f$ and $g$ become equal. Here’s where we use the fact that pullback squares, well, commute: We know that $f$ is $π_{1} \circ ⟨ f, g ⟩,$ and that $⟨ f, g ⟩ \circ equ = ⟨ id, id ⟩$ (since the square above is a pullback).

But both projections out of $⟨ id, id ⟩$ are equal, so we can apply commutativity of the square above again to conclude that $f \circ equ = g \circ 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^{'}$ is another map which equalises $f$ and $g,$ then it fits into a commutative diagram like the one below, so that we may conclude the dashed arrow $E^{'} \to 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) \to A$ in our pullback diagram is indeed the equaliser of $f$ and $g .$

      eq .has-is-eq .universal {e' = e'} p =
        Pb.universal (Bb.unique₂ refl refl (sym p1) (sym p2))
        where
          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'
        where
          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

    field
      pres-⊤ : ∀ {T} → is-terminal C T → is-terminal D (F.₀ T)
      pres-pullback
        : ∀ {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 \times B$ can be identified with pullbacks $A \times_{⊤} B,$ if $C$ has a terminal object, then a lex functor $F : C \to D$ also preserves products.

    pres-product
      : ∀ {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 \to B$ being a monomorphism is equivalent to certain squares being pullbacks, a lex functor $F : C \to D$ preserves monomorphisms.

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