Adjunction of pushforward and pullback in P.Over Q X

A morphism f : X ⟶ Y defines two functors:

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

These are adjoint under suitable assumptions on P and Q.

def CategoryTheory.MorphismProperty.Over.map {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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_hom {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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

@[simp]

theorem CategoryTheory.MorphismProperty.Over.map_obj_left {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.IsStableUnderComposition] (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

theorem CategoryTheory.MorphismProperty.Over.map_comp {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {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.mapComp {T : Type u_1} [Category.{u_2, u_1} T] {P : MorphismProperty T} (Q : MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] : map Q ⋯ ≅ (map Q hf).comp (map Q hg)

Over.map commutes with composition.

@[simp]

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

@[simp]

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

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

If P and Q are stable under base change and pullbacks exist in T, 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.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [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_hom {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] (A : P.Over Q Y) : ((pullback P Q f).obj A).hom = Limits.pullback.snd A.hom f

@[simp]

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

noncomputable def CategoryTheory.MorphismProperty.Over.pullbackComp {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : pullback P Q (CategoryStruct.comp f g) ≅ (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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : P.Over Q Z) : ((pullbackComp f g).inv.app X✝).left = (Limits.pullbackLeftPullbackSndIso X✝.hom g f).hom

@[simp]

theorem CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : P.Over Q Z) : ((pullbackComp f g).hom.app X✝).left = (Limits.pullbackLeftPullbackSndIso X✝.hom g f).inv

theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst {T : Type u_1} [Category.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (A : P.Over Q Z) : CategoryStruct.comp ((pullbackComp 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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f 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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f g : X ⟶ Y} (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.{u_2, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] [Limits.HasPullbacks T] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] {X Y : T} {f g : X ⟶ Y} (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.mapPullbackAdj {T : Type u_1} [Category.{u_2, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] [Limits.HasPullbacks T] [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 f satisfies P.