Structures · Category theory
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions
A multiplicative morphism property W has right calculus of fractions if
any left fraction can be turned into a right fraction and that two morphisms
that can be equalized by postcomposition with a morphism in W can also
be equalized by precomposition with a morphism in W.
- Shape
- One type argument · adds exists_rightFraction, ext
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- HomotopyCategory
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- CategoryTheory.Localization.exists_rightFraction
- CategoryTheory.MorphismProperty.map_eq_iff_precomp
- CategoryTheory.MorphismProperty.LeftFraction.rightFraction
- CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction
- CategoryTheory.MorphismProperty.RightFractionRel.trans
- CategoryTheory.MorphismProperty.RightFraction.map_eq_iff
- CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction
- CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac
- CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions
- CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc
- CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.toIsMultiplicative
- CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions
- CategoryTheory.MorphismProperty.equivalenceRightFractionRel
- CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions
- CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite