English
For any chain complex K and integer n, certain higher face maps vanish on the Γ₀-splitting summand of K, reflecting the acyclicity of higher faces in the Dold–Kan correspondence.
Русский
Для любого цепного комплекса K и целого n вершины высших граней на разложении Γ₀-санитирования суммирования равны нулю, что отражает ацикличность высших граней в соответствии Долд-Кана.
LaTeX
$$$\text{HigherFacesVanish}_{\Gamma_0,\text{summand}}(K,n) \;: \text{some composition equals zero on the summand.}$$$
Lean4
theorem on_Γ₀_summand_id (K : ChainComplex C ℕ) (n : ℕ) :
@HigherFacesVanish C _ _ (Γ₀.obj K) _ n (n + 1)
(((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n + 1⦌))) :=
by
intro j _
have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq; rotate_left
· intro h
exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)
· exact fun h => Fin.succ_ne_zero j (by simpa only [Isδ₀.iff] using h)
exact eq
