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
added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.fac
added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts
added theorem CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.uniq