Mathlib Map

Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Splitting.summand

{C : Type u_1} → (ℕ → C) → (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ → C

Given a sequences of objects N : ℕ → C in a category C, this is a family of objects indexed by the elements A : Splitting.IndexSet Δ. The Δ-simplices of a split simplicial objects shall identify to the coproduct of objects in such a family.

Defined in
Mathlib.AlgebraicTopology.SimplicialObject.Split
Cited by
48 results in Mathlib
Foundations
Depth 31 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.SimplicialObject.Splitting.cofan · cited by 46Splitting.cofanAlgebraicTopology.DoldKan.Γ₀.splitting · cited by 31Γ₀.splittingCategoryTheory.SimplicialObject.Splitting.hom_ext' · cited by 5Splitting.hom_ext'CategoryTheory.SimplicialObject.Splitting.ι_desc · cited by 5Splitting.ι_descCategoryTheory.SimplicialObject.Splitting.cofan_inj_eq · cited by 4Splitting.cofan_inj_eqAlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand · cited by 4Obj.map_on_summandCategoryTheory.SimplicialObject.Splitting.cofan' · cited by 3Splitting.cofan'CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero · cited by 2Splitting.cofan_inj_comp_…CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_app · cited by 2Splitting.cofan_inj_comp_…CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero · cited by 2Splitting.cofan_inj_πSumm…CategoryTheory.SimplicialObject.Splitting.decomposition_id · cited by 2Splitting.decomposition_idAlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self · cited by 2DoldKan.PInfty_on_Γ₀_spli…AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc · cited by 2DoldKan.PInfty_on_Γ₀_spli…CategoryTheory.SimplicialObject.Splitting.isColimit · cited by 2Splitting.isColimitCategoryTheory.SimplicialObject.Splitting.ι_desc_assoc · cited by 2Splitting.ι_desc_assocOpposite · cited by 8081OppositeOpposite.unop · cited by 2231Opposite.unopSimplexCategory · cited by 2204SimplexCategorySimplexCategory.len · cited by 542SimplexCategory.lenCategoryTheory.SimplicialObject.Splitting.IndexSet · cited by 65Splitting.IndexSetSplitting.summandCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by56

Results whose statement or proof uses this declaration.