Commit 2024-03-29 10:05 1c323119

View on Github →

feat(CategoryTheory/Localization): dualize results for right calculus of fractions (#11721) In this PR, the results for the left calculus of fractions are dualized in order to obtain similar results for the right calculus of fractions

Estimated changes

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

added theorem CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusofFractions

added theorem CategoryTheory.Localization.exists_rightFraction

added def CategoryTheory.MorphismProperty.LeftFraction.op

added theorem CategoryTheory.MorphismProperty.LeftFraction.op_map

added def CategoryTheory.MorphismProperty.LeftFraction.unop

added theorem CategoryTheory.MorphismProperty.LeftFractionRel.op

added theorem CategoryTheory.MorphismProperty.LeftFractionRel.unop

added theorem CategoryTheory.MorphismProperty.RightFraction.map_eq_iff

added def CategoryTheory.MorphismProperty.RightFraction.op

added theorem CategoryTheory.MorphismProperty.RightFraction.op_map

added def CategoryTheory.MorphismProperty.RightFraction.unop

added theorem CategoryTheory.MorphismProperty.RightFractionRel.op

added theorem CategoryTheory.MorphismProperty.RightFractionRel.refl

added theorem CategoryTheory.MorphismProperty.RightFractionRel.symm

added theorem CategoryTheory.MorphismProperty.RightFractionRel.trans

added theorem CategoryTheory.MorphismProperty.RightFractionRel.unop

added def CategoryTheory.MorphismProperty.RightFractionRel

added theorem CategoryTheory.MorphismProperty.equivalenceRightFractionRel

added theorem CategoryTheory.MorphismProperty.leftFractionRel_op_iff

added theorem CategoryTheory.MorphismProperty.map_eq_iff_precomp

added theorem CategoryTheory.MorphismProperty.rightFractionRel_op_iff