Commit 2026-01-12 11:29 197b55cb

View on Github →

feat(CategoryTheory): MorphismProperty induced on a quotient category (#33084) 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.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

Created Mathlib/CategoryTheory/MorphismProperty/Quotient.lean

added theorem CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGen

added theorem CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor

added def CategoryTheory.MorphismProperty.quotient

added theorem CategoryTheory.MorphismProperty.quotient_iff

Modified Mathlib/CategoryTheory/PathCategory/Basic.lean

Modified Mathlib/CategoryTheory/Quotient.lean

added theorem CategoryTheory.HomRel.CompClosure.of

added inductive CategoryTheory.HomRel.CompClosure

added theorem CategoryTheory.HomRel.compClosure_eq_self

added theorem CategoryTheory.HomRel.compClosure_iff_self

deleted theorem CategoryTheory.Quotient.CompClosure.of

deleted inductive CategoryTheory.Quotient.CompClosure

modified def CategoryTheory.Quotient.Hom

deleted theorem CategoryTheory.Quotient.compClosure_eq_self

deleted theorem CategoryTheory.Quotient.compClosure_iff_self

deleted theorem CategoryTheory.Quotient.comp_left

deleted theorem CategoryTheory.Quotient.comp_right

Modified Mathlib/CategoryTheory/Quotient/Linear.lean

Modified Mathlib/CategoryTheory/Quotient/Preadditive.lean