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
    no-eta-equality
    field
      terminal   : Terminal C
      products   : Binary-products C
      equalisers : Equalisers C
      pullbacks  : Pullbacks C

    open Terminal terminal public
    open Binary-products products public
    open Equalisers equalisers public
    open Pullbacks pullbacks public

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 terminal products cat (finite .has-finite-Ob))
      (Cartesian→finite-products terminal products cat (finite .has-finite-Arrows))
      equalisers
    where open Finitely-complete Flim

  is-finitely-complete→Finitely-complete
    : is-finitely-complete → Finitely-complete
  is-finitely-complete→Finitely-complete flim = Flim where
    open Finitely-complete

    Flim : Finitely-complete
    Flim .terminal = Limit→Terminal C (flim finite-cat _)
    Flim .products = all-products→binary-products λ a b →
      Limit→Product C (flim Disc-finite _)
    Flim .equalisers = all-equalisers→equalisers λ f g →
      Limit→Equaliser C (flim ·⇉·-finite _)
    Flim .pullbacks = all-pullbacks→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.π₁∘⟨⟩ ⟩
        f ∘ p₁'                     ≡⟨ p ⟩
        g ∘ p₂'                     ≡˘⟨ pullr pr.π₂∘⟨⟩ ⟩
        (g ∘ p2) ∘ pr.⟨ p₁' , p₂' ⟩ ∎
      )
    pb .p₁∘universal = pullr eq.factors ∙ pr.π₁∘⟨⟩
    pb .p₂∘universal = pullr eq.factors ∙ pr.π₂∘⟨⟩
    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
    → Binary-products C
    → Equalisers C
    → Finitely-complete
  with-equalisers top prods eqs .Finitely-complete.terminal = top
  with-equalisers top prods eqs .Finitely-complete.products = prods
  with-equalisers top prods eqs .Finitely-complete.equalisers = eqs
  with-equalisers top prods eqs .Finitely-complete.pullbacks =
    products+equalisers→pullbacks prods eqs

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.π₁∘⟨⟩ = Pb.p₁∘universal
    prod .is-product.π₂∘⟨⟩ = Pb.p₂∘universal
    prod .is-product.unique p q = Pb.unique p q

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:

  product+pullback→equaliser
    : ∀ {E X Y Y²}
    → {f g : Hom X Y} {e : Hom E X} {π₁ π₂ : Hom Y² Y} {p₁ : Hom E Y}
    → (is-prod : is-product C π₁ π₂) (let open is-product is-prod)
    → (is-pb : is-pullback C p₁ ⟨ id , id ⟩ e ⟨ f , g ⟩)
    → is-equaliser C f g e
  product+pullback→equaliser {f = f} {g} {e} {π₁} {π₂} {p₁} is-prod is-pb = is-eq where
    open is-product is-prod renaming (unique₂ to ⟨⟩-unique₂)
    open is-pullback is-pb renaming (unique to pb-unique)

The actual equaliser map is the top, horizontal face (what the code calls e, 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 .$

    is-eq : is-equaliser C f g e
    is-eq .is-equaliser.equal =
      f ∘ e                 ≡˘⟨ pulll π₁∘⟨⟩ ⟩
      π₁ ∘ ⟨ f , g ⟩ ∘ e    ≡˘⟨ ap₂ _∘_ refl square ⟩
      π₁ ∘ ⟨ id , id ⟩ ∘ p₁ ≡⟨ extendl (π₁∘⟨⟩ ∙ sym (π₂∘⟨⟩)) ⟩
      π₂ ∘ ⟨ id , id ⟩ ∘ p₁ ≡⟨ ap₂ _∘_ refl square ⟩
      π₂ ∘ ⟨ f , g ⟩ ∘ e    ≡⟨ pulll π₂∘⟨⟩ ⟩
      g ∘ e ∎

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 .$

    is-eq .is-equaliser.universal {e' = e'} p =
      universal {p₁' = f ∘ e'} {p₂' = e'} comm
      where abstract
        comm : ⟨ id , id ⟩ ∘ f ∘ e' ≡ (⟨ f , g ⟩ ∘ e')
        comm =
          ⟨⟩-unique₂
            (cancell π₁∘⟨⟩) (cancell π₂∘⟨⟩)
            (pulll π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ sym p)
    is-eq .is-equaliser.factors = p₂∘universal
    is-eq .is-equaliser.unique {e' = e'} {p = p} {other = other} e∘other=e' =
      pb-unique
        p₁∘other=f∘e'
        e∘other=e'
      where
        p₁∘other=f∘e' : p₁ ∘ other ≡ f ∘ e'
        p₁∘other=f∘e' =
          p₁ ∘ other                    ≡⟨ insertl π₁∘⟨⟩ ⟩
          π₁ ∘ ⟨ id , id ⟩ ∘ p₁ ∘ other ≡⟨ ap₂ _∘_ refl (extendl square) ⟩
          π₁ ∘ ⟨ f , g ⟩ ∘ e ∘ other    ≡⟨ pulll π₁∘⟨⟩ ⟩
          f ∘ e ∘ other                 ≡⟨ ap₂ _∘_ refl e∘other=e' ⟩
          f ∘ e' ∎

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

  with-pullbacks
    : Terminal C
    → Pullbacks C
    → Finitely-complete
  with-pullbacks top pbs = fc where
    prods : Binary-products C
    prods = terminal+pullbacks→products top pbs

    fc : Finitely-complete
    fc .Finitely-complete.terminal = top
    fc .Finitely-complete.products = prods
    fc .Finitely-complete.equalisers = products+pullbacks→equalisers prods pbs
    fc .Finitely-complete.pullbacks = pbs

–

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)))