SplitSimplicialObject

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

Statistics

Metric	Count
Definitions nondegComplexFunctor, toKaroubiNondegComplexFunctorIsoN₁, d, nondegComplex, toKaroubiNondegComplexIsoN₁, πSummand	6
Theorems nondegComplexFunctor_map_f, nondegComplexFunctor_obj, toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, PInfty_comp_πSummand_id, PInfty_comp_πSummand_id_assoc, cofan_inj_comp_PInfty_eq_zero, cofan_inj_πSummand_eq_id, cofan_inj_πSummand_eq_id_assoc, cofan_inj_πSummand_eq_zero, cofan_inj_πSummand_eq_zero_assoc, comp_PInfty_eq_zero_iff, decomposition_id, nondegComplex_X, nondegComplex_d, toKaroubiNondegComplexIsoN₁_hom_f_f, toKaroubiNondegComplexIsoN₁_inv_f_f, ιSummand_comp_d_comp_πSummand_eq_zero, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, σ_comp_πSummand_id_eq_zero, σ_comp_πSummand_id_eq_zero_assoc	22
Total	28

SimplicialObject.Split

Definitions

Name	Category	Theorems
nondegComplexFunctor 📖	CompOp	4 math math: toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, nondegComplexFunctor_map_f, nondegComplexFunctor_obj, toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f
toKaroubiNondegComplexFunctorIsoN₁ 📖	CompOp	2 math math: toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nondegComplexFunctor_map_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne SimplicialObject.Splitting.nondegComplex X s CategoryTheory.Functor.map SimplicialObject.Split SimplicialObject.instCategorySplit ChainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd nondegComplexFunctor Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
nondegComplexFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplicialObject.Split SimplicialObject.instCategorySplit ChainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd nondegComplexFunctor SimplicialObject.Splitting.nondegComplex X s	—	AddRightCancelSemigroup.toIsRightCancelAdd
toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.toKaroubi SimplicialObject.Splitting.nondegComplex X s CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject AlgebraicTopology.DoldKan.N₁ CategoryTheory.Idempotents.Karoubi.Hom.f SimplicialObject.Split SimplicialObject.instCategorySplit CategoryTheory.Functor.comp nondegComplexFunctor forget CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category toKaroubiNondegComplexFunctorIsoN₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct SimplicialObject.Splitting.N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete SimplicialObject.Splitting.IndexSet Opposite.op SimplexCategory CategoryTheory.discreteCategory CategoryTheory.Discrete.functor SimplicialObject.Splitting.summand SimplicialObject.Splitting.cofan Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory SimplicialObject.Splitting.IndexSet.id AlgebraicTopology.AlternatingFaceMapComplex.obj AlgebraicTopology.DoldKan.PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd
toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory AlgebraicTopology.DoldKan.N₁ X CategoryTheory.Idempotents.toKaroubi SimplicialObject.Splitting.nondegComplex s CategoryTheory.Idempotents.Karoubi.Hom.f SimplicialObject.Split SimplicialObject.instCategorySplit CategoryTheory.Functor.comp forget nondegComplexFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category toKaroubiNondegComplexFunctorIsoN₁ SimplicialObject.Splitting.πSummand Opposite.op SimplexCategory SimplicialObject.Splitting.IndexSet.id	—	AddRightCancelSemigroup.toIsRightCancelAdd

SimplicialObject.Splitting

Definitions

Name	Category	Theorems
d 📖	CompOp	1 math math: nondegComplex_d
nondegComplex 📖	CompOp	15 math math: AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, nondegComplex_d, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, toKaroubiNondegComplexIsoN₁_inv_f_f, nondegComplex_X, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, SimplicialObject.Split.nondegComplexFunctor_map_f, SimplicialObject.Split.nondegComplexFunctor_obj, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_app
toKaroubiNondegComplexIsoN₁ 📖	CompOp	7 math math: AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, toKaroubiNondegComplexIsoN₁_inv_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_app
πSummand 📖	CompOp	15 math math: cofan_inj_πSummand_eq_id_assoc, PInfty_comp_πSummand_id, ιSummand_comp_d_comp_πSummand_eq_zero, toKaroubiNondegComplexIsoN₁_inv_f_f, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, cofan_inj_πSummand_eq_id, cofan_inj_πSummand_eq_zero, σ_comp_πSummand_id_eq_zero_assoc, PInfty_comp_πSummand_id_assoc, decomposition_id, πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, cofan_inj_πSummand_eq_zero_assoc, comp_PInfty_eq_zero_iff, σ_comp_πSummand_id_eq_zero, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PInfty_comp_πSummand_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj N SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory Opposite.op CategoryTheory.Epi IndexSet.id HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty πSummand	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp sub_eq_zero CategoryTheory.Preadditive.sub_comp comp_PInfty_eq_zero_iff AlgebraicTopology.DoldKan.PInfty_f_idem sub_self
PInfty_comp_πSummand_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty N SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi IndexSet.id Opposite.op πSummand	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' PInfty_comp_πSummand_id
cofan_inj_comp_PInfty_eq_zero 📖	mathematical	IndexSet.EqId Opposite.op SimplexCategory	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd cofan_inj_eq CategoryTheory.Category.assoc AlgebraicTopology.DoldKan.degeneracy_comp_PInfty IndexSet.eqId_iff_mono CategoryTheory.Limits.comp_zero
cofan_inj_πSummand_eq_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi πSummand CategoryTheory.CategoryStruct.id	—	ι_desc
cofan_inj_πSummand_eq_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi πSummand	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_πSummand_eq_id
cofan_inj_πSummand_eq_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi πSummand CategoryTheory.Limits.HasZeroMorphisms.zero	—	ι_desc
cofan_inj_πSummand_eq_zero_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan SimplexCategory.len Opposite.unop SimplexCategory Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi πSummand CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_πSummand_eq_zero
comp_PInfty_eq_zero_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero N SimplexCategory.len Opposite.unop CategoryTheory.Epi IndexSet.id πSummand	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id CategoryTheory.Limits.zero_comp CategoryTheory.whisker_eq AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f zero_add CategoryTheory.Preadditive.comp_add CategoryTheory.Category.assoc AlgebraicTopology.DoldKan.QInfty_f AlgebraicTopology.DoldKan.decomposition_Q CategoryTheory.Preadditive.sum_comp CategoryTheory.Preadditive.comp_sum Finset.sum_eq_zero σ_comp_πSummand_id_eq_zero CategoryTheory.Limits.comp_zero decomposition_id Fintype.sum_eq_zero Mathlib.Tactic.Reassoc.eq_whisker' cofan_inj_comp_PInfty_eq_zero
decomposition_id 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Finset.sum IndexSet Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor summand N cofan AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.univ IndexSet.instFintype CategoryTheory.CategoryStruct.comp SimplexCategory.len Opposite.unop CategoryTheory.Epi πSummand CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	hom_ext' CategoryTheory.Category.comp_id CategoryTheory.Preadditive.comp_sum Finset.sum_eq_single cofan_inj_πSummand_eq_zero_assoc CategoryTheory.Limits.zero_comp cofan_inj_πSummand_eq_id_assoc instIsEmptyFalse
nondegComplex_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 nondegComplex N	—	AddRightCancelSemigroup.toIsRightCancelAdd
nondegComplex_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 nondegComplex d	—	AddRightCancelSemigroup.toIsRightCancelAdd
toKaroubiNondegComplexIsoN₁_hom_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.toKaroubi nondegComplex CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject AlgebraicTopology.DoldKan.N₁ CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Iso.hom AddRightCancelSemigroup.toIsRightCancelAdd toKaroubiNondegComplexIsoN₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet Opposite.op SimplexCategory CategoryTheory.discreteCategory CategoryTheory.Discrete.functor summand N cofan IndexSet.id AlgebraicTopology.AlternatingFaceMapComplex.obj AlgebraicTopology.DoldKan.PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd
toKaroubiNondegComplexIsoN₁_inv_f_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Idempotents.Karoubi.X ChainComplex HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory AlgebraicTopology.DoldKan.N₁ CategoryTheory.Idempotents.toKaroubi nondegComplex CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Iso.inv AddRightCancelSemigroup.toIsRightCancelAdd toKaroubiNondegComplexIsoN₁ πSummand Opposite.op SimplexCategory IndexSet.id	—	AddRightCancelSemigroup.toIsRightCancelAdd
ιSummand_comp_d_comp_πSummand_eq_zero 📖	mathematical	IndexSet.EqId Opposite.op SimplexCategory	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct summand N CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor cofan SimplexCategory.len Opposite.unop Opposite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SimplexCategory.smallCategory CategoryTheory.Epi IndexSet.id HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.d πSummand CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc comp_PInfty_eq_zero_iff HomologicalComplex.Hom.comm cofan_inj_eq AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc IndexSet.eqId_iff_mono CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi IndexSet.id HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj πSummand CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor summand cofan HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp decomposition_id CategoryTheory.Preadditive.sum_comp Fintype.sum_eq_single CategoryTheory.Category.assoc cofan_inj_comp_PInfty_eq_zero CategoryTheory.Limits.comp_zero
πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi IndexSet.id πSummand CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete IndexSet CategoryTheory.discreteCategory CategoryTheory.Discrete.functor summand cofan HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AlgebraicTopology.AlternatingFaceMapComplex.obj HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty
σ_comp_πSummand_id_eq_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi IndexSet.id CategoryTheory.SimplicialObject.σ πSummand CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	hom_ext' CategoryTheory.Limits.comp_zero CategoryTheory.unop_epi_of_mono CategoryTheory.op_mono_of_epi SimplexCategory.instEpiσ cofan_inj_epi_naturality_assoc cofan_inj_πSummand_eq_zero IndexSet.eqId_iff_len_eq SimplexCategory.len_le_of_epi IndexSet.instEpiSimplexCategoryE
σ_comp_πSummand_id_eq_zero_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.SimplicialObject.σ N SimplexCategory.len Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Epi IndexSet.id πSummand CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_comp_πSummand_id_eq_zero

---

← Back to Index