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 θ) :