module Cat.Diagram.Pullback {β ββ²} (C : Precategory β ββ²) 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 (β β ββ²) 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 (β β ββ²) 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
Categories with all pullbacksπ
We also provide a helper module for working with categories that have all pullbacks.
has-pullbacks : Type _ has-pullbacks = β {A B X} (f : Hom A X) (g : Hom B X) β Pullback f g module Pullbacks (all-pullbacks : has-pullbacks) where 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 right 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 fβΊ g p2 f β P fβΊ