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.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.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