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

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 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 be a (the) product of and with its projections called and Letting be a cospan, if the composites and have an equaliser then the square

is a pullback. Now, that description is almost entirely abstract-nonsensical, because (for generality) we do not use any β€œcanonical” products or equalisers If we work slightly more concretely, then this can be read as building the pullback as the largest subobject of where agree. In particular, the pullback we want is the object 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 and note that we can factor any pair of arrows and through the Cartesian product and use the universal property of equalisers to factor that as a unique arrow

    pb .universal {p₁' = p₁'} {pβ‚‚' = pβ‚‚'} p =
      eq.universal {e' = pr.⟨ p₁' , pβ‚‚' ⟩pr.} (
        (f ∘ p1) ∘ pr.⟨ p₁' , pβ‚‚' ⟩pr. β‰‘βŸ¨ pullr pr.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
        f ∘ p₁'                     β‰‘βŸ¨ p βŸ©β‰‘
        g ∘ pβ‚‚'                     β‰‘Λ˜βŸ¨ pullr pr.Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘Λ˜
        (g ∘ p2) ∘ pr.⟨ p₁' , pβ‚‚' ⟩pr. ∎
      )
    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
    β†’ (βˆ€ 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.Ο€β‚βˆ˜βŸ¨βŸ© = Pb.pβ‚βˆ˜universal
    prod .is-product.Ο€β‚‚βˆ˜βŸ¨βŸ© = Pb.pβ‚‚βˆ˜universal
    prod .is-product.unique 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 for some We can consider the two sides of this equation as a single map The equation is solved where this pairing map equals some 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, and become equal. Here’s where we use the fact that pullback squares, well, commute: We know that is and that (since the square above is a pullback).

But both projections out of are equal, so we can apply commutativity of the square above again to conclude that

      eq : Equaliser C f g
      eq .apex = Pb.apex
      eq .equ = Pb.pβ‚‚
      eq .has-is-eq .equal =
        f ∘ Pb.pβ‚‚               β‰‘Λ˜βŸ¨ pulll Bb.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘Λ˜
        Bb.π₁ ∘ ⟨f,g⟩ ∘ Pb.pβ‚‚   β‰‘βŸ¨ ap (Bb.π₁ ∘_) (sym Pb.square) βŸ©β‰‘
        Bb.π₁ ∘ ⟨id,id⟩ ∘ Pb.p₁ β‰‘βŸ¨ pulll Bb.Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ sym (pulll Bb.Ο€β‚‚βˆ˜βŸ¨βŸ©) βŸ©β‰‘
        Bb.Ο€β‚‚ ∘ ⟨id,id⟩ ∘ Pb.p₁ β‰‘βŸ¨ ap (Bb.Ο€β‚‚ ∘_) Pb.square βŸ©β‰‘
        Bb.Ο€β‚‚ ∘ ⟨f,g⟩ ∘ Pb.pβ‚‚   β‰‘βŸ¨ pulll Bb.Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
        g ∘ Pb.pβ‚‚               ∎

We must now show that if is another map which equalises and then it fits into a commutative diagram like the one below, so that we may conclude the dashed arrow 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 in our pullback diagram is indeed the equaliser of and

      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.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
            f ∘ e'                     β‰‘Λ˜βŸ¨ pulll Bb.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘Λ˜
            Bb.π₁ ∘ ⟨f,g⟩ ∘ e'         ∎

          p2 : Bb.Ο€β‚‚ ∘ ⟨id,id⟩ ∘ f ∘ e' ≑ Bb.Ο€β‚‚ ∘ ⟨f,g⟩ ∘ e'
          p2 =
            Bb.Ο€β‚‚ ∘ ⟨id,id⟩ ∘ f ∘ e'   β‰‘βŸ¨ cancell Bb.Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
            f ∘ e'                     β‰‘βŸ¨ p βŸ©β‰‘
            g ∘ e'                     β‰‘Λ˜βŸ¨ pulll Bb.Ο€β‚‚βˆ˜βŸ¨βŸ© βŸ©β‰‘Λ˜
            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.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
            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.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
            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 can be identified with pullbacks if has a terminal object, then a lex functor 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 being a monomorphism is equivalent to certain squares being pullbacks, a lex functor 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)))