module Cat.Diagram.Pullback where

PullbacksπŸ”—

A pullback of and is the product of and in the category the category of objects fibred over We note that the fibre of over some element of is the product of the fibres of and over Hence the pullback is also called the fibred product.

  record is-pullback {P} (p₁ : Hom P X) (f : Hom X Z) (pβ‚‚ : Hom P Y) (g : Hom Y Z)
    : Type (o βŠ” β„“) where

    no-eta-equality
    field
      square   : f ∘ p₁ ≑ g ∘ pβ‚‚

The concrete incarnation of the abstract nonsense above is that a pullback turns out to be a universal square like the one below. Since it is a product, it comes equipped with projections and onto its factors; Since isn’t merely a product of and but rather of and considered as objects over in a specified way, overall square has to commute.

      universal : βˆ€ {P'} {p₁' : Hom P' X} {pβ‚‚' : Hom P' Y}
               β†’ f ∘ p₁' ≑ g ∘ pβ‚‚' β†’ Hom P' P
      pβ‚βˆ˜universal : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} β†’ p₁ ∘ universal p ≑ p₁'
      pβ‚‚βˆ˜universal : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} β†’ pβ‚‚ ∘ universal p ≑ pβ‚‚'

      unique : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} {lim' : Hom P' P}
             β†’ p₁ ∘ lim' ≑ p₁'
             β†’ pβ‚‚ ∘ lim' ≑ pβ‚‚'
             β†’ lim' ≑ universal p

    uniqueβ‚‚
      : {p : f ∘ p₁' ≑ g ∘ pβ‚‚'} {lim' lim'' : Hom P' P}
      β†’ p₁ ∘ lim' ≑ p₁' β†’ pβ‚‚ ∘ lim' ≑ pβ‚‚'
      β†’ p₁ ∘ lim'' ≑ p₁' β†’ pβ‚‚ ∘ lim'' ≑ pβ‚‚'
      β†’ lim' ≑ lim''
    uniqueβ‚‚ {p = o} p q r s = unique {p = o} p q βˆ™ sym (unique r s)

By universal, we mean that any other β€œsquare” (here the second β€œsquare” has corners β€” it’s a bit bent) admits a unique factorisation that passes through We can draw the whole situation as in the diagram below. Note the little corner on indicating that the square is a pullback.

We provide a convenient packaging of the pullback and the projection maps:

  record Pullback {X Y Z} (f : Hom X Z) (g : Hom Y Z) : Type (o βŠ” β„“) where
    no-eta-equality
    field
      {apex} : Ob
      p₁ : Hom apex X
      pβ‚‚ : Hom apex Y
      has-is-pb : is-pullback p₁ f pβ‚‚ g

    open is-pullback has-is-pb public
module _ {o β„“} {C : Precategory o β„“} where
  open Cat.Reasoning C
  private variable
    P' X Y Z : Ob
    h p₁' pβ‚‚' : Hom X Y

  is-pullback-is-prop : βˆ€ {P} {p₁ : Hom P X} {f : Hom X Z} {pβ‚‚ : Hom P Y} {g : Hom Y Z} β†’ is-prop (is-pullback C p₁ f pβ‚‚ g)
  is-pullback-is-prop {X = X} {Y = Y} {p₁ = p₁} {f} {pβ‚‚} {g} x y = q where
    open is-pullback
    p : Path (βˆ€ {P'} {p₁' : Hom P' X} {pβ‚‚' : Hom P' Y} β†’ f ∘ p₁' ≑ g ∘ pβ‚‚' β†’ _) (x .universal) (y .universal)
    p i sq = y .unique {p = sq} (x .pβ‚βˆ˜universal {p = sq}) (x .pβ‚‚βˆ˜universal) i
    q : x ≑ y
    q i .square = Hom-set _ _ _ _ (x .square) (y .square) i
    q i .universal = p i
    q i .pβ‚βˆ˜universal {p₁' = p₁'} {p = sq} = is-propβ†’pathp (Ξ» i β†’ Hom-set _ _ (p₁ ∘ p i sq) p₁') (x .pβ‚βˆ˜universal) (y .pβ‚βˆ˜universal) i
    q i .pβ‚‚βˆ˜universal {p = sq} = is-propβ†’pathp (Ξ» i β†’ Hom-set _ _ (pβ‚‚ ∘ p i sq) _) (x .pβ‚‚βˆ˜universal) (y .pβ‚‚βˆ˜universal) i
    q i .unique {p = sq} {lim' = lim'} c₁ cβ‚‚ = is-propβ†’pathp (Ξ» i β†’ Hom-set _ _ lim' (p i sq)) (x .unique c₁ cβ‚‚) (y .unique c₁ cβ‚‚) i

  instance
    H-Level-is-pullback : βˆ€ {P} {p₁ : Hom P X} {f : Hom X Z} {pβ‚‚ : Hom P Y} {g : Hom Y Z} {n} β†’ H-Level (is-pullback C p₁ f pβ‚‚ g) (suc n)
    H-Level-is-pullback = prop-instance is-pullback-is-prop

Kernel pairsπŸ”—

The kernel pair of a morphism (if it exists) is the pullback of along itself. Intuitively, one should think of a kernel pair as a partition of induced by the preimage of

  is-kernel-pair : βˆ€ {P X Y} β†’ Hom P X β†’ Hom P X β†’ Hom X Y β†’ Type _
  is-kernel-pair p1 p2 f = is-pullback C p1 f p2 f

Note that each of the projections out of the kernel pair of are epimorphisms. Without loss of generality, we will focus our attention on the first projection.

  is-kernel-pair→epil
    : βˆ€ {p1 p2 : Hom P X} {f : Hom X Y}
    β†’ is-kernel-pair C p1 p2 f
    β†’ is-epic p1

Recall that a morphism is epic if it has a section; that is, some morphism such that We can construct such a by applying the universal property of the pullback to the following diagram.

  is-kernel-pair→epil {p1 = p1} is-kp =
    has-section→epic $
    make-section
      (universal refl)
      pβ‚βˆ˜universal
    where open is-pullback is-kp

If is a monomorphism, then its kernel pair always exists, and is given by

  monic→id-kernel-pair
    : βˆ€ {f : Hom X Y}
    β†’ is-monic f
    β†’ is-kernel-pair C id id f

Clearly, the square commutes, so the tricky bit will be constructing a universal morphism. If for some then we can simply use one of or for our universal map; the choice we make does not matter, as we can obtain from the fact that is monic! The rest of the universal property follows directly from this lovely little observation.

  monic→id-kernel-pair {f = f} f-monic = id-kp where
    open is-pullback

    id-kp : is-kernel-pair C id id f
    id-kp .square = refl
    id-kp .universal {p₁' = p₁'} _ = p₁'
    id-kp .pβ‚βˆ˜universal = idl _
    id-kp .pβ‚‚βˆ˜universal {p = p} = idl _ βˆ™ f-monic _ _ p
    id-kp .unique p q = sym (idl _) βˆ™ p

Conversely, if is the kernel pair of then is monic. Suppose that for some and note that both and are equal to the universal map obtained via the square

  id-kernel-pair→monic
    : βˆ€ {f : Hom X Y}
    β†’ is-kernel-pair C id id f
    β†’ is-monic f
  id-kernel-pair→monic {f = f} id-kp g h p =
    g                β‰‘Λ˜βŸ¨ pβ‚βˆ˜universal βŸ©β‰‘Λ˜
    id ∘ universal p β‰‘βŸ¨ pβ‚‚βˆ˜universal βŸ©β‰‘
    h                ∎
    where open is-pullback id-kp

We can strengthen this result by noticing that if is the kernel pair of for some then is also a kernel pair of

  same-kernel-pair→id-kernel-pair
    : βˆ€ {P} {p : Hom P X} {f : Hom X Y}
    β†’ is-kernel-pair C p p f
    β†’ is-kernel-pair C id id f

As usual, the difficulty is constructing the universal map. Suppose that for some as in the following diagram:

This diagram is conspicuously missing a morphism, so let’s fill it in by using the universal property of the kernel pair.

Next, note that factorizes both and moreover, it is the unique such map!

  same-kernel-pair→id-kernel-pair {p = p} {f = f} p-kp = id-kp where
    open is-pullback

    id-kp : is-kernel-pair C id id f
    id-kp .square = refl
    id-kp .universal q = p ∘ p-kp .universal q
    id-kp .pβ‚βˆ˜universal {p = q} = idl _ βˆ™ p-kp .pβ‚βˆ˜universal
    id-kp .pβ‚‚βˆ˜universal {p = q} = idl _ βˆ™ p-kp .pβ‚‚βˆ˜universal
    id-kp .unique q r = (sym (idl _)) βˆ™ q βˆ™ sym (p-kp .pβ‚βˆ˜universal)

Categories with all pullbacksπŸ”—

We also provide a helper module for working with categories that have all pullbacks.

has-pullbacks : βˆ€ {o β„“} β†’ Precategory o β„“ β†’ Type _
has-pullbacks C = βˆ€ {A B X} (f : Hom A X) (g : Hom B X) β†’ Pullback C f g
  where open Precategory C

module Pullbacks
  {o β„“}
  (C : Precategory o β„“)
  (all-pullbacks : has-pullbacks  C)
  where
  open Precategory C
  module pullback {x y z} (f : Hom x z) (g : Hom y z) =
    Pullback (all-pullbacks f g)

  Pb : βˆ€ {x y z} β†’ Hom x z β†’ Hom y z β†’ Ob
  Pb = pullback.apex

StabilityπŸ”—

Pullbacks, in addition to their nature as limits, serve as the way of β€œchanging the base” of a family of objects: if we think of an arrow as encoding the data of a family over (think of the special case where and then we can think of pulling back along as β€œthe universal solution to making a family over via ”. One way of making this intuition formal is through the fundamental fibration of a category with pullbacks.

In that framing, there is a canonical choice for β€œthe” pullback of an arrow along another: We put the arrow we want to pullback on the right side of the diagram, and the pullback is the left arrow. Using the type is-pullback defined above, the arrow which results from pulling back is adjacent to the adjustment: is-pullback f⁺ g _ f. To help keep this straight, we define what it means for a class of arrows to be stable under pullback: If f has a given property, then so does f⁺, for any pullback of f.

  is-pullback-stable
    : βˆ€ {β„“'} β†’ (βˆ€ {a b} β†’ Hom a b β†’ Type β„“') β†’ Type _
  is-pullback-stable P =
    βˆ€ {p A B X} (f : Hom A B) (g : Hom X B) {f⁺ : Hom p X} {p2}
    β†’ P f β†’ is-pullback C f⁺ g p2 f β†’ P f⁺