English
Let φ have the HigherFacesVanish q property and suppose n = a + q. Then φ composed with the Hσ_q structure map at level n+1 equals a linear combination expressed via δ and σ maps at positions a and a+1, with a sign determined by the construction. This is the vanishing relation that ties the Hσ part to the boundary-like operations when the shifted index matches a + q.
Русский
Пусть φ удовлетворяет свойству HigherFacesVanish q и пусть n = a + q. Тогда композиция φ с соответствующим маппингом Hσ_q на уровне n+1 равна линейной комбинации, выражаемой через отображения δ и σ в позициях a и a+1, с соответствующим знаком. Это содержащаяся в построении связь между частью Hσ и границей при сдвинутых индексах.
LaTeX
$$$\text{If } φ \text{ has } \text{HigherFacesVanish}_q, \ n = a+q: \ φ \circ (Hσ_q)_{n+1} = - φ \circ X.δ_{a+1} \circ X.σ_{a}.$$$
Lean4
theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) (hnaq : n = a + q) :
φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, by cutsat⟩ ≫ X.σ ⟨a, by cutsat⟩ :=
by
have hnaq_shift (d : ℕ) : n + d = a + d + q := by omega
rw [Hσ, Homotopy.nullHomotopicMap'_f (c_mk (n + 2) (n + 1) rfl) (c_mk (n + 1) n rfl),
hσ'_eq hnaq (c_mk (n + 1) n rfl), hσ'_eq (hnaq_shift 1) (c_mk (n + 2) (n + 1) rfl)]
simp only [AlternatingFaceMapComplex.obj_d_eq, eqToHom_refl, comp_id, comp_sum, sum_comp, comp_add]
simp only [comp_zsmul, zsmul_comp, ← assoc, ← mul_zsmul]
-- cleaning up the first sum
rw [← Fin.sum_congr' _ (hnaq_shift 2).symm, Fin.sum_trunc]
swap
· rintro ⟨k, hk⟩
suffices φ ≫ X.δ (⟨a + 2 + k, by cutsat⟩ : Fin (n + 2)) = 0 by
simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
convert v ⟨a + k + 1, by cutsat⟩ (by rw [Fin.val_mk]; cutsat)
dsimp
cutsat
-- cleaning up the second sum
rw [← Fin.sum_congr' _ (hnaq_shift 3).symm, @Fin.sum_trunc _ _ (a + 3)]
swap
· rintro ⟨k, hk⟩
rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
· intro h
replace h : a + 3 + k = 1 := by simp [Fin.ext_iff] at h
cutsat
· dsimp [Fin.cast, Fin.pred]
rw [Nat.add_right_comm, Nat.add_sub_assoc (by simp : 1 ≤ 3)]
cutsat
· simp only [Fin.lt_iff_val_lt_val]
dsimp [Fin.natAdd, Fin.cast]
cutsat
simp only [assoc]
conv_lhs =>
congr
· rw [Fin.sum_univ_castSucc]
· rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
dsimp [Fin.cast, Fin.castLE, Fin.castLT]
/- the purpose of the following `simplif` is to create three subgoals in order
to finish the proof -/
have simplif : ∀ a b c d e f : Y ⟶ X _⦋n + 1⦌, b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f :=
by
intro a b c d e f h1 h2 h3
rw [add_assoc c d e, h2, add_zero, add_comm a, add_assoc, add_comm a, h3, add_zero, h1]
apply simplif
· -- b = f
rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
exact ⟨a, by cutsat⟩
· -- d + e = 0
rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm, X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul, add_neg_cancel]
· -- c + a = 0
rw [← Finset.sum_add_distrib]
apply Finset.sum_eq_zero
rintro ⟨i, hi⟩ _
simp only
have hia : (⟨i, by cutsat⟩ : Fin (n + 2)) ≤ Fin.castSucc (⟨a, by cutsat⟩ : Fin (n + 1)) :=
by
rw [Fin.le_iff_val_le_val]
dsimp
omega
generalize_proofs
rw [← Fin.succ_mk (n + 1) a ‹_›, ← Fin.castSucc_mk (n + 2) i ‹_›, δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ←
neg_zsmul]
congr 2
ring
