module Cat.Functor.Pullback {o β} {C : Precategory o β} where
Base changeπ
Let be a category with all pullbacks, and a morphism in . Then we have a functor , called the base change, where the action on objects is given by pulling back along .
On objects, the functor maps as in the diagram below. Itβs a bit busy, so look at it in parts: On the left we have the object of , and on the right we have the whole pullback diagram, showing how the parts fit together. The actual object of the functor gives is the vertical arrow .
module _ (pullbacks : β {X Y Z} f g β Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where Base-change : Functor (Slice C X) (Slice C Y) Base-change .Fβ x = ob where ob : /-Obj Y ob .domain = pullbacks (x .map) f .apex ob .map = pullbacks (x .map) f .pβ
On morphisms, we use the universal property of the pullback to obtain a map , by observing that the square diagram below is a cone over .
Base-change .Fβ {x} {y} dh = dhβ² where module ypb = Pullback (pullbacks (y .map) f) module xpb = Pullback (pullbacks (x .map) f) dhβ² : /-Hom _ _ dhβ² .map = ypb.universal {pβ' = dh .map β xpb.pβ} (pulll (dh .commutes) β xpb.square) dhβ² .commutes = ypb.pββuniversal
The properties of pullbacks also guarantee that this operation is functorial, but the details are not particularly enlightening.
Base-change .F-id {x} = /-Hom-path (sym (xpb.unique id-comm (idr _))) where module xpb = Pullback (pullbacks (x .map) f) Base-change .F-β {x} {y} {z} am bm = /-Hom-path (sym (zpb.unique (pulll zpb.pββuniversal β pullr ypb.pββuniversal β assoc _ _ _) (pulll zpb.pββuniversal β ypb.pββuniversal))) where module ypb = Pullback (pullbacks (y .map) f) module zpb = Pullback (pullbacks (z .map) f)
Propertiesπ
The base change functor is a right adjoint. We construct the left adjoint directly, then give the unit and counit, and finally prove the triangle identities.
The left adjoint, called dependent sum and written , is given on objects by precomposition with , and on morphisms by what is essentially the identity function β only the witness of commutativity must change.
module _ {X Y : Ob} (f : Hom Y X) where Ξ£f : Functor (Slice C Y) (Slice C X) Ξ£f .Fβ o = cut (f β o .map) Ξ£f .Fβ dh = record { map = dh .map ; commutes = pullr (dh .commutes) } Ξ£f .F-id = /-Hom-path refl Ξ£f .F-β f g = /-Hom-path refl open _β£_ open _=>_
Ξ£-iso-equiv : {X Y : Ob} {f : Hom Y X} β Cat.Reasoning.is-invertible C f β is-equivalence (Ξ£f f) Ξ£-iso-equiv {X} {f = f} isom = ff+split-esoβis-equivalence Ξ£-ff Ξ£-seso where module Sl = Cat.Reasoning (Slice C X) module isom = is-invertible isom func = Ξ£f f Ξ£-ff : β {x y} β is-equiv (func .Fβ {x} {y}) Ξ£-ff = is-isoβis-equiv (iso βinv (Ξ» x β /-Hom-path refl) Ξ» x β /-Hom-path refl) where βinv : /-Hom _ _ β /-Hom _ _ βinv o .map = o .map βinv o .commutes = invertibleβmonic isom _ _ (assoc _ _ _ β o .commutes) Ξ£-seso : is-split-eso func Ξ£-seso y = cut (isom.inv β y .map) , Sl.make-iso into fromβ² (/-Hom-path (eliml refl)) (/-Hom-path (eliml refl)) where into : /-Hom _ _ into .map = id into .commutes = id-comm β sym (pulll isom.invl) fromβ² : /-Hom _ _ fromβ² .map = id fromβ² .commutes = elimr refl β cancell isom.invl
The adjunction unit and counit are given by the universal properties of pullbacks. β οΈ WIP β οΈ
module _ (pullbacks : β {X Y Z} f g β Pullback C {X} {Y} {Z} f g) {X Y : Ob} (f : Hom Y X) where open _β£_ open _=>_ Ξ£fβ£f* : Ξ£f f β£ Base-change pullbacks f Ξ£fβ£f* .unit .Ξ· obj = dh where module pb = Pullback (pullbacks (f β obj .map) f) dh : /-Hom _ _ dh .map = pb.universal {pβ' = id} {pβ' = obj .map} (idr _) dh .commutes = pb.pββuniversal Ξ£fβ£f* .unit .is-natural x y g = /-Hom-path (pb.uniqueβ {p = (f β y .map) β id β g .map β‘β¨ cat! C β©β‘ f β y .map β g .map β} (pulll pb.pββuniversal) (pulll pb.pββuniversal) (pulll pb.pββuniversal β pullr pbβ².pββuniversal β id-comm) (pulll pb.pββuniversal β pbβ².pββuniversal β sym (g .commutes))) where module pb = Pullback (pullbacks (f β y .map) f) module pbβ² = Pullback (pullbacks (f β x .map) f) Ξ£fβ£f* .counit .Ξ· obj = dh where module pb = Pullback (pullbacks (obj .map) f) dh : /-Hom _ _ dh .map = pb.pβ dh .commutes = pb.square Ξ£fβ£f* .counit .is-natural x y g = /-Hom-path pb.pββuniversal where module pb = Pullback (pullbacks (y .map) f) Ξ£fβ£f* .zig {A} = /-Hom-path pb.pββuniversal where module pb = Pullback (pullbacks (f β A .map) f) Ξ£fβ£f* .zag {B} = /-Hom-path (sym (pb.uniqueβ {p = pb.square} (idr _) (idr _) (pulll pb.pββuniversal β pullr pbβ².pββuniversal β idr _) (pulll pb.pββuniversal β pbβ².pββuniversal))) where module pb = Pullback (pullbacks (B .map) f) module pbβ² = Pullback (pullbacks (f β pb.pβ) f)