open import Cat.Functor.Equivalence open import Cat.Diagram.Pullback open import Cat.Diagram.Initial open import Cat.Functor.Adjoint open import Cat.Instances.Comma open import Cat.Instances.Slice open import Cat.Functor.Base open import Cat.Prelude import Cat.Reasoning 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.limiting {pβ' = dh .map β xpb.pβ} (pulll (dh .commutes) β xpb.square) dhβ² .commutes = ypb.pββlimiting
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ββlimiting β pullr ypb.pββlimiting β assoc _ _ _) (pulll zpb.pββlimiting β ypb.pββlimiting))) 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 _=>_
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.limiting {pβ' = id} {pβ' = obj .map} (idr _) dh .commutes = pb.pββlimiting Ξ£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ββlimiting) (pulll pb.pββlimiting) (pulll pb.pββlimiting β pullr pbβ².pββlimiting β id-comm) (pulll pb.pββlimiting β pbβ².pββlimiting β 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ββlimiting where module pb = Pullback (pullbacks (y .map) f) Ξ£fβ£f* .zig {A} = /-Hom-path pb.pββlimiting 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ββlimiting β pullr pbβ².pββlimiting β idr _) (pulll pb.pββlimiting β pbβ².pββlimiting))) where module pb = Pullback (pullbacks (B .map) f) module pbβ² = Pullback (pullbacks (f β pb.pβ) f)