Theorems · Definition · algebraic topology

AlgebraicTopology.DoldKan.P

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        ℕ → (AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X)

This is the inductive definition of the projections P q : K[X] ⟶ K[X], with P 0 := 𝟙 _ and P (q+1) := P q ≫ (𝟙 _ + Hσ q).

Defined in

Mathlib.AlgebraicTopology.DoldKan.Projections

Cited by

38 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive