Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Split.natTransCofanInj

(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Δ : SimplexCategoryᵒᵖ} →
      (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) →
        CategoryTheory.SimplicialObject.Split.evalN C (Opposite.unop A.fst).len ⟶
          (CategoryTheory.SimplicialObject.Split.forget C).comp ((CategoryTheory.evaluation SimplexCategoryᵒᵖ C).obj Δ)

The inclusion of each summand in the coproduct decomposition of simplices in split simplicial objects is a natural transformation of functors SimplicialObject.Split C ⥤ C

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Split

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category