module Cat.Diagram.Pullback where
Pullbacksπ
module _ {o β} (C : Precategory o β) where open Cat.Reasoning C private variable P' X Y Z : Ob h pβ' pβ' : Hom X Y
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)
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 (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
is-kernel-pairβepir : β {P} {p1 p2 : Hom P X} {f : Hom X Y} β is-kernel-pair C p1 p2 f β is-epic p2 is-kernel-pairβepir {p2 = p2} 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βΊ