Theorems · Definition · category theory

CategoryTheory.MorphismProperty.quotient

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (homRel : HomRel C) →
        [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel] →
          [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] →
            [W.HasQuotient homRel] → CategoryTheory.MorphismProperty (CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Quotient

Cited by

2 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.HomRel.IsStableUnderPrecompCategoryTheory.HomRel.IsStableUnderPostcompCategoryTheory.MorphismProperty.HasQuotient