Fractions

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/Fractions.lean

Statistics

Metric	Count
Definitions	0
Theorems instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, left_fac, left_fac_of_isStrictlyGE, left_fac_of_isStrictlyLE_of_isStrictlyGE, right_fac, right_fac_of_isStrictlyLE, right_fac_of_isStrictlyLE_of_isStrictlyGE, subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE	9
Total	9

DerivedCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.quasiIso CategoryTheory.categoryWithHomology_of_abelian	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic
instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.HasRightCalculusOfFractions HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.quasiIso CategoryTheory.categoryWithHomology_of_abelian	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W CategoryTheory.ObjectProperty.instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic
left_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CategoryTheory.Functor.map CategoryTheory.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Localization.inverts instIsLocalizationHomotopyCategoryIntUpQhQuasiIso CategoryTheory.Localization.exists_leftFraction instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso CategoryTheory.MorphismProperty.LeftFraction.cases HomotopyCategory.quotient_obj_surjective CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient isIso_Qh_map_iff
left_fac_of_isStrictlyGE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CategoryTheory.Functor.map CategoryTheory.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd left_fac CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian isIso_Q_map_iff_quasiIso HomologicalComplex.truncGE.instHasHomology ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE CochainComplex.quasiIso_truncGEMap_iff QuasiIso.quasiIsoAt HomologicalComplex.instIsStrictlySupportedTruncGE CategoryTheory.Functor.map_comp CategoryTheory.IsIso.comp_isIso instIsIsoMapCochainComplexIntQ CochainComplex.instQuasiIsoIntπTruncGEOfIsGE HomologicalComplex.instIsSupportedOfIsStrictlySupported CategoryTheory.Functor.congr_map CochainComplex.πTruncGE_naturality CategoryTheory.inv.congr_simp CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.instIsSplitMonoMap CategoryTheory.IsSplitMono.of_iso CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.IsIso.inv_hom_id_assoc
left_fac_of_isStrictlyLE_of_isStrictlyGE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CategoryTheory.Functor.map CategoryTheory.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd left_fac_of_isStrictlyGE CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian isIso_Q_map_iff_quasiIso HomologicalComplex.instHasHomologyTruncLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE CochainComplex.quasiIso_truncLEMap_iff QuasiIso.quasiIsoAt HomologicalComplex.instIsStrictlySupportedTruncLE_1 HomologicalComplex.instIsStrictlySupportedTruncLE CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE CategoryTheory.Functor.map_comp CategoryTheory.IsIso.comp_isIso instIsIsoMapCochainComplexIntQ quasiIso_of_isIso CategoryTheory.IsIso.inv_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_comp CategoryTheory.IsIso.inv_inv CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id CochainComplex.ιTruncLE_naturality CategoryTheory.IsIso.inv_hom_id_assoc
right_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CategoryTheory.inv CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Localization.inverts instIsLocalizationHomotopyCategoryIntUpQhQuasiIso CategoryTheory.Localization.exists_rightFraction instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso CategoryTheory.MorphismProperty.RightFraction.cases HomotopyCategory.quotient_obj_surjective CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient isIso_Qh_map_iff
right_fac_of_isStrictlyLE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CategoryTheory.inv CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd right_fac CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian isIso_Q_map_iff_quasiIso HomologicalComplex.instHasHomologyTruncLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE CochainComplex.quasiIso_truncLEMap_iff QuasiIso.quasiIsoAt HomologicalComplex.instIsStrictlySupportedTruncLE CategoryTheory.Functor.map_comp CategoryTheory.IsIso.comp_isIso instIsIsoMapCochainComplexIntQ CochainComplex.instQuasiIsoIntιTruncLEOfIsLE HomologicalComplex.instIsSupportedOfIsStrictlySupported CochainComplex.ιTruncLE_naturality CategoryTheory.inv.congr_simp CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id_assoc
right_fac_of_isStrictlyLE_of_isStrictlyGE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp DerivedCategory CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q CategoryTheory.inv CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd right_fac_of_isStrictlyLE CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian isIso_Q_map_iff_quasiIso HomologicalComplex.truncGE.instHasHomology ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE CochainComplex.quasiIso_truncGEMap_iff QuasiIso.quasiIsoAt HomologicalComplex.instIsStrictlySupportedTruncGE HomologicalComplex.instIsStrictlySupportedTruncGE_1 CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE CategoryTheory.Functor.map_comp CategoryTheory.IsIso.comp_isIso instIsIsoMapCochainComplexIntQ quasiIso_of_isIso CategoryTheory.IsIso.inv_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.inv.congr_simp CategoryTheory.IsIso.inv_comp CategoryTheory.IsIso.inv_inv CategoryTheory.Category.assoc CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.hom_inv_id_assoc CategoryTheory.Functor.map_comp_assoc CochainComplex.πTruncGE_naturality CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE 📖	mathematical	—	Quiver.Hom DerivedCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd Q	—	AddRightCancelSemigroup.toIsRightCancelAdd right_fac_of_isStrictlyLE HomologicalComplex.hom_ext CategoryTheory.Limits.IsZero.eq_of_src CochainComplex.isZero_of_isStrictlyLE CategoryTheory.Limits.IsZero.eq_of_tgt CochainComplex.isZero_of_isStrictlyGE CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveCochainComplexIntQ CategoryTheory.Limits.comp_zero

---

← Back to Index