diagonal — Mathlib

English

There is a canonical diagonal map diag_n: X_n → X_1 given by applying X to the diagonal map in the simplex category.

Русский

Существует каноническое диагональное отображение diag_n: X_n → X_1, получаемое как образ X от диагонального отображения в симплексной категории.

LaTeX

$$$\mathrm{diag}_n := X(\mathrm{diag}_n^{\mathrm{op}}): X_n \to X_1$$$

Lean4

/-- The diagonal of a simplex is the long edge of the simplex. -/
def diagonal {n : ℕ} : X _⦋n⦌ ⟶ X _⦋1⦌ :=
  X.map ((SimplexCategory.diag n).op)

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