HomotopyEquivalence

📁 Source: Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean

Statistics

Metric	Count
Definitions homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex, homotopyPInftyToId, homotopyPToId, homotopyQToZero	4
Theorems homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, homotopyPInftyToId_hom, homotopyPToId_eventually_constant	6
Total	10

AlgebraicTopology.DoldKan

Definitions

Name	Category	Theorems
homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex 📖	CompOp	4 math math: homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom
homotopyPInftyToId 📖	CompOp	2 math math: homotopyPInftyToId_hom, homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId
homotopyPToId 📖	CompOp	2 math math: homotopyPInftyToId_hom, homotopyPToId_eventually_constant
homotopyQToZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom 📖	mathematical	—	HomotopyEquiv.hom CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory AlgebraicTopology.normalizedMooreComplex AlgebraicTopology.alternatingFaceMapComplex homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex AlgebraicTopology.inclusionOfMooreComplexMap	—	AddRightCancelSemigroup.toIsRightCancelAdd
homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId 📖	mathematical	—	HomotopyEquiv.homotopyHomInvId CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory AlgebraicTopology.normalizedMooreComplex AlgebraicTopology.alternatingFaceMapComplex homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex Homotopy.ofEq CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct AlgebraicTopology.inclusionOfMooreComplexMap PInftyToNormalizedMooreComplex CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd
homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId 📖	mathematical	—	HomotopyEquiv.homotopyInvHomId CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory AlgebraicTopology.normalizedMooreComplex AlgebraicTopology.alternatingFaceMapComplex homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex Homotopy.trans CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct PInftyToNormalizedMooreComplex AlgebraicTopology.inclusionOfMooreComplexMap PInfty CategoryTheory.CategoryStruct.id Homotopy.ofEq PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap homotopyPInftyToId	—	AddRightCancelSemigroup.toIsRightCancelAdd
homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv 📖	mathematical	—	HomotopyEquiv.inv CategoryTheory.Abelian.toPreadditive ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory AlgebraicTopology.normalizedMooreComplex AlgebraicTopology.alternatingFaceMapComplex homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex PInftyToNormalizedMooreComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd
homotopyPInftyToId_hom 📖	mathematical	—	Homotopy.hom ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj PInfty CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory homotopyPInftyToId P homotopyPToId	—	AddRightCancelSemigroup.toIsRightCancelAdd
homotopyPToId_eventually_constant 📖	mathematical	—	Homotopy.hom ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj P CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory homotopyPToId	—	AddRightCancelSemigroup.toIsRightCancelAdd hσ'_eq_zero CategoryTheory.Limits.comp_zero add_zero zero_add

---

← Back to Index