Commit 2024-04-18 01:19 42916140

View on Github →

feat(CategoryTheory): more lemmas for the calculus of fractions (#11737) We introduce lemmas on fractions which shall be useful when constructing the preadditive structure on the localized category.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean

added theorem CategoryTheory.Localization.exists_leftFraction₂

added theorem CategoryTheory.Localization.exists_leftFraction₃

added def CategoryTheory.MorphismProperty.LeftFraction₂.fst

added theorem CategoryTheory.MorphismProperty.LeftFraction₂.map_eq_iff

added def CategoryTheory.MorphismProperty.LeftFraction₂.snd

added def CategoryTheory.MorphismProperty.LeftFraction₂.symm

added structure CategoryTheory.MorphismProperty.LeftFraction₂

added theorem CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst

added theorem CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd

added def CategoryTheory.MorphismProperty.LeftFraction₂Rel

added def CategoryTheory.MorphismProperty.LeftFraction₃.forgetFst

added def CategoryTheory.MorphismProperty.LeftFraction₃.forgetSnd

added def CategoryTheory.MorphismProperty.LeftFraction₃.forgetThd

added def CategoryTheory.MorphismProperty.LeftFraction₃.fst

added def CategoryTheory.MorphismProperty.LeftFraction₃.snd

added def CategoryTheory.MorphismProperty.LeftFraction₃.thd

added structure CategoryTheory.MorphismProperty.LeftFraction₃

added theorem CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂

added def CategoryTheory.MorphismProperty.RightFraction₂.fst

added def CategoryTheory.MorphismProperty.RightFraction₂.snd

added structure CategoryTheory.MorphismProperty.RightFraction₂