CalculusOfFractions

📁 Source: Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

Statistics

Metric	Count
Definitions `HasLeftCalculusOfFractions`, `HasRightCalculusOfFractions`, `LeftFraction`, `comp`, `map`, `mk`, `Q`, `Qinv`, `Qiso`, `homMk`, `instCategory`, `strictUniversalPropertyFixedTarget`, `Y'`, `comp`, `comp₀`, `f`, `map`, `ofHom`, `ofInv`, `op`, `rightFraction`, `s`, `unop`, `LeftFractionRel`, `RightFraction`, `X'`, `f`, `leftFraction`, `map`, `ofHom`, `ofInv`, `op`, `s`, `unop`, `RightFractionRel`	35
Theorems `essSurj_mapArrow`, `essSurj_mapArrow_of_hasRightCalculusOfFractions`, `exists_leftFraction`, `exists_rightFraction`, `exists_leftFraction`, `ext`, `toIsMultiplicative`, `exists_rightFraction`, `ext`, `toIsMultiplicative`, `comp_eq`, `map_mk`, `mk_surjective`, `Q_map`, `Q_map_comp_Qinv`, `Q_obj`, `Qiso_hom`, `Qiso_hom_inv_id`, `Qiso_hom_inv_id_assoc`, `Qiso_inv`, `Qiso_inv_hom_id`, `Qiso_inv_hom_id_assoc`, `fac`, `inverts`, `uniq`, `homMk_comp_homMk`, `homMk_eq`, `homMk_eq_hom_mk`, `homMk_eq_iff_leftFractionRel`, `homMk_eq_of_leftFractionRel`, `instIsIsoQinv`, `instIsLocalizationQ`, `map_eq_iff`, `comp_eq`, `comp₀_rel`, `exists_rightFraction`, `hs`, `map_comp_map_eq_map`, `map_comp_map_s`, `map_comp_map_s_assoc`, `map_compatibility`, `map_eq`, `map_eq_iff`, `map_eq_of_map_eq`, `map_hom_ofInv_id`, `map_hom_ofInv_id_assoc`, `map_ofHom`, `map_ofInv_hom_id`, `map_ofInv_hom_id_assoc`, `ofHom_Y'`, `ofHom_f`, `ofHom_s`, `ofInv_Y'`, `ofInv_f`, `ofInv_s`, `op_X'`, `op_f`, `op_map`, `op_s`, `rightFraction_fac`, `rightFraction_fac_assoc`, `unop_X'`, `unop_f`, `unop_s`, `op`, `refl`, `trans`, `unop`, `exists_leftFraction`, `hs`, `leftFraction_fac`, `leftFraction_fac_assoc`, `map_eq_iff`, `map_hom_ofInv_id`, `map_hom_ofInv_id_assoc`, `map_ofHom`, `map_ofInv_hom_id`, `map_ofInv_hom_id_assoc`, `map_s_comp_map`, `map_s_comp_map_assoc`, `ofHom_X'`, `ofHom_f`, `ofHom_s`, `ofInv_X'`, `ofInv_f`, `ofInv_s`, `op_Y'`, `op_f`, `op_map`, `op_s`, `unop_Y'`, `unop_f`, `unop_s`, `op`, `refl`, `trans`, `unop`, `equivalenceLeftFractionRel`, `equivalenceRightFractionRel`, `instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions`, `instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite`, `instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions`, `instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite`, `leftFractionRel_op_iff`, `map_eq_iff_postcomp`, `map_eq_iff_precomp`, `rightFractionRel_op_iff`	107
Total	142

CategoryTheory.Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essSurj_mapArrow` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.mapArrow`	—	`essSurj` `inverts` `exists_leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.cancel_epi` `CategoryTheory.IsSplitEpi.epi` `CategoryTheory.IsSplitEpi.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s`
`essSurj_mapArrow_of_hasRightCalculusOfFractions` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.mapArrow`	—	`essSurj_mapArrow` `CategoryTheory.Functor.IsLocalization.op` `CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions` `CategoryTheory.CommaMorphism.w`
`exists_leftFraction` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.map` `inverts`	—	`CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsLocalizationQ` `inverts` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Functor.map_surjective` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective` `CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq` `CategoryTheory.MorphismProperty.LeftFraction.map_compatibility`
`exists_rightFraction` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.map` `inverts`	—	`inverts` `CategoryTheory.Functor.IsLocalization.op` `exists_leftFraction` `CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions` `CategoryTheory.MorphismProperty.IsInvertedBy.op` `CategoryTheory.MorphismProperty.RightFraction.op_map`

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`HasLeftCalculusOfFractions` 📖	CompData	6 math math: `CategoryTheory.Adjunction.hasLeftCalculusOfFractions'`, `instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite`, `instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions`, `DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso`, `CategoryTheory.Adjunction.hasLeftCalculusOfFractions`, `CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated`
`HasRightCalculusOfFractions` 📖	CompData	6 math math: `CategoryTheory.ObjectProperty.instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated`, `CategoryTheory.Adjunction.hasRightCalculusOfFractions`, `instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite`, `CategoryTheory.Adjunction.hasRightCalculusOfFractions'`, `instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions`, `DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso`
`LeftFraction` 📖	CompData	1 math math: `equivalenceLeftFractionRel`
`LeftFractionRel` 📖	MathDef	12 math math: `RightFractionRel.unop`, `LeftFraction₂Rel.snd`, `LeftFraction.Localization.homMk_eq_iff_leftFractionRel`, `RightFractionRel.op`, `LeftFraction.map_eq_iff`, `rightFractionRel_op_iff`, `LeftFractionRel.refl`, `LeftFraction₂Rel.fst`, `equivalenceLeftFractionRel`, `LeftFraction.comp₀_rel`, `leftFractionRel_op_iff`, `LeftFraction.Localization.map_eq_iff`
`RightFraction` 📖	CompData	1 math math: `equivalenceRightFractionRel`
`RightFractionRel` 📖	MathDef	7 math math: `LeftFractionRel.unop`, `equivalenceRightFractionRel`, `rightFractionRel_op_iff`, `RightFraction.map_eq_iff`, `leftFractionRel_op_iff`, `RightFractionRel.refl`, `LeftFractionRel.op`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalenceLeftFractionRel` 📖	mathematical	—	`LeftFraction` `LeftFractionRel`	—	`LeftFractionRel.refl` `LeftFractionRel.symm` `LeftFractionRel.trans`
`equivalenceRightFractionRel` 📖	mathematical	—	`RightFraction` `RightFractionRel`	—	`RightFractionRel.refl` `RightFractionRel.symm` `RightFractionRel.trans`
`instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions` 📖	mathematical	—	`HasLeftCalculusOfFractions` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct`	—	`IsMultiplicative.op` `HasRightCalculusOfFractions.toIsMultiplicative` `HasRightCalculusOfFractions.exists_rightFraction` `HasRightCalculusOfFractions.ext`
`instHasLeftCalculusOfFractionsUnopOfHasRightCalculusOfFractionsOpposite` 📖	mathematical	—	`HasLeftCalculusOfFractions` `unop` `CategoryTheory.Category.toCategoryStruct`	—	`IsMultiplicative.unop` `HasRightCalculusOfFractions.toIsMultiplicative` `HasRightCalculusOfFractions.exists_rightFraction` `HasRightCalculusOfFractions.ext`
`instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions` 📖	mathematical	—	`HasRightCalculusOfFractions` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct`	—	`IsMultiplicative.op` `HasLeftCalculusOfFractions.toIsMultiplicative` `HasLeftCalculusOfFractions.exists_leftFraction` `HasLeftCalculusOfFractions.ext`
`instHasRightCalculusOfFractionsUnopOfHasLeftCalculusOfFractionsOpposite` 📖	mathematical	—	`HasRightCalculusOfFractions` `unop` `CategoryTheory.Category.toCategoryStruct`	—	`IsMultiplicative.unop` `HasLeftCalculusOfFractions.toIsMultiplicative` `HasLeftCalculusOfFractions.exists_leftFraction` `HasLeftCalculusOfFractions.ext`
`leftFractionRel_op_iff` 📖	mathematical	—	`LeftFractionRel` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `RightFraction.op` `RightFractionRel`	—	`LeftFractionRel.unop` `RightFractionRel.op`
`map_eq_iff_postcomp` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`IsMultiplicative.toContainsIdentities` `HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.Localization.inverts` `LeftFraction.map_eq_iff` `LeftFraction.map_ofHom` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Functor.map_comp`
`map_eq_iff_precomp` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`IsMultiplicative.toContainsIdentities` `HasRightCalculusOfFractions.toIsMultiplicative` `CategoryTheory.Localization.inverts` `RightFraction.map_eq_iff` `RightFraction.map_ofHom` `CategoryTheory.cancel_epi` `CategoryTheory.IsSplitEpi.epi` `CategoryTheory.IsSplitEpi.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Functor.map_comp`
`rightFractionRel_op_iff` 📖	mathematical	—	`RightFractionRel` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `LeftFraction.op` `LeftFractionRel`	—	`RightFractionRel.unop` `LeftFractionRel.op`

CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_leftFraction` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.RightFraction.X'` `CategoryTheory.MorphismProperty.LeftFraction.Y'` `CategoryTheory.MorphismProperty.RightFraction.f` `CategoryTheory.MorphismProperty.LeftFraction.s` `CategoryTheory.MorphismProperty.RightFraction.s` `CategoryTheory.MorphismProperty.LeftFraction.f`	—	—
`ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—	—
`toIsMultiplicative` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative`	—	—

CategoryTheory.MorphismProperty.HasRightCalculusOfFractions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_rightFraction` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.RightFraction.X'` `CategoryTheory.MorphismProperty.LeftFraction.Y'` `CategoryTheory.MorphismProperty.RightFraction.s` `CategoryTheory.MorphismProperty.LeftFraction.f` `CategoryTheory.MorphismProperty.RightFraction.f` `CategoryTheory.MorphismProperty.LeftFraction.s`	—	—
`ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—	—
`toIsMultiplicative` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative`	—	—

CategoryTheory.MorphismProperty.LeftFraction

Definitions

Name	Category	Theorems
`Y'` 📖	CompOp	22 math math: `hs`, `op_X'`, `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac`, `rightFraction_fac`, `ofHom_Y'`, `unop_X'`, `unop_f`, `op_f`, `op_s`, `unop_s`, `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc`, `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction`, `exists_rightFraction`, `CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`, `rightFraction_fac_assoc`, `map_comp_map_s`, `map_comp_map_s_assoc`, `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`, `CategoryTheory.MorphismProperty.RightFraction.unop_Y'`, `ofInv_Y'`, `CategoryTheory.MorphismProperty.RightFraction.op_Y'`, `map_eq`
`comp` 📖	CompOp	2 math math: `Localization.Hom.comp_eq`, `comp_eq`
`comp₀` 📖	CompOp	4 math math: `Localization.homMk_comp_homMk`, `comp_eq`, `map_comp_map_eq_map`, `comp₀_rel`
`f` 📖	CompOp	17 math math: `ofInv_f`, `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac`, `rightFraction_fac`, `unop_f`, `op_f`, `CategoryTheory.MorphismProperty.RightFraction.op_f`, `CategoryTheory.MorphismProperty.RightFraction.unop_f`, `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc`, `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction`, `exists_rightFraction`, `CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`, `rightFraction_fac_assoc`, `map_comp_map_s`, `ofHom_f`, `map_comp_map_s_assoc`, `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`, `map_eq`
`map` 📖	CompOp	21 math math: `map_compatibility`, `op_map`, `CategoryTheory.MorphismProperty.LeftFraction₂.map_add`, `Localization.Hom.map_mk`, `map_ofHom`, `CategoryTheory.MorphismProperty.LeftFraction₂.map_eq_iff`, `CategoryTheory.Localization.exists_leftFraction₂`, `map_hom_ofInv_id_assoc`, `map_eq_iff`, `CategoryTheory.MorphismProperty.RightFraction.op_map`, `Localization.homMk_eq`, `map_ofInv_hom_id_assoc`, `map_hom_ofInv_id`, `CategoryTheory.Localization.exists_leftFraction`, `map_comp_map_eq_map`, `map_comp_map_s`, `CategoryTheory.Localization.exists_leftFraction₃`, `map_ofInv_hom_id`, `map_comp_map_s_assoc`, `Localization.map_eq_iff`, `map_eq`
`ofHom` 📖	CompOp	5 math math: `ofHom_Y'`, `map_ofHom`, `Localization.Q_map`, `ofHom_f`, `ofHom_s`
`ofInv` 📖	CompOp	7 math math: `ofInv_f`, `map_hom_ofInv_id_assoc`, `map_ofInv_hom_id_assoc`, `map_hom_ofInv_id`, `map_ofInv_hom_id`, `ofInv_s`, `ofInv_Y'`
`op` 📖	CompOp	6 math math: `op_map`, `op_X'`, `op_f`, `op_s`, `CategoryTheory.MorphismProperty.rightFractionRel_op_iff`, `CategoryTheory.MorphismProperty.LeftFractionRel.op`
`rightFraction` 📖	CompOp	2 math math: `rightFraction_fac`, `rightFraction_fac_assoc`
`s` 📖	CompOp	18 math math: `hs`, `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac`, `rightFraction_fac`, `CategoryTheory.MorphismProperty.RightFraction.unop_s`, `op_s`, `unop_s`, `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc`, `CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction`, `exists_rightFraction`, `CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`, `rightFraction_fac_assoc`, `map_comp_map_s`, `map_comp_map_s_assoc`, `ofHom_s`, `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`, `CategoryTheory.MorphismProperty.RightFraction.op_s`, `ofInv_s`, `map_eq`
`unop` 📖	CompOp	4 math math: `CategoryTheory.MorphismProperty.LeftFractionRel.unop`, `unop_X'`, `unop_f`, `unop_s`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Y'` `f` `s`	`comp` `comp₀`	—	`hs` `comp₀_rel` `CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac`
`comp₀_rel` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Y'` `f` `s`	`CategoryTheory.MorphismProperty.LeftFractionRel` `comp₀`	—	`hs` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative`
`exists_rightFraction` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.RightFraction.X'` `Y'` `CategoryTheory.MorphismProperty.RightFraction.s` `f` `CategoryTheory.MorphismProperty.RightFraction.f` `s`	—	`CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`
`hs` 📖	mathematical	—	`Y'` `s`	—	—
`map_comp_map_eq_map` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Y'` `f` `s`	`CategoryTheory.Functor.obj` `map` `CategoryTheory.Localization.inverts` `comp₀`	—	`CategoryTheory.Localization.inverts` `hs` `CategoryTheory.Functor.map_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `map_comp_map_s` `CategoryTheory.Category.assoc` `map_comp_map_s_assoc`
`map_comp_map_s` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Y'` `map` `CategoryTheory.Functor.map` `s` `f`	—	`CategoryTheory.Category.assoc` `CategoryTheory.IsIso.inv_hom_id` `CategoryTheory.Category.comp_id`
`map_comp_map_s_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `Y'` `CategoryTheory.Functor.map` `s` `f`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_comp_map_s`
`map_compatibility` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Equivalence.functor` `CategoryTheory.Localization.uniq` `CategoryTheory.Functor.obj` `map` `CategoryTheory.Localization.inverts` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Localization.compUniqFunctor` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Localization.inverts` `hs` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `map_comp_map_s` `CategoryTheory.NatTrans.naturality`
`map_eq` 📖	mathematical	—	`map` `CategoryTheory.Localization.inverts` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Y'` `CategoryTheory.Functor.map` `f` `CategoryTheory.Iso.inv` `CategoryTheory.Localization.isoOfHom` `s` `hs`	—	`CategoryTheory.Localization.inverts`
`map_eq_iff` 📖	mathematical	—	`map` `CategoryTheory.Localization.inverts` `CategoryTheory.MorphismProperty.LeftFractionRel`	—	`CategoryTheory.Localization.inverts` `Localization.instIsLocalizationQ` `Localization.map_eq_iff` `map_eq_of_map_eq`
`map_eq_of_map_eq` 📖	—	`map` `CategoryTheory.Localization.inverts`	—	—	`CategoryTheory.Localization.inverts` `CategoryTheory.Functor.map_injective` `CategoryTheory.Equivalence.faithful_functor` `map_compatibility`
`map_hom_ofInv_id` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `map` `ofInv` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.IsIso.hom_inv_id`
`map_hom_ofInv_id_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `map` `ofInv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_hom_ofInv_id`
`map_ofHom` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`map` `ofHom` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.inv.congr_simp` `CategoryTheory.IsIso.inv_id` `CategoryTheory.Category.comp_id`
`map_ofInv_hom_id` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `ofInv` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.IsIso.inv_hom_id`
`map_ofInv_hom_id_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `ofInv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_ofInv_hom_id`
`ofHom_Y'` 📖	mathematical	—	`Y'` `ofHom`	—	—
`ofHom_f` 📖	mathematical	—	`f` `ofHom`	—	—
`ofHom_s` 📖	mathematical	—	`s` `ofHom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`ofInv_Y'` 📖	mathematical	—	`Y'` `ofInv`	—	—
`ofInv_f` 📖	mathematical	—	`f` `ofInv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`ofInv_s` 📖	mathematical	—	`s` `ofInv`	—	—
`op_X'` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.X'` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `op` `Y'`	—	—
`op_f` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.f` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `Y'` `f`	—	—
`op_map` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `CategoryTheory.MorphismProperty.RightFraction.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `Opposite.op` `op` `CategoryTheory.Functor.op` `CategoryTheory.MorphismProperty.IsInvertedBy.op`	—	`CategoryTheory.MorphismProperty.IsInvertedBy.op` `CategoryTheory.isIso_op` `CategoryTheory.op_inv`
`op_s` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.s` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `Y'` `s`	—	—
`rightFraction_fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.RightFraction.X'` `rightFraction` `Y'` `CategoryTheory.MorphismProperty.RightFraction.s` `f` `CategoryTheory.MorphismProperty.RightFraction.f` `s`	—	`exists_rightFraction`
`rightFraction_fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.RightFraction.X'` `rightFraction` `CategoryTheory.MorphismProperty.RightFraction.s` `Y'` `f` `CategoryTheory.MorphismProperty.RightFraction.f` `s`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `rightFraction_fac`
`unop_X'` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.X'` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `unop` `Y'` `Opposite` `CategoryTheory.Category.opposite`	—	—
`unop_f` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.f` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `Y'` `Opposite` `CategoryTheory.Category.opposite` `f`	—	—
`unop_s` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFraction.s` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `Y'` `Opposite` `CategoryTheory.Category.opposite` `s`	—	—

CategoryTheory.MorphismProperty.LeftFraction.Localization

Definitions

Name	Category	Theorems
`Q` 📖	CompOp	16 math math: `StrictUniversalPropertyFixedTarget.fac`, `homMk_comp_homMk`, `Qiso_hom_inv_id`, `StrictUniversalPropertyFixedTarget.inverts`, `Qiso_inv_hom_id_assoc`, `instIsLocalizationQ`, `Qiso_hom_inv_id_assoc`, `homMk_eq`, `instIsIsoQinv`, `Qiso_hom`, `Qiso_inv`, `Q_map`, `Qiso_inv_hom_id`, `Q_obj`, `map_eq_iff`, `Q_map_comp_Qinv`
`Qinv` 📖	CompOp	7 math math: `Qiso_hom_inv_id`, `Qiso_inv_hom_id_assoc`, `Qiso_hom_inv_id_assoc`, `instIsIsoQinv`, `Qiso_inv`, `Qiso_inv_hom_id`, `Q_map_comp_Qinv`
`Qiso` 📖	CompOp	2 math math: `Qiso_hom`, `Qiso_inv`
`homMk` 📖	CompOp	7 math math: `homMk_comp_homMk`, `homMk_eq_iff_leftFractionRel`, `homMk_eq_of_leftFractionRel`, `homMk_eq`, `Q_map`, `homMk_eq_hom_mk`, `Q_map_comp_Qinv`
`instCategory` 📖	CompOp	16 math math: `StrictUniversalPropertyFixedTarget.fac`, `homMk_comp_homMk`, `Qiso_hom_inv_id`, `StrictUniversalPropertyFixedTarget.inverts`, `Qiso_inv_hom_id_assoc`, `instIsLocalizationQ`, `Qiso_hom_inv_id_assoc`, `homMk_eq`, `instIsIsoQinv`, `Qiso_hom`, `Qiso_inv`, `Q_map`, `Qiso_inv_hom_id`, `Q_obj`, `map_eq_iff`, `Q_map_comp_Qinv`
`strictUniversalPropertyFixedTarget` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Q_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `Q` `homMk` `CategoryTheory.MorphismProperty.LeftFraction.ofHom` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative`	—	—
`Q_map_comp_Qinv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `Q` `CategoryTheory.Functor.map` `Qinv` `homMk`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `homMk_comp_homMk` `CategoryTheory.Category.comp_id`
`Q_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `Q`	—	—
`Qiso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `CategoryTheory.Functor.obj` `Q` `Qiso` `CategoryTheory.Functor.map`	—	—
`Qiso_hom_inv_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `Q` `CategoryTheory.Functor.map` `Qinv` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Iso.hom_inv_id`
`Qiso_hom_inv_id_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `Q` `CategoryTheory.Functor.map` `Qinv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `Qiso_hom_inv_id`
`Qiso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `CategoryTheory.Functor.obj` `Q` `Qiso` `Qinv`	—	—
`Qiso_inv_hom_id` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `Q` `Qinv` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Iso.inv_hom_id`
`Qiso_inv_hom_id_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Functor.obj` `Q` `Qinv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `Qiso_inv_hom_id`
`homMk_comp_homMk` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.LeftFraction.Y'` `CategoryTheory.MorphismProperty.LeftFraction.f` `CategoryTheory.MorphismProperty.LeftFraction.s`	`CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `CategoryTheory.Functor.obj` `Q` `homMk` `CategoryTheory.MorphismProperty.LeftFraction.comp₀`	—	`Hom.comp_eq` `CategoryTheory.MorphismProperty.LeftFraction.comp_eq`
`homMk_eq` 📖	mathematical	—	`homMk` `CategoryTheory.MorphismProperty.LeftFraction.map` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `Q` `CategoryTheory.Localization.inverts` `instIsLocalizationQ`	—	`CategoryTheory.Localization.inverts` `instIsLocalizationQ` `CategoryTheory.MorphismProperty.LeftFraction.hs` `Q_map_comp_Qinv` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Category.assoc` `Qiso_inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s`
`homMk_eq_hom_mk` 📖	mathematical	—	`homMk`	—	—
`homMk_eq_iff_leftFractionRel` 📖	mathematical	—	`homMk` `CategoryTheory.MorphismProperty.LeftFractionRel`	—	`Equivalence.quot_mk_eq_iff` `CategoryTheory.MorphismProperty.equivalenceLeftFractionRel`
`homMk_eq_of_leftFractionRel` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFractionRel`	`homMk`	—	—
`instIsIsoQinv` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `CategoryTheory.Functor.obj` `Q` `Qinv`	—	`CategoryTheory.Iso.isIso_inv`
`instIsLocalizationQ` 📖	mathematical	—	`CategoryTheory.Functor.IsLocalization` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `Q`	—	`CategoryTheory.Functor.IsLocalization.mk'`
`map_eq_iff` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.map` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `instCategory` `Q` `CategoryTheory.Localization.inverts` `instIsLocalizationQ` `CategoryTheory.MorphismProperty.LeftFractionRel`	—	`CategoryTheory.Localization.inverts` `instIsLocalizationQ` `homMk_eq_iff_leftFractionRel` `homMk_eq`

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_eq`
`map` 📖	CompOp	1 math math: `map_mk`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq` 📖	mathematical	—	`comp` `CategoryTheory.MorphismProperty.LeftFraction.comp`	—	—
`map_mk` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`map` `CategoryTheory.MorphismProperty.LeftFraction.map`	—	—
`mk_surjective` 📖	—	—	—	—	—

CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Q` `lift`	—	`CategoryTheory.Functor.ext` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.MorphismProperty.LeftFraction.map_ofHom`
`inverts` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Q`	—	`CategoryTheory.Iso.isIso_hom`
`uniq` 📖	—	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.LeftFraction.Localization` `CategoryTheory.MorphismProperty.LeftFraction.Localization.instCategory` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Q`	—	—	`CategoryTheory.Functor.ext` `CategoryTheory.Functor.congr_obj` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.congr_hom` `inverts` `CategoryTheory.cancel_epi` `CategoryTheory.IsSplitEpi.epi` `CategoryTheory.instIsSplitEpiMap` `CategoryTheory.IsSplitEpi.of_iso` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.eqToHom_refl` `CategoryTheory.Category.comp_id`

CategoryTheory.MorphismProperty.LeftFractionRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFractionRel`	`CategoryTheory.MorphismProperty.RightFractionRel` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.MorphismProperty.LeftFraction.op`	—	—
`refl` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFractionRel`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.MorphismProperty.LeftFraction.hs`
`trans` 📖	—	`CategoryTheory.MorphismProperty.LeftFractionRel`	—	—	`CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext` `CategoryTheory.MorphismProperty.LeftFraction.hs` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative`
`unop` 📖	mathematical	`CategoryTheory.MorphismProperty.LeftFractionRel` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.MorphismProperty.RightFractionRel` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `CategoryTheory.MorphismProperty.LeftFraction.unop`	—	—

CategoryTheory.MorphismProperty.RightFraction

Definitions

Name	Category	Theorems
`X'` 📖	CompOp	21 math math: `CategoryTheory.MorphismProperty.LeftFraction.op_X'`, `leftFraction_fac`, `CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac`, `map_s_comp_map_assoc`, `CategoryTheory.MorphismProperty.LeftFraction.unop_X'`, `unop_s`, `map_s_comp_map`, `ofHom_X'`, `op_f`, `ofInv_X'`, `unop_f`, `leftFraction_fac_assoc`, `exists_leftFraction`, `CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction`, `CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`, `CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc`, `hs`, `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`, `unop_Y'`, `op_s`, `op_Y'`
`f` 📖	CompOp	16 math math: `leftFraction_fac`, `CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac`, `map_s_comp_map_assoc`, `map_s_comp_map`, `CategoryTheory.MorphismProperty.LeftFraction.unop_f`, `CategoryTheory.MorphismProperty.LeftFraction.op_f`, `op_f`, `unop_f`, `leftFraction_fac_assoc`, `exists_leftFraction`, `CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction`, `CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`, `CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc`, `ofInv_f`, `ofHom_f`, `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`
`leftFraction` 📖	CompOp	2 math math: `leftFraction_fac`, `leftFraction_fac_assoc`
`map` 📖	CompOp	11 math math: `CategoryTheory.Localization.exists_rightFraction`, `CategoryTheory.MorphismProperty.LeftFraction.op_map`, `map_ofInv_hom_id`, `map_s_comp_map_assoc`, `map_hom_ofInv_id`, `map_hom_ofInv_id_assoc`, `map_s_comp_map`, `map_ofInv_hom_id_assoc`, `op_map`, `map_eq_iff`, `map_ofHom`
`ofHom` 📖	CompOp	4 math math: `ofHom_s`, `ofHom_X'`, `map_ofHom`, `ofHom_f`
`ofInv` 📖	CompOp	7 math math: `map_ofInv_hom_id`, `ofInv_s`, `map_hom_ofInv_id`, `map_hom_ofInv_id_assoc`, `map_ofInv_hom_id_assoc`, `ofInv_X'`, `ofInv_f`
`op` 📖	CompOp	6 math math: `CategoryTheory.MorphismProperty.RightFractionRel.op`, `op_f`, `op_map`, `CategoryTheory.MorphismProperty.leftFractionRel_op_iff`, `op_s`, `op_Y'`
`s` 📖	CompOp	17 math math: `leftFraction_fac`, `CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac`, `ofInv_s`, `map_s_comp_map_assoc`, `ofHom_s`, `unop_s`, `map_s_comp_map`, `CategoryTheory.MorphismProperty.LeftFraction.op_s`, `CategoryTheory.MorphismProperty.LeftFraction.unop_s`, `leftFraction_fac_assoc`, `exists_leftFraction`, `CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction`, `CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction`, `CategoryTheory.MorphismProperty.LeftFraction.rightFraction_fac_assoc`, `hs`, `CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`, `op_s`
`unop` 📖	CompOp	4 math math: `CategoryTheory.MorphismProperty.RightFractionRel.unop`, `unop_s`, `unop_f`, `unop_Y'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_leftFraction` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X'` `CategoryTheory.MorphismProperty.LeftFraction.Y'` `f` `CategoryTheory.MorphismProperty.LeftFraction.s` `s` `CategoryTheory.MorphismProperty.LeftFraction.f`	—	`CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction`
`hs` 📖	mathematical	—	`X'` `s`	—	—
`leftFraction_fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X'` `CategoryTheory.MorphismProperty.LeftFraction.Y'` `leftFraction` `f` `CategoryTheory.MorphismProperty.LeftFraction.s` `s` `CategoryTheory.MorphismProperty.LeftFraction.f`	—	`exists_leftFraction`
`leftFraction_fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X'` `f` `CategoryTheory.MorphismProperty.LeftFraction.Y'` `leftFraction` `CategoryTheory.MorphismProperty.LeftFraction.s` `s` `CategoryTheory.MorphismProperty.LeftFraction.f`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `leftFraction_fac`
`map_eq_iff` 📖	mathematical	—	`map` `CategoryTheory.Localization.inverts` `CategoryTheory.MorphismProperty.RightFractionRel`	—	`CategoryTheory.Localization.inverts` `CategoryTheory.MorphismProperty.leftFractionRel_op_iff` `CategoryTheory.Functor.IsLocalization.op` `CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff` `CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions` `CategoryTheory.MorphismProperty.IsInvertedBy.op` `op_map`
`map_hom_ofInv_id` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `map` `ofInv` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.IsIso.hom_inv_id`
`map_hom_ofInv_id_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `map` `ofInv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_hom_ofInv_id`
`map_ofHom` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`map` `ofHom` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.inv.congr_simp` `CategoryTheory.IsIso.inv_id` `CategoryTheory.Category.id_comp`
`map_ofInv_hom_id` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `ofInv` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.IsIso.inv_hom_id`
`map_ofInv_hom_id_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `ofInv` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_ofInv_hom_id`
`map_s_comp_map` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `X'` `CategoryTheory.Functor.map` `s` `map` `f`	—	`CategoryTheory.IsIso.hom_inv_id_assoc`
`map_s_comp_map_assoc` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `X'` `CategoryTheory.Functor.map` `s` `map` `f`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_s_comp_map`
`ofHom_X'` 📖	mathematical	—	`X'` `ofHom`	—	—
`ofHom_f` 📖	mathematical	—	`f` `ofHom`	—	—
`ofHom_s` 📖	mathematical	—	`s` `ofHom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`ofInv_X'` 📖	mathematical	—	`X'` `ofInv`	—	—
`ofInv_f` 📖	mathematical	—	`f` `ofInv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`ofInv_s` 📖	mathematical	—	`s` `ofInv`	—	—
`op_Y'` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.Y'` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `op` `X'`	—	—
`op_f` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.f` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `X'` `f`	—	—
`op_map` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `map` `CategoryTheory.MorphismProperty.LeftFraction.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `Opposite.op` `op` `CategoryTheory.Functor.op` `CategoryTheory.MorphismProperty.IsInvertedBy.op`	—	`CategoryTheory.MorphismProperty.IsInvertedBy.op` `CategoryTheory.isIso_op` `CategoryTheory.op_inv`
`op_s` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.s` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `X'` `s`	—	—
`unop_Y'` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.Y'` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `unop` `X'` `Opposite` `CategoryTheory.Category.opposite`	—	—
`unop_f` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.f` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `X'` `Opposite` `CategoryTheory.Category.opposite` `f`	—	—
`unop_s` 📖	mathematical	—	`CategoryTheory.MorphismProperty.LeftFraction.s` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `X'` `Opposite` `CategoryTheory.Category.opposite` `s`	—	—

CategoryTheory.MorphismProperty.RightFractionRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op` 📖	mathematical	`CategoryTheory.MorphismProperty.RightFractionRel`	`CategoryTheory.MorphismProperty.LeftFractionRel` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MorphismProperty.op` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.MorphismProperty.RightFraction.op`	—	—
`refl` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RightFractionRel`	—	`CategoryTheory.MorphismProperty.LeftFractionRel.unop` `CategoryTheory.MorphismProperty.LeftFractionRel.refl`
`trans` 📖	—	`CategoryTheory.MorphismProperty.RightFractionRel`	—	—	`CategoryTheory.MorphismProperty.LeftFractionRel.unop` `CategoryTheory.MorphismProperty.LeftFractionRel.trans` `CategoryTheory.MorphismProperty.instHasLeftCalculusOfFractionsOppositeOpOfHasRightCalculusOfFractions` `op`
`unop` 📖	mathematical	`CategoryTheory.MorphismProperty.RightFractionRel` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.MorphismProperty.LeftFractionRel` `CategoryTheory.MorphismProperty.unop` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `CategoryTheory.MorphismProperty.RightFraction.unop`	—	—

---

← Back to Index