Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.HasQuotient

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

Defined in

Mathlib.CategoryTheory.MorphismProperty.Quotient

Cited by

4 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.HomRel.IsStableUnderPrecompCategoryTheory.HomRel.IsStableUnderPostcomp