Stability under retracts

Given P : MorphismProperty C, we introduce a typeclass P.IsStableUnderRetracts which is the property that P is stable under retracts.

class CategoryTheory.MorphismProperty.IsStableUnderRetracts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : Prop

A class of morphisms is stable under retracts if a retract of such a morphism still lies in the class.

• of_retract {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g) : P f

theorem CategoryTheory.MorphismProperty.isStableUnderRetracts_iff {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.IsStableUnderRetracts ↔ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f

theorem CategoryTheory.MorphismProperty.of_retract {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderRetracts] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g) : P f

instance CategoryTheory.MorphismProperty.instIsStableUnderRetractsInverseImage {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) (P : MorphismProperty D) [P.IsStableUnderRetracts] : (P.inverseImage F).IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.IsStableUnderRetracts.monomorphisms {C : Type u} [Category.{v, u} C] : (MorphismProperty.monomorphisms C).IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.IsStableUnderRetracts.epimorphisms {C : Type u} [Category.{v, u} C] : (MorphismProperty.epimorphisms C).IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.IsStableUnderRetracts.isomorphisms {C : Type u} [Category.{v, u} C] : (MorphismProperty.isomorphisms C).IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.instIsStableUnderRetractsOppositeOp {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.IsStableUnderRetracts] : P.op.IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.instIsStableUnderRetractsUnopOfOpposite {C : Type u} [Category.{v, u} C] (P : MorphismProperty Cᵒᵖ) [P.IsStableUnderRetracts] : P.unop.IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.instIsStableUnderRetractsMin {C : Type u} [Category.{v, u} C] (P₁ P₂ : MorphismProperty C) [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts] : (P₁ ⊓ P₂).IsStableUnderRetracts

def CategoryTheory.MorphismProperty.retracts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : MorphismProperty C

The class of morphisms that are retracts of morphisms belonging to P : MorphismProperty C.

Equations

• P.retracts f = ∃ (Z : C) (W : C) (g : Z ⟶ W) (x : CategoryTheory.RetractArrow f g), P g

theorem CategoryTheory.MorphismProperty.le_retracts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P ≤ P.retracts

theorem CategoryTheory.MorphismProperty.retracts_monotone {C : Type u} [Category.{v, u} C] : Monotone retracts

theorem CategoryTheory.MorphismProperty.isStableUnderRetracts_iff_retracts_le {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.IsStableUnderRetracts ↔ P.retracts ≤ P

theorem CategoryTheory.MorphismProperty.retracts_le {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.IsStableUnderRetracts] : P.retracts ≤ P

@[simp]

theorem CategoryTheory.MorphismProperty.retracts_le_iff {C : Type u} [Category.{v, u} C] {P Q : MorphismProperty C} [Q.IsStableUnderRetracts] : P.retracts ≤ Q ↔ P ≤ Q

instance CategoryTheory.MorphismProperty.instRespectsIsoOfIsStableUnderRetracts {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderRetracts] : P.RespectsIso