Localization

📁 Source: Mathlib/Algebra/Homology/Localization.lean

Statistics

Metric	Count
Definitions instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso, instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso, mapHomologicalComplexUpToQuasiIso, mapHomologicalComplexUpToQuasiIsoFactors, mapHomologicalComplexUpToQuasiIsoFactorsh, mapHomologicalComplexUpToQuasiIsoLocalizerMorphism, QFactorsThroughHomotopy, strictUniversalPropertyFixedTargetQuotient, HomologicalComplexUpToQuasiIso, Q, Qh, homologyFunctor, homologyFunctorFactors, homologyFunctorFactorsh, quotientCompQhIso, quasiIso	16
Theorems mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor, mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, areEqualizedByLocalization, QFactorsThroughHomotopy_of_exists_prev, quotient_isLocalization, homologyFunctor_inverts_quasiIso, Q_inverts_homotopyEquivalences, Q_map_eq_of_homotopy, Qh_inverts_quasiIso, instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, instIsLocalizationHomotopyCategoryQhQuasiIso, isIso_Q_map_iff_mem_quasiIso, homologyFunctor_inverts_quasiIso, mem_quasiIso_iff, quasiIso_eq_quasiIso_map_quotient, quotient_map_mem_quasiIso_iff, respectsIso_quasiIso, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, instQFactorsThroughHomotopyDown, instQFactorsThroughHomotopyIntUp	23
Total	39

CategoryTheory.Functor

Definitions

Name	Category	Theorems
instLiftingHomologicalComplexHomologicalComplexUpToQuasiIsoQQuasiIsoCompMapHomologicalComplexMapHomologicalComplexUpToQuasiIso 📖	CompOp	—
instLiftingHomotopyCategoryHomologicalComplexUpToQuasiIsoQhQuasiIsoCompMapHomotopyCategoryMapHomologicalComplexUpToQuasiIso 📖	CompOp	—
mapHomologicalComplexUpToQuasiIso 📖	CompOp	2 math math: mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
mapHomologicalComplexUpToQuasiIsoFactors 📖	CompOp	2 math math: mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
mapHomologicalComplexUpToQuasiIsoFactorsh 📖	CompOp	2 math math: mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
mapHomologicalComplexUpToQuasiIsoLocalizerMorphism 📖	CompOp	1 math math: mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopyCategory instCategoryHomotopyCategory HomologicalComplexUpToQuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.quasiIso comp HomologicalComplexUpToQuasiIso.Qh mapHomologicalComplexUpToQuasiIso mapHomotopyCategory CategoryTheory.Iso.hom CategoryTheory.Functor category mapHomologicalComplexUpToQuasiIsoFactorsh obj HomotopyCategory.quotient CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplexUpToQuasiIso.Q map HomologicalComplexUpToQuasiIso.quotientCompQhIso mapHomologicalComplex preservesZeroMorphisms_of_additive mapHomologicalComplexUpToQuasiIsoFactors CategoryTheory.Iso.inv mapHomotopyCategoryFactors	—	preservesZeroMorphisms_of_additive CategoryTheory.Localization.liftNatTrans_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp map_id
mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplexUpToQuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.quasiIso obj mapHomologicalComplexUpToQuasiIso HomotopyCategory instCategoryHomotopyCategory HomologicalComplexUpToQuasiIso.Qh HomotopyCategory.quotient mapHomotopyCategory CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category mapHomologicalComplexUpToQuasiIsoFactorsh HomologicalComplexUpToQuasiIso.Q map HomologicalComplexUpToQuasiIso.quotientCompQhIso mapHomologicalComplex preservesZeroMorphisms_of_additive mapHomologicalComplexUpToQuasiIsoFactors CategoryTheory.Iso.inv mapHomotopyCategoryFactors	—	preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex.quasiIso mapHomologicalComplexUpToQuasiIsoLocalizerMorphism mapHomologicalComplex preservesZeroMorphisms_of_additive	—	preservesZeroMorphisms_of_additive
mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplexUpToQuasiIso CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex.quasiIso comp mapHomologicalComplex preservesZeroMorphisms_of_additive HomologicalComplexUpToQuasiIso.Q	—	preservesZeroMorphisms_of_additive CategoryTheory.LocalizerMorphism.inverts CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'

ComplexShape

Definitions

Name	Category	Theorems
QFactorsThroughHomotopy 📖	CompData	3 math math: instQFactorsThroughHomotopyIntUp, QFactorsThroughHomotopy_of_exists_prev, instQFactorsThroughHomotopyDown
strictUniversalPropertyFixedTargetQuotient 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
QFactorsThroughHomotopy_of_exists_prev 📖	mathematical	Rel	QFactorsThroughHomotopy	—	Homotopy.map_eq_of_inverts_homotopyEquivalences CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.instHasHomotopyCofiberOfHasBinaryBiproducts HomologicalComplex.instHasBinaryBiproduct CategoryTheory.MorphismProperty.IsInvertedBy.of_le CategoryTheory.Localization.inverts CategoryTheory.Functor.q_isLocalization homotopyEquivalences_le_quasiIso
quotient_isLocalization 📖	mathematical	Rel	CategoryTheory.Functor.IsLocalization HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory HomotopyCategory.quotient HomologicalComplex.homotopyEquivalences	—	CategoryTheory.Functor.IsLocalization.mk'

ComplexShape.QFactorsThroughHomotopy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
areEqualizedByLocalization 📖	mathematical	—	CategoryTheory.AreEqualizedByLocalization HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex.quasiIso	—	—

HomologicalComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyFunctor_inverts_quasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomologicalComplex instCategory quasiIso homologyFunctor	—	instIsIsoHomologyMapOfQuasiIsoAt QuasiIso.quasiIsoAt CategoryTheory.CategoryWithHomology.hasHomology mem_quasiIso_iff

HomologicalComplexUpToQuasiIso

Definitions

Name	Category	Theorems
Q 📖	CompOp	6 math math: CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, Q_inverts_homotopyEquivalences, CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, Q_map_eq_of_homotopy, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, isIso_Q_map_iff_mem_quasiIso
Qh 📖	CompOp	5 math math: CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, Qh_inverts_quasiIso, instIsLocalizationHomotopyCategoryQhQuasiIso, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
homologyFunctor 📖	CompOp	—
homologyFunctorFactors 📖	CompOp	—
homologyFunctorFactorsh 📖	CompOp	—
quotientCompQhIso 📖	CompOp	2 math math: CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Q_inverts_homotopyEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplexUpToQuasiIso CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex.quasiIso HomologicalComplex.homotopyEquivalences Q	—	CategoryTheory.MorphismProperty.IsInvertedBy.of_le CategoryTheory.Localization.inverts CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q' homotopyEquivalences_le_quasiIso
Q_map_eq_of_homotopy 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplexUpToQuasiIso CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex.quasiIso Q	—	CategoryTheory.AreEqualizedByLocalization.map_eq ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'
Qh_inverts_quasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomotopyCategory instCategoryHomotopyCategory HomologicalComplexUpToQuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.quasiIso HomotopyCategory.quasiIso Qh	—	CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient HomotopyCategory.quotient_map_mem_quasiIso_iff isIso_Q_map_iff_mem_quasiIso CategoryTheory.NatIso.isIso_map_iff
instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplexUpToQuasiIso HomologicalComplex.instCategory CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex.quasiIso CategoryTheory.Functor.comp HomotopyCategory instCategoryHomotopyCategory HomotopyCategory.quotient Qh	—	CategoryTheory.Functor.IsLocalization.of_iso CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'
instIsLocalizationHomotopyCategoryQhQuasiIso 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopyCategory HomologicalComplexUpToQuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategoryHomotopyCategory CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.quasiIso Qh HomotopyCategory.quasiIso	—	CategoryTheory.Functor.IsLocalization.of_comp instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso homotopyEquivalences_le_quasiIso HomotopyCategory.quasiIso_eq_quasiIso_map_quotient
isIso_Q_map_iff_mem_quasiIso 📖	mathematical	—	CategoryTheory.IsIso HomologicalComplexUpToQuasiIso CategoryTheory.MorphismProperty.instCategoryLocalization' HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.Functor.obj Q CategoryTheory.Functor.map	—	CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.mem_quasiIso_iff quasiIso_iff quasiIsoAt_iff_isIso_homologyMap CategoryTheory.NatIso.isIso_map_iff CategoryTheory.Functor.map_isIso CategoryTheory.Localization.inverts CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'

HomotopyCategory

Definitions

Name	Category	Theorems
quasiIso 📖	CompOp	12 math math: respectsIso_quasiIso, quasiIso_eq_quasiIso_map_quotient, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, mem_quasiIso_iff, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, quasiIso_eq_subcategoryAcyclic_W, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, homologyFunctor_inverts_quasiIso, DerivedCategory.isIso_Qh_map_iff, quotient_map_mem_quasiIso_iff, DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyFunctor_inverts_quasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomotopyCategory instCategoryHomotopyCategory quasiIso homologyFunctor	—	—
mem_quasiIso_iff 📖	mathematical	—	quasiIso CategoryTheory.IsIso CategoryTheory.Functor.obj HomotopyCategory instCategoryHomotopyCategory homologyFunctor CategoryTheory.Functor.map	—	—
quasiIso_eq_quasiIso_map_quotient 📖	mathematical	—	quasiIso CategoryTheory.MorphismProperty.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory HomologicalComplex.quasiIso quotient	—	CategoryTheory.MorphismProperty.ext CategoryTheory.Functor.map_surjective instFullHomologicalComplexQuotient CategoryTheory.MorphismProperty.map_mem_map quotient_map_mem_quasiIso_iff CategoryTheory.MorphismProperty.arrow_mk_iso_iff respectsIso_quasiIso
quotient_map_mem_quasiIso_iff 📖	mathematical	—	quasiIso CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient CategoryTheory.Functor.map HomologicalComplex.quasiIso	—	CategoryTheory.NatIso.isIso_map_iff CategoryTheory.CategoryWithHomology.hasHomology
respectsIso_quasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso HomotopyCategory instCategoryHomotopyCategory quasiIso	—	CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms

(root)

Definitions

Name	Category	Theorems
HomologicalComplexUpToQuasiIso 📖	CompOp	9 math math: CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences, CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory HomotopyCategory.quotient HomologicalComplex.homotopyEquivalences	—	ComplexShape.quotient_isLocalization AddRightCancelSemigroup.toIsRightCancelAdd
instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory HomotopyCategory.quotient HomologicalComplex.homotopyEquivalences	—	ComplexShape.quotient_isLocalization AddRightCancelSemigroup.toIsRightCancelAdd sub_add_cancel
instQFactorsThroughHomotopyDown 📖	mathematical	—	ComplexShape.QFactorsThroughHomotopy ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	ComplexShape.QFactorsThroughHomotopy_of_exists_prev AddRightCancelSemigroup.toIsRightCancelAdd
instQFactorsThroughHomotopyIntUp 📖	mathematical	—	ComplexShape.QFactorsThroughHomotopy ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	ComplexShape.QFactorsThroughHomotopy_of_exists_prev AddRightCancelSemigroup.toIsRightCancelAdd sub_add_cancel

---

← Back to Index