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)
pullback-univ : β {O} β Hom O P β (Ξ£ (Hom O X) Ξ» h β Ξ£ (Hom O Y) Ξ» h' β f β h β‘ g β h') pullback-univ .fst h = pβ β h , pβ β h , extendl square pullback-univ .snd = is-isoβis-equiv Ξ» where .is-iso.inv (f , g , Ξ±) β universal Ξ± .is-iso.rinv x β Ξ£-pathp pββuniversal $ Ξ£-prop-pathp (Ξ» _ _ β hlevel 1) pββuniversal .is-iso.linv x β sym (unique refl refl)
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βΊ