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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.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 : CategoryTheory.RetractArrow f g) (hg : P g) : P f

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

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

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

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