Structures · Category theory
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions
A multiplicative morphism property W has left calculus of fractions if
any right fraction can be turned into a left fraction and that two morphisms
that can be equalized by precomposition with a morphism in W can also
be equalized by postcomposition with a morphism in W.
- Shape
- One type argument · adds exists_leftFraction, 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 by103
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Q
- CategoryTheory.Localization.Preadditive.add'
- CategoryTheory.Localization.exists_leftFraction
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv
- CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk
- CategoryTheory.Localization.Preadditive.add'_eq
- CategoryTheory.Localization.Preadditive.add
- CategoryTheory.Localization.exists_leftFraction₂
- CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction
- CategoryTheory.MorphismProperty.LeftFraction.comp₀
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso
- CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff
- CategoryTheory.Localization.essSurj_mapArrow
- CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
- CategoryTheory.Localization.Preadditive.add'.congr_simp
- CategoryTheory.MorphismProperty.RightFraction.leftFraction
- CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map
- CategoryTheory.MorphismProperty.LeftFractionRel.trans
- CategoryTheory.Localization.functor_additive_iff
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id
- CategoryTheory.Localization.Preadditive.addCommGroup
- CategoryTheory.Localization.Preadditive.neg'
- CategoryTheory.Localization.Preadditive.comp_add
- CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac
- CategoryTheory.MorphismProperty.map_eq_iff_postcomp
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv
- CategoryTheory.MorphismProperty.LeftFraction.comp
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id
- CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq
- CategoryTheory.Localization.Preadditive.add_comp
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq
- CategoryTheory.Localization.essSurj_mapComposableArrows
- CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts
- CategoryTheory.Localization.Preadditive.add'_comp
- CategoryTheory.Localization.Preadditive.add_eq
- CategoryTheory.Localization.Preadditive.map_add
- CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel
- CategoryTheory.Localization.exists_leftFraction₃
- CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map
- CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk
- CategoryTheory.MorphismProperty.RightFraction₂.exists_leftFraction₂
- CategoryTheory.Localization.Preadditive.add_eq_add
- CategoryTheory.Localization.Preadditive.neg'_eq
- CategoryTheory.MorphismProperty.LeftFraction.comp_eq
- CategoryTheory.MorphismProperty.equivalenceLeftFractionRel
- CategoryTheory.Localization.preadditive
- CategoryTheory.Functor.faithful_of_comp_of_hasLeftCalculusOfFractions
- CategoryTheory.Localization.Preadditive.add.congr_simp
- CategoryTheory.Localization.Preadditive.add'_zero