module Cat.Displayed.Instances.Pullback {o β o' β' o'' β''} {X : Precategory o β} {B : Precategory o' β'} (F : Functor X B) (E : Displayed B o'' β'') where
Pullback of a displayed categoryπ
If we have a category displayed over , then a functor defines a (contravariant) βchange-of-baseβ action, resulting in a category displayed over .
private module X = Precategory X module B = Precategory B module E = Displayed E open Functor F open Displayed open Dr E
The reason for this contravariance is the following: A category displayed over must have a -indexed space of objects; But our category has a -indexed space of objects. Fortunately, gives us a map which allows us to convert our -indices to -indices. The same goes for indexing the displayed -sets.
Change-of-base : Displayed X o'' β'' Change-of-base .Ob[_] x = E.Ob[ Fβ x ] Change-of-base .Hom[_] f x y = E.Hom[ Fβ f ] x y Change-of-base .Hom[_]-set f = E.Hom[ Fβ f ]-set Change-of-base .id' = hom[ sym F-id ] E.id' Change-of-base ._β'_ f' g' = hom[ sym (F-β _ _) ] (f' E.β' g')
Proving that the pullback is indeed a displayed category is a bit trickier than it might seem β we must adjust the identity and composites in by the paths witnessing functoriality of , and this really throws a spanner in the works β but the handy displayed category reasoning combinators are here to help.
Change-of-base .idr' {f = f} f' = to-pathp $ hom[] (hom[ F-β _ _ ]β» (f' E.β' hom[ F-id ]β» _)) β‘β¨ hom[]β©β¨ smashr _ _ β©β‘ hom[] (hom[] (f' E.β' E.id')) β‘β¨ Ds.disp! E β©β‘ f' β Change-of-base .idl' f' = to-pathp $ hom[] (hom[ F-β _ _ ]β» (hom[ F-id ]β» _ E.β' f')) β‘β¨ hom[]β©β¨ smashl _ _ β©β‘ hom[] (hom[] (E.id' E.β' f')) β‘β¨ Ds.disp! E β©β‘ f' β Change-of-base .assoc' f' g' h' = to-pathp $ hom[ ap Fβ _ ] (hom[ F-β _ _ ]β» (f' E.β' hom[ F-β _ _ ]β» (g' E.β' h'))) β‘β¨ hom[]β©β¨ smashr _ _ β©β‘ hom[] (hom[] (f' E.β' g' E.β' h')) β‘β¨ Ds.disp! E β©β‘ hom[ sym (F-β _ _) ] (hom[ sym (F-β _ _) ] (f' E.β' g') E.β' h') β
As a fibrationπ
If
is a cartesian
fibration, then the base change of
along
is also cartesian. To prove this, observe that the object and hom spaces
of Change-of-base
contain the same
data as
,
just restricted to objects and morphisms in the image of
.
This means that we still have cartesian lifts of all morphisms in
:
we just have to perform the lifting of
.
Change-of-base-fibration : Cartesian-fibration E β Cartesian-fibration Change-of-base Change-of-base-fibration fib .Cartesian-fibration.has-lift f FY' = cart-lift where open Cartesian-lift (Cartesian-fibration.has-lift fib (Fβ f) FY') cart-lift : Cartesian-lift Change-of-base f FY' cart-lift .Cartesian-lift.x' = x' cart-lift .Cartesian-lift.lifting = lifting cart-lift .Cartesian-lift.cartesian .is-cartesian.universal m h' = universal (F .Functor.Fβ m) (hom[ F-β f m ] h') cart-lift .Cartesian-lift.cartesian .is-cartesian.commutes m h' = hom[ F-β f m ]β» (lifting E.β' universal (Fβ m) (hom[ F-β f m ] h')) β‘β¨ ap hom[ F-β f m ]β» (commutes _ _) β©β‘ hom[ F-β f m ]β» (hom[ F-β f m ] h') β‘β¨ Ds.disp! E β©β‘ h' β cart-lift .Cartesian-lift.cartesian .is-cartesian.unique {m = m} {h' = h'} m' p = unique m' $ lifting E.β' m' β‘β¨ Ds.disp! E β©β‘ hom[ F-β f m ] (hom[ F-β f m ]β» (lifting E.β' m')) β‘β¨ ap hom[ F-β f m ] p β©β‘ hom[ F-β f m ] h' β