σ — Mathlib · SciLib

English

For each n and i in Fin(n+1), σ(i) is the i-th degeneracy morphism from Δ^{n+1} to Δ^n, sending the i-th vertex to collapse two adjacent vertices.

Русский

Для каждого n и i ∈ Fin(n+1) морфизм σ(i) — редукционный морфизм Δ^{n+1}→Δ^n, сжатие двух соседних вершин.

LaTeX

$$$\sigma\{n\} (i) : \Delta^{n+1} \to \Delta^n$$$

Lean4

/-- The `i`-th degeneracy map from `⦋n+1⦌` to `⦋n⦌` -/
def σ {n} (i : Fin (n + 1)) : ⦋n + 1⦌ ⟶ ⦋n⦌ :=
  mkHom i.predAboveOrderHom

Похожие утверждения