Classes of morphisms induced on quotient categories

Let W : MorphismProperty C and homRel : HomRel C. We assume that homRel is stable under pre- and postcomposition. We introduce a property W.HasQuotient homRel expressing that W induces a property of morphisms on the quotient category, i.e. W f ↔ W g when homRel f g holds. We denote W.quotient homRel : MorphismProperty (Quotient homRel) the induced property of morphisms: a morphism in C satisfies W iff (Quotient.functor homRel).map f does.

class CategoryTheory.MorphismProperty.HasQuotient {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) (homRel : HomRel C) [HomRel.IsStableUnderPrecomp homRel] [HomRel.IsStableUnderPostcomp homRel] : Prop

Let W : MorphismProperty C and homRel : HomRel C. We say that W induces a class of morphisms on the quotient category by homRel if homRel is stable under pre- and postcomposition and if W f ↔ W g whenever homRel f g hold.

• iff ⦃X Y : C⦄ ⦃f g : X ⟶ Y⦄ : homRel f g → (W f ↔ W g)

theorem CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGen {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) {homRel : HomRel C} [HomRel.IsStableUnderPrecomp homRel] [HomRel.IsStableUnderPostcomp homRel] [W.HasQuotient homRel] {X Y : C} {f g : X ⟶ Y} (h : Relation.EqvGen homRel f g) : W f ↔ W g

def CategoryTheory.MorphismProperty.quotient {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) (homRel : HomRel C) [HomRel.IsStableUnderPrecomp homRel] [HomRel.IsStableUnderPostcomp homRel] [W.HasQuotient homRel] : MorphismProperty (Quotient homRel)

The property of morphisms that is induced by W : MorphismProperty C on the quotient category by homRel : HomRel C when W.HasQuotient homRel holds.

Equations

• W.quotient homRel f_3 = ∃ (f' : X ⟶ Y) (_ : W f'), f_3 = (CategoryTheory.Quotient.functor homRel).map f'

theorem CategoryTheory.MorphismProperty.quotient_iff {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) (homRel : HomRel C) [HomRel.IsStableUnderPrecomp homRel] [HomRel.IsStableUnderPostcomp homRel] [W.HasQuotient homRel] {X Y : C} (f : X ⟶ Y) : W.quotient homRel ((Quotient.functor homRel).map f) ↔ W f

theorem CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor {C : Type u_1} [Category.{v_1, u_1} C] (W : MorphismProperty C) (homRel : HomRel C) [HomRel.IsStableUnderPrecomp homRel] [HomRel.IsStableUnderPostcomp homRel] [W.HasQuotient homRel] : W = (W.quotient homRel).inverseImage (Quotient.functor homRel)