Adjunction of pushforward and pullback in `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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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

source

@[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

source

@[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) ⋯

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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) ⋯ ⋯)

source

@[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

source

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)

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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

source

@[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✝

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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) ⋯ ⋯) ⋯ ⋯

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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) (A : P.Over Q Y) :

(mapPullbackAdj P Q f hPf hQf).counit.app A = Over.homMk (Limits.pullback.fst A.hom f) ⋯ ⋯

source

@[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) (A : P.Over Q X) :

(mapPullbackAdj P Q f hPf hQf).unit.app A = Over.homMk (Limits.pullback.lift (CategoryStruct.id A.left) A.hom ⋯) ⋯ ⋯

source

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

source

theorem CategoryTheory.MorphismProperty.isRightAdjoint_pullback {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.pullback P ⊤ f).IsRightAdjoint

source

def CategoryTheory.MorphismProperty.Under.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.Under Q Y) (P.Under Q X)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.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.fromPUnit Y) (Functor.id T) P ⊤ Q) :

((map Q hPf).obj X✝).hom = CategoryStruct.comp f X✝.hom

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.map_map_right {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.fromPUnit Y) (Functor.id T) P ⊤ Q} (f✝ : X✝ ⟶ Y✝) :

((map Q hPf).map f✝).right = (Comma.Hom.hom f✝).right

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.map_obj_right {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.fromPUnit Y) (Functor.id T) P ⊤ Q) :

((map Q hPf).obj X✝).right = X✝.right

source

theorem CategoryTheory.MorphismProperty.Under.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 hg).comp (map Q hf)

source

def CategoryTheory.MorphismProperty.Under.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 Under.map functors.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mapCongr_inv_app_right {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.Under Q Y) :

((mapCongr Q hfg hf).inv.app X✝).right = CategoryStruct.id X✝.right

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mapCongr_hom_app_right {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.Under Q Y) :

((mapCongr Q hfg hf).hom.app X✝).right = CategoryStruct.id X✝.right

source

def CategoryTheory.MorphismProperty.Under.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.Under Q X)

Under.map preserves identities.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mapId_inv_app_right {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.Under Q X) :

((mapId Q X f hf).inv.app X✝).right = CategoryStruct.id X✝.right

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.mapId_hom_app_right {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.Under Q X) :

((mapId Q X f hf).hom.app X✝).right = CategoryStruct.id X✝.right

source

def CategoryTheory.MorphismProperty.Under.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 hg).comp (map Q hf)

Under.map commutes with composition.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.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.Under Q Z) :

((mapComp Q hf hg fg hfg).hom.app X✝).left = CategoryStruct.id ((map Q ⋯).obj X✝).toComma.1

source

instance CategoryTheory.MorphismProperty.instHasPushoutHomDiscretePUnitOfHasPushoutsAlong {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] (A : P.Under Q X) :

Limits.HasPushout A.hom f

source

instance CategoryTheory.MorphismProperty.instHasPushoutInrHomDiscretePUnitOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) {X Y Z : T} (f : Y ⟶ X) (g : Z ⟶ Y) [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [P.IsStableUnderCobaseChangeAlong g] (A : P.Under Q Z) :

Limits.HasPushout (Limits.pushout.inr A.hom g) f

source

noncomputable def CategoryTheory.MorphismProperty.Under.pushout {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] :

Functor (P.Under Q X) (P.Under Q Y)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushout_obj_right {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (A : P.Under Q X) :

((pushout P Q f).obj A).right = Limits.pushout A.hom f

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushout_map_right {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] {A B : P.Under Q X} (g : A ⟶ B) :

((pushout P Q f).map g).right = Limits.pushout.desc (CategoryStruct.comp g.right (Limits.pushout.inl B.hom f)) (Limits.pushout.inr B.hom f) ⋯

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushout_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.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (A : P.Under Q X) :

((pushout P Q f).obj A).hom = Limits.pushout.inr A.hom f

source

noncomputable def CategoryTheory.MorphismProperty.Under.pushoutComp {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.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [Q.RespectsIso] [Q.IsStableUnderCobaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) :

pushout P Q fg ≅ (pushout P Q f).comp (pushout P Q g)

Under.pushout commutes with composition.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushoutComp_inv_app_right {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.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [Q.RespectsIso] [Q.IsStableUnderCobaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Under Q X) :

((pushoutComp f g fg hfg).inv.app X✝).right = CategoryStruct.comp (Limits.pushoutLeftPushoutInrIso X✝.hom f g).hom (Limits.pushout.map X✝.hom (CategoryStruct.comp f g) X✝.hom fg (CategoryStruct.id X✝.right) (CategoryStruct.id Z) (CategoryStruct.id X) ⋯ ⋯)

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushoutComp_hom_app_right {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.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [Q.RespectsIso] [Q.IsStableUnderCobaseChange] (fg : X ⟶ Z := CategoryStruct.comp f g) (hfg : fg = CategoryStruct.comp f g := by cat_disch) (X✝ : P.Under Q X) :

((pushoutComp f g fg hfg).hom.app X✝).right = CategoryStruct.comp (Limits.pushout.map X✝.hom fg X✝.hom (CategoryStruct.comp f g) (CategoryStruct.id X✝.right) (CategoryStruct.id Z) (CategoryStruct.id X) ⋯ ⋯) (Limits.pushoutLeftPushoutInrIso X✝.hom f g).inv

source

noncomputable def CategoryTheory.MorphismProperty.Under.pushoutCongr {T : Type u_1} [Category.{v_1, u_1} T] {P Q : MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] {g : X ⟶ Y} (h : f = g) :

pushout P Q f ≅ pushout P Q g

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushoutCongr_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.HasPushoutsAlong f] {g : X ⟶ Y} [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (h : f = g) (A : P.Under Q X) :

CategoryStruct.comp (Limits.pushout.inl A.hom f) ((pushoutCongr h).hom.app A).right = Limits.pushout.inl A.hom g

source

@[simp]

theorem CategoryTheory.MorphismProperty.Under.pushoutCongr_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.HasPushoutsAlong f] {g : X ⟶ Y} [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (h : f = g) (A : P.Under Q X) {Z : T} (h✝ : ((pushout P Q g).obj A).right ⟶ Z) :

CategoryStruct.comp (Limits.pushout.inl A.hom f) (CategoryStruct.comp ((pushoutCongr h).hom.app A).right h✝) = CategoryStruct.comp (Limits.pushout.inl A.hom g) h✝

source

noncomputable def CategoryTheory.MorphismProperty.Under.mapPushoutAdj {T : Type u_1} [Category.{v_1, u_1} T] (P Q : MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderCobaseChange] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.HasOfPrecompProperty Q] (hPf : P f) (hQf : Q f) :

pushout P Q f ⊣ map Q hPf

P.Under.pushout is left adjoint to P.Under.map if pushouts of morphisms satisfying P exist along f and are also in P, and f is in both P and Q.

Equations