English
If a morphism φ has the HigherFacesVanish q property, then it also has the HigherFacesVanish (q+1) property after forming the sum with the identity and Hσ_q, i.e., φ ≫ (1 + Hσ_q).f(n+1) still vanishes on higher faces at level q+1.
Русский
Если морфизм φ обладает свойством HigherFacesVanish q, то он сохраняет свойство на уровне q+1 после суммы с идентичностью и Hσ_q, то есть φ ≫ (1 + Hσ_q).f(n+1) продолжает исчезать на высших гранях на уровне q+1.
LaTeX
$$$\text{If } v: \text{HigherFacesVanish}_q(φ),\ then\ HigherFacesVanish_{q+1}(φ \;≫\; (Id + Hσ_q)_{n+1}).$$$
Lean4
theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) (hqn : n < q) :
φ ≫ (Hσ q).f (n + 1) = 0 :=
by
simp only [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl)]
rw [hσ'_eq_zero hqn (c_mk (n + 1) n rfl), comp_zero, zero_add]
by_cases hqn' : n + 1 < q
· rw [hσ'_eq_zero hqn' (c_mk (n + 2) (n + 1) rfl), zero_comp, comp_zero]
· simp only [hσ'_eq (show n + 1 = 0 + q by cutsat) (c_mk (n + 2) (n + 1) rfl), pow_zero, Fin.mk_zero, one_zsmul,
eqToHom_refl, comp_id, comp_sum, AlternatingFaceMapComplex.obj_d_eq]
-- All terms of the sum but the first two are zeros
rw [Fin.sum_univ_succ, Fin.sum_univ_succ, Fintype.sum_eq_zero, add_zero]
·
simp only [Fin.val_zero, Fin.val_succ, Fin.coe_castSucc, zero_add, pow_zero, one_smul, pow_one, neg_smul,
comp_neg, ← Fin.castSucc_zero (n := n + 2), δ_comp_σ_self, δ_comp_σ_succ, add_neg_cancel]
· intro j
rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
· simp [Fin.succ_ne_zero]
· dsimp
cutsat
· simp only [Fin.succ_lt_succ_iff, j.succ_pos]
