English
Let X be a simplicial object in a preadditive category. For every q and n in natural numbers, the morphism (P_q).f(n+1) has the HigherFacesVanish property; in particular, all higher-face maps disappear when composed with (P_q).f(n+1).
Русский
Пусть X — симплициальный объект в предадитивной категории. Для всякого q, n ∈ ℕ отображение (P_q).f(n+1) обладает свойством HigherFacesVanish; в частности, для всех более высоких граней их композиция с (P_q).f(n+1) равна нулю.
LaTeX
$$$\forall q,n \in \mathbb{N},\; HigherFacesVanish_q\Bigl((P_q).f(n+1) : X_{\langle n+1 \rangle} \to X_{\langle n+1 \rangle}\Bigr).$$$
Lean4
/-- This lemma expresses the vanishing of
`(P q).f (n+1) ≫ X.δ k : X _⦋n+1⦌ ⟶ X _⦋n⦌` when `k≠0` and `k≥n-q+2` -/
theorem of_P : ∀ q n : ℕ, HigherFacesVanish q ((P q).f (n + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌)
| 0 => fun n j hj₁ => by omega
| q + 1 => fun n => by
simp only [P_succ]
exact (of_P q n).induction
