Behaviour of P_infty with respect to degeneracies #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For any X : simplicial_object C where C is an abelian category,
the projector P_infty : 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 : simplicial_object C with C a preadditive category,
θ : [n] ⟶ Δ' is a non injective map in simplex_category, 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.
theorem
algebraic_topology.dold_kan.higher_faces_vanish.comp_σ
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{Y : C}
{X : category_theory.simplicial_object C}
{n b q : ℕ}
{φ : Y ⟶ X.obj (opposite.op (simplex_category.mk (n + 1)))}
(v : algebraic_topology.dold_kan.higher_faces_vanish q φ)
(hnbq : n + 1 = b + q) :
algebraic_topology.dold_kan.higher_faces_vanish q (φ ≫ X.σ ⟨b, _⟩)
theorem
algebraic_topology.dold_kan.σ_comp_P_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{n q : ℕ}
(i : fin (n + 1))
(hi : n + 1 ≤ ↑i + q) :
@[simp]
theorem
algebraic_topology.dold_kan.σ_comp_P_infty_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{n : ℕ}
(i : fin (n + 1))
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X (n + 1) ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.σ_comp_P_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
{n : ℕ}
(i : fin (n + 1)) :
theorem
algebraic_topology.dold_kan.degeneracy_comp_P_infty_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
(n : ℕ)
{Δ' : simplex_category}
(θ : simplex_category.mk n ⟶ Δ')
(hθ : ¬category_theory.mono θ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
theorem
algebraic_topology.dold_kan.degeneracy_comp_P_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.simplicial_object C)
(n : ℕ)
{Δ' : simplex_category}
(θ : simplex_category.mk n ⟶ Δ')
(hθ : ¬category_theory.mono θ) :