English
If a morphism φ has HigherFacesVanish q, then the composition φ with the Hσ_q map has a controlled expression as a sum of terms which vanish, yielding a zero when n < q. This is a vanishing identity guided by the target’s decomposition via the alternating face map complex.
Русский
Если для морфизма φ верно HigherFacesVanish q, то композиция φ с картой Hσ_q имеет выражение в виде суммы членов, которые исчезают, и в случае n < q сумма дает нулевой результат; это тождество исчезновения, управляемое разложением целевого объекта через чередующий комплекс лиц.
LaTeX
$$$\text{If } v: \text{HigherFacesVanish}_q(φ)\text{, then } φ \circ (Hσ_q) = 0 \text{ when } n < q.$$$
Lean4
/-- `Isδ₀ i` is a simple condition used to check whether a monomorphism `i` in
`SimplexCategory` identifies to the coface map `δ 0`. -/
@[nolint unusedArguments]
def Isδ₀ {Δ Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [Mono i] : Prop :=
Δ.len = Δ'.len + 1 ∧ i.toOrderHom 0 ≠ 0
