Theorems · Definition · algebraic topology

AlgebraicTopology.DoldKan.PInfty

{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

The endomorphism PInfty : K[X] ⟶ K[X] obtained from the P q by passing to the limit.

Defined in

Mathlib.AlgebraicTopology.DoldKan.PInfty

Cited by

94 results in Mathlib

Foundations

Depth 86 from the axioms, rests on 2,468 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive