English
Let C be a category with finite coproducts and X a simplicial object in C. If a morphism φ: Y → X_{n+1} has the property that its higher faces vanish at level q (i.e., HigherFacesVanish q φ holds), then composing φ on the left with any morphism f: Z → Y yields a morphism f ∘ φ: Z → X_{n+1} that also has HigherFacesVanish q. In other words, HigherFacesVanish q is stable under precomposition.
Русский
Пусть C — категория с конечными копройдными и есть симплициальный объект X в C. Если для морфизма φ: Y → X_{n+1} выполняется свойство HigherFacesVanish q (то есть высшие грани исчезают на уровне q), то для любого морфизма f: Z → Y композиция φ с f даёт морфизм f ∘ φ: Z → X_{n+1}, который тоже имеет HigherFacesVanish q. Иными словами, свойство исчезновения высших гран сохраняется при префиксной композиции.
LaTeX
$$$\forall \; C, X, q, n, Y, Z, φ: Y \to X_{n+1},\ f: Z \to Y,\ v: \text{HigherFacesVanish}_q(φ) \\ o\; \text{HigherFacesVanish}_q(f \circ φ).$$$
Lean4
theorem of_comp {Y Z : C} {q n : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) (f : Z ⟶ Y) :
HigherFacesVanish q (f ≫ φ) := fun j hj => by rw [assoc, v j hj, comp_zero]
