Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Splitting.d

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) → [CategoryTheory.Preadditive C] → (i j : ℕ) → s.N i ⟶ s.N j

The differentials s.d i j : s.N i ⟶ s.N j on nondegenerate simplices of a split simplicial object are induced by the differentials on the alternating face map complex.

Defined in

Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive