Descent of morphism properties

Given morphism properties P and Q we say that P descends along Q (P.DescendsAlong Q), if whenever Q holds for X ⟶ Z, P holds for X ×[Z] Y ⟶ X implies P holds for Y ⟶ Z. Dually, we define P.CodescendsAlong Q.

class CategoryTheory.MorphismProperty.DescendsAlong {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) : Prop

P descends along Q if whenever Q holds for X ⟶ Z, P holds for X ×[Z] Y ⟶ X implies P holds for Y ⟶ Z.

• of_isPullback {A X Y Z : C} {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} : IsPullback fst snd f g → Q f → P fst → P g

theorem CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {A X Y Z : C} {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} [P.DescendsAlong Q] (h : IsPullback fst snd f g) (hf : Q f) (hfst : P fst) : P g

theorem CategoryTheory.MorphismProperty.iff_of_isPullback {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {A X Y Z : C} {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q] (h : IsPullback fst snd f g) (hf : Q f) : P fst ↔ P g

theorem CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [P.DescendsAlong Q] [Limits.HasPullback f g] (hf : Q f) (hfst : P (Limits.pullback.fst f g)) : P g

theorem CategoryTheory.MorphismProperty.pullback_fst_iff {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q] [Limits.HasPullback f g] (hf : Q f) : P (Limits.pullback.fst f g) ↔ P g

theorem CategoryTheory.MorphismProperty.of_pullback_snd_of_descendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [P.DescendsAlong Q] [Limits.HasPullback f g] (hg : Q g) (hsnd : P (Limits.pullback.snd f g)) : P f

theorem CategoryTheory.MorphismProperty.pullback_snd_iff {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q] [Limits.HasPullback f g] (hg : Q g) : P (Limits.pullback.snd f g) ↔ P f

instance CategoryTheory.MorphismProperty.DescendsAlong.top {C : Type u_1} [Category.{v_1, u_1} C] {Q : MorphismProperty C} : ⊤.DescendsAlong Q

instance CategoryTheory.MorphismProperty.DescendsAlong.inf {C : Type u_1} [Category.{v_1, u_1} C] {P Q W : MorphismProperty C} [P.DescendsAlong Q] [W.DescendsAlong Q] : (P ⊓ W).DescendsAlong Q

theorem CategoryTheory.MorphismProperty.DescendsAlong.of_le {C : Type u_1} [Category.{v_1, u_1} C] {P Q W : MorphismProperty C} [P.DescendsAlong Q] (hle : W ≤ Q) : P.DescendsAlong W

theorem CategoryTheory.MorphismProperty.DescendsAlong.mk' {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} [P.RespectsIso] (H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : Limits.HasPullback f g], Q f → P (Limits.pullback.fst f g) → P g) : P.DescendsAlong Q

Alternative constructor for CodescendsAlong using HasPullback.

instance CategoryTheory.MorphismProperty.instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} [Q.IsStableUnderBaseChange] [P.HasOfPrecompProperty Q] [P.RespectsRight Q] : P.DescendsAlong Q

instance CategoryTheory.MorphismProperty.instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] (P Q : MorphismProperty C) [P.DescendsAlong Q] [P.RespectsIso] [Q.IsStableUnderBaseChange] : P.diagonal.DescendsAlong Q

If P descends along Q, then P.diagonal descends along Q.

theorem CategoryTheory.MorphismProperty.eq_of_isomorphisms_descendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [(isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange] [Limits.HasEqualizers C] [Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) (hv : P v) (H : Limits.pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯ = Limits.pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) : f = g

theorem CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [(isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange] [Limits.HasPullbacks C] [Limits.HasEqualizers C] {S T : C} {f : T ⟶ S} (hf : P f) : (Over.pullback f).Faithful

@[deprecated CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendsAlong (since := "2026-10-08")]

theorem CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [(isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange] [Limits.HasPullbacks C] [Limits.HasEqualizers C] {S T : C} {f : T ⟶ S} (hf : P f) : (Over.pullback f).Faithful

Alias of CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendsAlong.

class CategoryTheory.MorphismProperty.CodescendsAlong {C : Type u_1} [Category.{v_1, u_1} C] (P Q : MorphismProperty C) : Prop

P codescends along Q if whenever Q holds for Z ⟶ X, P holds for X ⟶ X ∐[Z] Y implies P holds for Z ⟶ Y.

• of_isPushout {Z X Y A : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} : IsPushout f g inl inr → Q f → P inl → P g

theorem CategoryTheory.MorphismProperty.of_isPushout_of_codescendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y A : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} [P.CodescendsAlong Q] (h : IsPushout f g inl inr) (hf : Q f) (hinl : P inl) : P g

theorem CategoryTheory.MorphismProperty.iff_of_isPushout {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y A : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] (h : IsPushout f g inl inr) (hg : Q f) : P inl ↔ P g

theorem CategoryTheory.MorphismProperty.of_pushout_inl_of_codescendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} [P.CodescendsAlong Q] [Limits.HasPushout f g] (hf : Q f) (hinl : P (Limits.pushout.inl f g)) : P g

theorem CategoryTheory.MorphismProperty.pushout_inl_iff {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] [Limits.HasPushout f g] (hf : Q f) : P (Limits.pushout.inl f g) ↔ P g

theorem CategoryTheory.MorphismProperty.of_pushout_inr_of_codescendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} [P.CodescendsAlong Q] [Limits.HasPushout f g] (hg : Q g) (hinr : P (Limits.pushout.inr f g)) : P f

@[deprecated CategoryTheory.MorphismProperty.of_pushout_inr_of_codescendsAlong (since := "2026-10-08")]

theorem CategoryTheory.MorphismProperty.of_pushout_inr_of_descendsAlong {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} [P.CodescendsAlong Q] [Limits.HasPushout f g] (hg : Q g) (hinr : P (Limits.pushout.inr f g)) : P f

Alias of CategoryTheory.MorphismProperty.of_pushout_inr_of_codescendsAlong.

theorem CategoryTheory.MorphismProperty.pushout_inr_iff {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] [Limits.HasPushout f g] (hg : Q g) : P (Limits.pushout.inr f g) ↔ P f

theorem CategoryTheory.MorphismProperty.CodescendsAlong.of_le {C : Type u_1} [Category.{v_1, u_1} C] {P Q W : MorphismProperty C} [P.CodescendsAlong Q] (hle : W ≤ Q) : P.CodescendsAlong W

instance CategoryTheory.MorphismProperty.CodescendsAlong.top {C : Type u_1} [Category.{v_1, u_1} C] {Q : MorphismProperty C} : ⊤.CodescendsAlong Q

instance CategoryTheory.MorphismProperty.CodescendsAlong.inf {C : Type u_1} [Category.{v_1, u_1} C] {P Q W : MorphismProperty C} [P.CodescendsAlong Q] [W.CodescendsAlong Q] : (P ⊓ W).CodescendsAlong Q

theorem CategoryTheory.MorphismProperty.CodescendsAlong.mk' {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} [P.RespectsIso] (H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : Limits.HasPushout f g], Q f → P (Limits.pushout.inl f g) → P g) : P.CodescendsAlong Q

Alternative constructor for CodescendsAlong using HasPushout.

instance CategoryTheory.MorphismProperty.instCodescendsAlongOfIsStableUnderCobaseChangeOfHasOfPostcompPropertyOfRespectsLeft {C : Type u_1} [Category.{v_1, u_1} C] {P Q : MorphismProperty C} [Q.IsStableUnderCobaseChange] [P.HasOfPostcompProperty Q] [P.RespectsLeft Q] : P.CodescendsAlong Q