Commit 2024-02-25 21:06 ca54d66e

View on Github →

feat(CategoryTheory/Localization): main results on left calculus of fractions (#10607) In this PR, given a class of morphisms W : MorphismProperty C which admits a left calculus of fractions, we obtain that if L : C ⥤ D is a localization functor for W, then morphisms in D can be computed using left fractions, and we show that the functor L.mapArrow : Arrow C ⥤ Arrow D is essentially surjective.

Estimated changes

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

added theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasLeftCalculusofFractions

added theorem CategoryTheory.Localization.exists_leftFraction

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.map_eq_iff

added theorem CategoryTheory.MorphismProperty.LeftFraction.map_compatibility

added theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq

added theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff

added theorem CategoryTheory.MorphismProperty.LeftFraction.map_eq_of_map_eq

added theorem CategoryTheory.MorphismProperty.map_eq_iff_postcomp