Commit 2024-02-22 12:56 a1edd24c

View on Github →

feat(CategoryTheory/Localization): construction of a localized category using left fractions (#10606) In this PR, given a class of morphisms W : MorphismProperty C which admits a left calculus of fractions, we construct a localized category in which the morphisms are equivalence classes of left fractions.

Estimated changes

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv

added def CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv

added def CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.fac

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.uniq

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_iff_leftFractionRel

added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_of_leftFractionRel