English
If a morphism φ satisfies HigherFacesVanish q φ, then composing φ with a face map σ at level b yields a morphism with the same vanish property for q.
Русский
Если морфизм φ удовлетворяет свойству HigherFacesVanish q φ, то композиция φ с лицевой картой σ на уровне b сохраняет это свойство для q.
LaTeX
$$$$ \\text{HigherFacesVanish}_q(φ \\circ X.\\sigma \\langle b, \\dots \\rangle). $$$$
Lean4
theorem comp_σ {Y : C} {X : SimplicialObject C} {n b q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ)
(hnbq : n + 1 = b + q) :
HigherFacesVanish q (φ ≫ X.σ ⟨b, by simp only [hnbq, Nat.lt_add_one_iff, le_add_iff_nonneg_right, zero_le]⟩) :=
fun j hj =>
by
rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj, zero_comp]
· intro hj'
simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right, nonpos_iff_eq_zero,
add_eq_zero, false_and, reduceCtorEq] at hj
· dsimp
rw [Fin.lt_iff_val_lt_val, Fin.val_succ]
linarith
