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.)
theorem
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ
{C : Type u_1}
[CategoryTheory.Category C]
[CategoryTheory.Preadditive C]
{Y : C}
{X : CategoryTheory.SimplicialObject C}
{n b q : Nat}
{φ : Quiver.Hom Y (X.obj { unop := SimplexCategory.mk (HAdd.hAdd n 1) })}
(v : HigherFacesVanish q φ)
(hnbq : Eq (HAdd.hAdd n 1) (HAdd.hAdd b q))
:
HigherFacesVanish q (CategoryTheory.CategoryStruct.comp φ (X.σ ⟨b, ⋯⟩))
theorem
AlgebraicTopology.DoldKan.σ_comp_P_eq_zero
{C : Type u_1}
[CategoryTheory.Category C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
{n q : Nat}
(i : Fin (HAdd.hAdd n 1))
(hi : LE.le (HAdd.hAdd n 1) (HAdd.hAdd i.val q))
:
theorem
AlgebraicTopology.DoldKan.σ_comp_PInfty
{C : Type u_1}
[CategoryTheory.Category C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
{n : Nat}
(i : Fin (HAdd.hAdd n 1))
:
theorem
AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc
{C : Type u_1}
[CategoryTheory.Category C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
{n : Nat}
(i : Fin (HAdd.hAdd n 1))
{Z : C}
(h : Quiver.Hom ((AlternatingFaceMapComplex.obj X).X (HAdd.hAdd n 1)) Z)
:
Eq (CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (PInfty.f (HAdd.hAdd n 1)) h))
(CategoryTheory.CategoryStruct.comp 0 h)
theorem
AlgebraicTopology.DoldKan.degeneracy_comp_PInfty
{C : Type u_1}
[CategoryTheory.Category C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
(n : Nat)
{Δ' : SimplexCategory}
(θ : Quiver.Hom (SimplexCategory.mk n) Δ')
(hθ : Not (CategoryTheory.Mono θ))
:
theorem
AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc
{C : Type u_1}
[CategoryTheory.Category C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
(n : Nat)
{Δ' : SimplexCategory}
(θ : Quiver.Hom (SimplexCategory.mk n) Δ')
(hθ : Not (CategoryTheory.Mono θ))
{Z : C}
(h : Quiver.Hom ((AlternatingFaceMapComplex.obj X).X n) Z)
:
Eq (CategoryTheory.CategoryStruct.comp (X.map θ.op) (CategoryTheory.CategoryStruct.comp (PInfty.f n) h))
(CategoryTheory.CategoryStruct.comp 0 h)