open import Cat.Prelude 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.
limiting : β {Pβ²} {pβ' : Hom Pβ² X} {pβ' : Hom Pβ² Y} β f β pβ' β‘ g β pβ' β Hom Pβ² P pββlimiting : {p : f β pβ' β‘ g β pβ'} β pβ β limiting p β‘ pβ' pββlimiting : {p : f β pβ' β‘ g β pβ'} β pβ β limiting p β‘ pβ' unique : {p : f β pβ' β‘ g β pβ'} {lim' : Hom Pβ² P} β pβ β lim' β‘ pβ' β pβ β lim' β‘ pβ' β lim' β‘ limiting 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