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.{u_2, u_1} C]
(P Q : MorphismProperty C)
:
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
Instances
theorem
CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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)
:
theorem
CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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)
:
theorem
CategoryTheory.MorphismProperty.of_pullback_snd_of_descendsAlong
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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)
:
instance
CategoryTheory.MorphismProperty.DescendsAlong.top
{C : Type u_1}
[Category.{u_2, u_1} C]
{Q : MorphismProperty C}
:
instance
CategoryTheory.MorphismProperty.DescendsAlong.inf
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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.{u_2, 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.{u_2, u_1} C]
{P Q : MorphismProperty C}
[Q.IsStableUnderBaseChange]
[P.HasOfPrecompProperty Q]
[P.RespectsRight Q]
:
P.DescendsAlong Q
class
CategoryTheory.MorphismProperty.CodescendsAlong
{C : Type u_1}
[Category.{u_2, u_1} C]
(P Q : MorphismProperty C)
:
P codescends along Q if whenever Q holds for Z ⟶ X,
P holds for X ⟶ X ∐[Z] Y implies P holds for Z ⟶ Y.
Instances
theorem
CategoryTheory.MorphismProperty.of_isPushout_of_codescendsAlong
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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)
:
theorem
CategoryTheory.MorphismProperty.of_pushout_inl_of_codescendsAlong
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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)
:
theorem
CategoryTheory.MorphismProperty.of_pushout_inr_of_descendsAlong
{C : Type u_1}
[Category.{u_2, 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
theorem
CategoryTheory.MorphismProperty.pushout_inr_iff
{C : Type u_1}
[Category.{u_2, 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)
:
theorem
CategoryTheory.MorphismProperty.CodescendsAlong.of_le
{C : Type u_1}
[Category.{u_2, 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.{u_2, u_1} C]
{Q : MorphismProperty C}
:
instance
CategoryTheory.MorphismProperty.CodescendsAlong.inf
{C : Type u_1}
[Category.{u_2, 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.{u_2, 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.{u_2, u_1} C]
{P Q : MorphismProperty C}
[Q.IsStableUnderCobaseChange]
[P.HasOfPostcompProperty Q]
[P.RespectsLeft Q]
:
P.CodescendsAlong Q