module Cat.Diagram.Pullback where

Pullbacks🔗

A pullback $X \times_{Z} Y$ of $f : X \to Z$ and $g : Y \to Z$ is the product of $f$ and $g$ in the category $C / Z,$ the category of objects fibred over $Z .$ We note that the fibre of $X \times_{Z} Y$ over some element $x$ of $Z$ is the product of the fibres of $f$ and $g$ over $x;$ 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 $π_{1}$ and $π_{2}$ onto its factors; Since isn’t merely a product of $X$ and $Y,$ but rather of $X$ and $Y$ considered as objects over $Z$ 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 $P^{'},$ $X,$ $Y,$ $Z$ — it’s a bit bent) admits a unique factorisation that passes through $P;$ We can draw the whole situation as in the diagram below. Note the little corner on $P,$ 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

Kernel pairs🔗

The kernel pair of a morphism $f : X \to Y$ (if it exists) is the pullback of $f$ along itself. Intuitively, one should think of a kernel pair as a partition of $X$ induced by the preimage of $f .$

  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 $f$ 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 $u$ such that $p_{1} \circ u = id .$ We can construct such a $u$ 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 $f$ is a monomorphism, then its kernel pair always exists, and is given by $(id, id) .$

  monic→id-kernel-pair
    : ∀ {f : Hom X Y}
    → is-monic f
    → is-kernel-pair C id id f

Clearly, the square $f \circ id = f \circ id$ commutes, so the tricky bit will be constructing a universal morphism. If $f \circ p_{1} = f \circ p_{2}$ for some $p_{1}, p_{2} : P \to X,$ then we can simply use one of $p_{1}$ or $p_{2}$ for our universal map; the choice we make does not matter, as we can obtain $p_{1} = p_{2}$ from the fact that $f$ 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 $(id, id)$ is the kernel pair of $f,$ then $f$ is monic. Suppose that $f \circ g = f \circ h$ for some $g, h : A \to X,$ and note that both $g$ and $h$ are equal to the universal map obtained via the square $f \circ g = f \circ h .$

  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 $(p, p)$ is the kernel pair of $f$ for some $P : C, p : P \to X,$ then $(id, id)$ is also a kernel pair of $f .$

  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 $f \circ p_{1} = f \circ p_{2}$ for some $P^{'} : C, p_{1}, p_{2} : P^{'} \to X,$ 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 $p \circ u$ factorizes both $p_{1}$ and $p_{2};$ 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.

record Pullbacks {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ ℓ) where
  no-eta-equality
  open Cat.Reasoning C
  field
    Pb : ∀ {X Y Z} → Hom X Z → Hom Y Z → Ob
    p₁ : ∀ {X Y Z} (f : Hom X Z) (g : Hom Y Z) → Hom (Pb f g) X
    p₂ : ∀ {X Y Z} (f : Hom X Z) (g : Hom Y Z) → Hom (Pb f g) Y
    square
      : ∀ {X Y Z} {f : Hom X Z} {g : Hom Y Z}
      → f ∘ p₁ f g ≡ g ∘ p₂ f g
    pb
      : ∀ {P X Y Z} {f : Hom X Z} {g : Hom Y Z}
      → (p1 : Hom P X) (p2 : Hom P Y)
      → f ∘ p1 ≡ g ∘ p2
      → Hom P (Pb f g)
    p₁∘pb
      : ∀ {P X Y Z} {f : Hom X Z} {g : Hom Y Z}
      → {p1 : Hom P X} {p2 : Hom P Y}
      → {sq : f ∘ p1 ≡ g ∘ p2}
      → p₁ f g ∘ pb p1 p2 sq ≡ p1
    p₂∘pb
      : ∀ {P X Y Z} {f : Hom X Z} {g : Hom Y Z}
      → {p1 : Hom P X} {p2 : Hom P Y}
      → {sq : f ∘ p1 ≡ g ∘ p2}
      → p₂ f g ∘ pb p1 p2 sq ≡ p2
    pb-unique
      : ∀ {P X Y Z} {f : Hom X Z} {g : Hom Y Z}
      → {p1 : Hom P X} {p2 : Hom P Y}
      → {sq : f ∘ p1 ≡ g ∘ p2}
      → {other : Hom P (Pb f g)}
      → p₁ f g ∘ other ≡ p1
      → p₂ f g ∘ other ≡ p2
      → other ≡ pb p1 p2 sq

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 $f : A \to B$ as encoding the data of a family over $B$ (think of the special case where $A = Σ_{x : A} F (x),$ and $f = π_{1}),$ then we can think of pulling back $f$ along $g : X \to B$ as “the universal solution to making $f$ a family over $X,$ via $g$ ”. 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 $f$ 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⁺