Adjunction of pushforward and pullback in P.Over Q X

Under suitable assumptions on P, Q and f, a morphism f : X ⟶ Y defines two functors:

• Over.map: post-composition with f
• Over.pullback: base-change along f

such that Over.map is the left adjoint to Over.pullback.

def CategoryTheory.MorphismProperty.Over.map {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) : Functor (P.Over Q X) (P.Over Q Y)

If P is stable under composition and f : X ⟶ Y satisfies P, this is the functor P.Over Q X ⥤ P.Over Q Y given by composing with f.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.map_obj_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) (X✝ : MorphismProperty.Comma (Functor.id T) (Functor.fromPUnit X) P Q ⊤) : ((map Q hPf).obj X✝).left = X✝.left

@[simp]

theorem CategoryTheory.MorphismProperty.Over.map_map_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) {X✝ Y✝ : MorphismProperty.Comma (Functor.id T) (Functor.fromPUnit X) P Q ⊤} (f✝ : X✝ ⟶ Y✝) : ((map Q hPf).map f✝).left = (Comma.Hom.hom f✝).left

@[simp]

theorem CategoryTheory.MorphismProperty.Over.map_obj_hom {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) (X✝ : MorphismProperty.Comma (Functor.id T) (Functor.fromPUnit X) P Q ⊤) : ((map Q hPf).obj X✝).hom = CategoryStruct.comp X✝.hom f

theorem CategoryTheory.MorphismProperty.Over.map_comp {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) : map Q ⋯ = (map Q hf).comp (map Q hg)

def CategoryTheory.MorphismProperty.Over.mapCongr {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) : map Q hf ≅ map Q ⋯

Promote an equality to an isomorphism of Over.map functors.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapCongr_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X✝ : P.Over Q X) : ((mapCongr Q hfg hf).hom.app X✝).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapCongr_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X✝ : P.Over Q X) : ((mapCongr Q hfg hf).inv.app X✝).left = CategoryStruct.id X✝.left

def CategoryTheory.MorphismProperty.Over.mapId {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryStruct.id X) (hf : f = CategoryStruct.id X := by cat_disch) : map Q ⋯ ≅ Functor.id (P.Over Q X)

Over.map preserves identities.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapId_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryStruct.id X) (hf : f = CategoryStruct.id X := by cat_disch) (X✝ : P.Over Q X) : ((mapId Q X f hf).inv.app X✝).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapId_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryStruct.id X) (hf : f = CategoryStruct.id X := by cat_disch) (X✝ : P.Over Q X) : ((mapId Q X f hf).hom.app X✝).left = CategoryStruct.id X✝.left

def CategoryTheory.MorphismProperty.Over.mapComp {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) : map Q ⋯ ≅ (map Q hf).comp (map Q hg)

Over.map commutes with composition.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapComp_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q X) : ((mapComp Q hf hg fg hfg).hom.app X✝).left = CategoryStruct.id X✝.left

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapComp_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q X) : ((mapComp Q hf hg fg hfg).inv.app X✝).left = CategoryStruct.id X✝.left

instance CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] (A : P.Over Q Y) : Limits.HasPullback A.hom f

instance CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [P.IsStableUnderBaseChangeAlong g] (A : P.Over Q Z) : Limits.HasPullback (Limits.pullback.snd A.hom g) f

noncomputable def CategoryTheory.MorphismProperty.Over.pullback {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] : Functor (P.Over Q Y) (P.Over Q X)

If P and Q are stable under base change and pullbacks along f exist for morphisms in P, this is the functor P.Over Q Y ⥤ P.Over Q X given by base change along f.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullback_map_left {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] {A B : P.Over Q Y} (g : A ⟶ B) : ((pullback P Q f).map g).left = Limits.pullback.lift (CategoryStruct.comp (Limits.pullback.fst A.hom f) g.left) (Limits.pullback.snd A.hom f) ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullback_obj_left {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) : ((pullback P Q f).obj A).left = Limits.pullback A.hom f

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullback_obj_hom {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) : ((pullback P Q f).obj A).hom = Limits.pullback.snd A.hom f

noncomputable def CategoryTheory.MorphismProperty.Over.pullbackComp {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) : pullback P Q fg ≅ (pullback P Q g).comp (pullback P Q f)

Over.pullback commutes with composition.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q Z) : ((pullbackComp f g fg hfg).inv.app X✝).left = CategoryStruct.comp (Limits.pullbackLeftPullbackSndIso X✝.hom g f).hom (Limits.pullback.map X✝.hom (CategoryStruct.comp f g) X✝.hom fg (CategoryStruct.id X✝.left) (CategoryStruct.id X) (CategoryStruct.id Z) ⋯ ⋯)

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Over Q Z) : ((pullbackComp f g fg hfg).hom.app X✝).left = CategoryStruct.comp (Limits.pullback.map X✝.hom fg X✝.hom (CategoryStruct.comp f g) (CategoryStruct.id X✝.left) (CategoryStruct.id X) (CategoryStruct.id Z) ⋯ ⋯) (Limits.pullbackLeftPullbackSndIso X✝.hom g f).inv

theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] [Q.RespectsIso] [Q.IsStableUnderBaseChange] (A : P.Over Q Z) : CategoryStruct.comp ((pullbackComp f g (CategoryStruct.comp f g) ⋯).hom.app A).left (CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.snd A.hom g) f) (Limits.pullback.fst A.hom g)) = Limits.pullback.fst A.hom (CategoryStruct.comp f g)

noncomputable def CategoryTheory.MorphismProperty.Over.pullbackCongr {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] {g : X ⟶ Y} (h : f = g) : pullback P Q f ≅ pullback P Q g

If f = g, then base change along f is naturally isomorphic to base change along g.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPullbacksAlong f] {g : X ⟶ Y} [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (h : f = g) (A : P.Over Q Y) : CategoryStruct.comp ((pullbackCongr h).hom.app A).left (Limits.pullback.fst A.hom g) = Limits.pullback.fst A.hom f

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst_assoc {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPullbacksAlong f] {g : X ⟶ Y} [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] (h : f = g) (A : P.Over Q Y) {Z : T} (h✝ : A.left ⟶ Z) : CategoryStruct.comp ((pullbackCongr h).hom.app A).left (CategoryStruct.comp (Limits.pullback.fst A.hom g) h✝) = CategoryStruct.comp (Limits.pullback.fst A.hom f) h✝

noncomputable def CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} (f : X ⟶ Y) (hPf : P f) (hQf : Q f) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [Q.IsStableUnderBaseChange] [Limits.HasPullbacks T] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : CategoryStruct.comp f g = fg := by cat_disch) : (pullback P Q fg).comp (map Q hPf) ⟶ pullback P Q g

The natural map between pullback functors induced by pullback.map.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback_app {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} (f : X ⟶ Y) (hPf : P f) (hQf : Q f) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] [P.IsStableUnderBaseChangeAlong g] [Q.IsStableUnderBaseChange] [Limits.HasPullbacks T] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : CategoryStruct.comp f g = fg := by cat_disch) (A : P.Over Q Z) : (pullbackMapHomPullback f hPf hQf g fg hfg).app A = Over.homMk (Limits.pullback.map A.hom fg A.hom g (CategoryStruct.id A.left) f (CategoryStruct.id Z) ⋯ ⋯) ⋯ ⋯

noncomputable def CategoryTheory.MorphismProperty.Over.mapPullbackAdj {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderBaseChange] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) : map Q hPf ⊣ pullback P Q f

P.Over.map is left adjoint to P.Over.pullback if pullbacks of morphisms satisfying P exist along f and are also in P, and f is in both P and Q.

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderBaseChange] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) (X✝ : P.Over Q X) : (mapPullbackAdj P Q f hPf hQf).unit.app X✝ = Over.homMk (Limits.pullback.lift (CategoryStruct.id X✝.left) X✝.hom ⋯) ⋯ ⋯

@[simp]

theorem CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderBaseChange] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) (Y✝ : P.Over Q Y) : (mapPullbackAdj P Q f hPf hQf).counit.app Y✝ = Over.homMk (Limits.pullback.fst Y✝.hom f) ⋯ ⋯

instance CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong {T : Type u_1} [Category.{v_1, u_1} T] (P : MorphismProperty T) {X Y : T} [P.IsStableUnderComposition] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] (hPf : P f) : (Over.map ⊤ hPf).IsLeftAdjoint