Behaviour of `P_infty` with respect to degeneracies #

For any X : SimplicialObject C where C is an abelian category, the projector PInfty : K[X] ⟶ K[X] is supposed to be the projection on the normalized subcomplex, parallel to the degenerate subcomplex, i.e. the subcomplex generated by the images of all X.σ i.

In this file, we obtain degeneracy_comp_P_infty which states that if X : SimplicialObject C with C a preadditive category, θ : ⦋n⦌ ⟶ Δ' is a non-injective map in SimplexCategory, then X.map θ.op ≫ P_infty.f n = 0. It follows from the more precise statement vanishing statement σ_comp_P_eq_zero for the P q.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

source

theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {Y : C} {X : CategoryTheory.SimplicialObject C} {n b q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })} (v : HigherFacesVanish q φ) (hnbq : n + 1 = b + q) :

HigherFacesVanish q (CategoryTheory.CategoryStruct.comp φ (X.σ ⟨b, ⋯⟩))

source

theorem AlgebraicTopology.DoldKan.σ_comp_P_eq_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {n q : ℕ} (i : Fin (n + 1)) (hi : n + 1 ≤ ↑i + q) :

CategoryTheory.CategoryStruct.comp (X.σ i) ((P q).f (n + 1)) = 0

source

@[simp]

theorem AlgebraicTopology.DoldKan.σ_comp_PInfty {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) :

CategoryTheory.CategoryStruct.comp (X.σ i) (PInfty.f (n + 1)) = 0

source

@[simp]

theorem AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) {Z : C} (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (PInfty.f (n + 1)) h) = CategoryTheory.CategoryStruct.comp 0 h

source

theorem AlgebraicTopology.DoldKan.degeneracy_comp_PInfty {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory} (θ : { len := n } ⟶ Δ') (hθ : ¬CategoryTheory.Mono θ) :

CategoryTheory.CategoryStruct.comp (X.map θ.op) (PInfty.f n) = 0

source

theorem AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory} (θ : { len := n } ⟶ Δ') (hθ : ¬CategoryTheory.Mono θ) {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (X.map θ.op) (CategoryTheory.CategoryStruct.comp (PInfty.f n) h) = CategoryTheory.CategoryStruct.comp 0 h

source

def AlgebraicTopology.DoldKan.DegeneraciesVanish {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {n : ℕ} {T : C} (f : X.obj (Opposite.op { len := n }) ⟶ T) :

Prop

If X is a simplicial object in a preadditive category and f : X _⦋n⦌ ⟶ T is a morphism, we say that is vanishes on degeneracies if n = 0 or if maps X.σ i ≫ f all vanish.

Equations