English
For all q and n, the morphism (P_q).f(n) acts as a projection (idempotent) on the alternating face map complex at level n, i.e., composing it with itself yields itself.
Русский
Для всех q и n отображение (P_q).f(n) является проекцией (идемпотентно) на чередующемся комплексе граней уровня n: при композиции с самим собой получается то же самое.
LaTeX
$$$\forall q,n: (P_q).f(n) \circ (P_q).f(n) = (P_q).f(n).$$$
Lean4
@[reassoc]
theorem comp_P_eq_self {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) : φ ≫ (P q).f (n + 1) = φ :=
by
induction q with
| zero =>
simp only [P_zero]
apply comp_id
| succ q
hq =>
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id, ← assoc,
hq v.of_succ, add_eq_left]
by_cases hqn : n < q
· exact v.of_succ.comp_Hσ_eq_zero hqn
· obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)
have hnaq : n = a + q := by omega
simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
have eq :=
v ⟨a, by cutsat⟩
(by
simp only [hnaq, add_assoc]
rfl)
simp only [Fin.succ_mk] at eq
simp only [eq, zero_comp]
