AlternatingFaceMapComplex

📁 Source: Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Statistics

Metric	Count
Definitions map, obj, objD, map, obj, objD, ε, alternatingCofaceMapComplex, alternatingFaceMapComplex, inclusionOfMooreComplex, inclusionOfMooreComplexMap	11
Theorems d_eq_unop_d, d_squared, d_squared, map_f, obj_X, obj_d_eq, ε_app_f_succ, ε_app_f_zero, alternatingCofaceMapComplex_map, alternatingCofaceMapComplex_obj, alternatingFaceMapComplex_map_f, alternatingFaceMapComplex_obj_X, alternatingFaceMapComplex_obj_d, inclusionOfMooreComplexMap_f, inclusionOfMooreComplex_app, karoubi_alternatingFaceMapComplex_d, map_alternatingFaceMapComplex	17
Total	28

AlgebraicTopology

Definitions

Name	Category	Theorems
alternatingCofaceMapComplex 📖	CompOp	3 math math: CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, alternatingCofaceMapComplex_obj, alternatingCofaceMapComplex_map
alternatingFaceMapComplex 📖	CompOp	22 math math: DoldKan.natTransPInfty_app, DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, AlternatingFaceMapComplex.ε_app_f_succ, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, alternatingFaceMapComplex_obj_d, alternatingFaceMapComplex_map_f, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, AlternatingFaceMapComplex.ε_app_f_zero, inclusionOfMooreComplex_app, DoldKan.inclusionOfMooreComplexMap_comp_PInfty, DoldKan.natTransP_app, map_alternatingFaceMapComplex, DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, DoldKan.natTransPInfty_f_app, DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, inclusionOfMooreComplexMap_f, alternatingFaceMapComplex_obj_X, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, DoldKan.natTransQ_app
inclusionOfMooreComplex 📖	CompOp	1 math math: inclusionOfMooreComplex_app
inclusionOfMooreComplexMap 📖	CompOp	11 math math: DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, inclusionOfMooreComplex_app, DoldKan.inclusionOfMooreComplexMap_comp_PInfty, DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, inclusionOfMooreComplexMap_f, DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatingCofaceMapComplex_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd alternatingCofaceMapComplex AlternatingCofaceMapComplex.map	—	AddRightCancelSemigroup.toIsRightCancelAdd
alternatingCofaceMapComplex_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd alternatingCofaceMapComplex AlternatingCofaceMapComplex.obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
alternatingFaceMapComplex_map_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 HomologicalComplex.instCategory alternatingFaceMapComplex CategoryTheory.Functor.map CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op	—	AddRightCancelSemigroup.toIsRightCancelAdd
alternatingFaceMapComplex_obj_X 📖	mathematical	—	HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 HomologicalComplex.instCategory alternatingFaceMapComplex Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op	—	AddRightCancelSemigroup.toIsRightCancelAdd
alternatingFaceMapComplex_obj_d 📖	mathematical	—	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 HomologicalComplex.instCategory alternatingFaceMapComplex AlternatingFaceMapComplex.objD	—	AddRightCancelSemigroup.toIsRightCancelAdd ChainComplex.of_d AlternatingFaceMapComplex.d_squared
inclusionOfMooreComplexMap_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 HomologicalComplex.instCategory normalizedMooreComplex alternatingFaceMapComplex inclusionOfMooreComplexMap CategoryTheory.Subobject.arrow Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op NormalizedMooreComplex.objX	—	AddRightCancelSemigroup.toIsRightCancelAdd ChainComplex.ofHom_f NormalizedMooreComplex.d_squared
inclusionOfMooreComplex_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd normalizedMooreComplex alternatingFaceMapComplex inclusionOfMooreComplex inclusionOfMooreComplexMap	—	AddRightCancelSemigroup.toIsRightCancelAdd
karoubi_alternatingFaceMapComplex_d 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f HomologicalComplex.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Idempotents.instPreadditiveKaroubi ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlternatingFaceMapComplex.obj CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory HomologicalComplex.d CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi.X CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Idempotents.Karoubi.p	—	AddRightCancelSemigroup.toIsRightCancelAdd AlternatingFaceMapComplex.obj_d_eq CategoryTheory.Idempotents.Karoubi.sum_hom Finset.sum_congr CategoryTheory.Idempotents.Karoubi.zsmul_hom CategoryTheory.Preadditive.comp_sum CategoryTheory.Preadditive.comp_zsmul
map_alternatingFaceMapComplex 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex alternatingFaceMapComplex CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.whiskering	—	CategoryTheory.Functor.ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.ext alternatingFaceMapComplex_obj_d CategoryTheory.Functor.map_sum Finset.sum_congr CategoryTheory.Functor.map_zsmul CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp HomologicalComplex.hom_ext HomologicalComplex.eqToHom_f

AlgebraicTopology.AlternatingCofaceMapComplex

Definitions

Name	Category	Theorems
map 📖	CompOp	1 math math: AlgebraicTopology.alternatingCofaceMapComplex_map
obj 📖	CompOp	1 math math: AlgebraicTopology.alternatingCofaceMapComplex_obj
objD 📖	CompOp	2 math math: d_eq_unop_d, d_squared

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_eq_unop_d 📖	mathematical	—	objD Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Equivalence.functor CategoryTheory.cosimplicialSimplicialEquiv Opposite.op AlgebraicTopology.AlternatingFaceMapComplex.objD CategoryTheory.instPreadditiveOpposite	—	CategoryTheory.unop_sum Finset.sum_congr
d_squared 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory objD Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	d_eq_unop_d AlgebraicTopology.AlternatingFaceMapComplex.d_squared

AlgebraicTopology.AlternatingFaceMapComplex

Definitions

Name	Category	Theorems
map 📖	CompOp	4 math math: AlgebraicTopology.DoldKan.N₁_map_f, map_f, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality
obj 📖	CompOp	107 math math: AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, AlgebraicTopology.DoldKan.P_f_0_eq, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, AlgebraicTopology.DoldKan.N₁_map_f, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, SimplicialObject.Splitting.PInfty_comp_πSummand_id, AlgebraicTopology.DoldKan.PInfty_idem, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, AlgebraicTopology.DoldKan.QInfty_idem, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, AlgebraicTopology.DoldKan.QInfty_idem_assoc, map_f, AlgebraicTopology.DoldKan.QInfty_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, AlgebraicTopology.DoldKan.P_f_idem_assoc, AlgebraicTopology.DoldKan.QInfty_f_0, AlgebraicTopology.DoldKan.map_Hσ, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, AlgebraicTopology.DoldKan.P_f_idem, AlgebraicTopology.DoldKan.PInfty_idem_assoc, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, AlgebraicTopology.DoldKan.map_PInfty_f, AlgebraicTopology.DoldKan.P_succ, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, AlgebraicTopology.DoldKan.Hσ_eq_zero, obj_d_eq, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, AlgebraicTopology.DoldKan.Q_idem_assoc, AlgebraicTopology.DoldKan.PInfty_f, AlgebraicTopology.DoldKan.Q_f_0_eq, AlgebraicTopology.DoldKan.QInfty_f_naturality, AlgebraicTopology.DoldKan.P_f_naturality_assoc, AlgebraicTopology.DoldKan.map_P, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, AlgebraicTopology.DoldKan.P_idem, AlgebraicTopology.DoldKan.N₁_obj_X, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Q_is_eventually_constant, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, AlgebraicTopology.DoldKan.Q_succ, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.hσ'_eq, AlgebraicTopology.DoldKan.MorphComponents.id_a, AlgebraicTopology.DoldKan.PInfty_f_0, AlgebraicTopology.DoldKan.PInfty_f_naturality, AlgebraicTopology.DoldKan.hσ'_eq_zero, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, AlgebraicTopology.DoldKan.P_is_eventually_constant, AlgebraicTopology.DoldKan.map_Q, AlgebraicTopology.DoldKan.PInfty_f_idem, AlgebraicTopology.DoldKan.N₂_obj_p_f, AlgebraicTopology.DoldKan.σ_comp_PInfty, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, AlgebraicTopology.DoldKan.P_zero, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, AlgebraicTopology.DoldKan.karoubi_PInfty_f, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, AlgebraicTopology.DoldKan.QInfty_f_idem, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, AlgebraicTopology.DoldKan.decomposition_Q, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, obj_X, AlgebraicTopology.DoldKan.Q_f_idem_assoc, AlgebraicTopology.DoldKan.Q_f_naturality, AlgebraicTopology.DoldKan.Q_zero, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, AlgebraicTopology.DoldKan.map_hσ', AlgebraicTopology.DoldKan.N₂_map_f_f, AlgebraicTopology.DoldKan.P_f_naturality, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.P_add_Q_f, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, AlgebraicTopology.DoldKan.PInfty_add_QInfty, AlgebraicTopology.DoldKan.Q_f_idem
objD 📖	CompOp	3 math math: AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, AlgebraicTopology.alternatingFaceMapComplex_obj_d, d_squared
ε 📖	CompOp	2 math math: ε_app_f_succ, ε_app_f_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_squared 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op objD Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.Preadditive.comp_sum Finset.sum_congr CategoryTheory.Preadditive.sum_comp Finset.univ_product_univ Finset.sum_add_sum_compl eq_neg_iff_add_eq_zero Finset.sum_neg_distrib lt_of_le_of_lt Finset.mem_filter Finset.sum_bij Finset.compl_filter CategoryTheory.Preadditive.comp_zsmul CategoryTheory.Preadditive.zsmul_comp smul_smul pow_add pow_one mul_neg mul_one neg_neg mul_comm Fin.le_iff_val_le_val CategoryTheory.SimplicialObject.δ_comp_δ''
map_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne obj map CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op	—	AddRightCancelSemigroup.toIsRightCancelAdd
obj_X 📖	mathematical	—	HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne obj CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op	—	AddRightCancelSemigroup.toIsRightCancelAdd
obj_d_eq 📖	mathematical	—	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne obj Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid CategoryTheory.SimplicialObject.δ	—	ChainComplex.of_d d_squared
ε_app_f_succ 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop AlgebraicTopology.alternatingFaceMapComplex CategoryTheory.SimplicialObject.Augmented.point ChainComplex.single₀ CategoryTheory.NatTrans.app ε Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
ε_app_f_zero 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Augmented.drop AlgebraicTopology.alternatingFaceMapComplex CategoryTheory.SimplicialObject.Augmented.point ChainComplex.single₀ CategoryTheory.NatTrans.app ε Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Comma.hom Opposite.op	—	ChainComplex.toSingle₀Equiv_symm_apply_f_zero AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index