single — Mathlib

English

For i ≠ j, there is a linear map from R into sl_n(R) sending r to the matrix unit E_{ij} with trace zero.

Русский

Для i ≠ j существует линейное отображение R → sl_n(R), отправляющее r в элемент-единицу матрицы E_{ij} с нулевой следой.

LaTeX

$$$$ (\text{single}(i,j,h)\, r).\text{val} = \mathrm{Matrix.single}_{i j} \, r, \quad h: i \neq j. $$$$

Lean4

/-- When `i ≠ j`, the single-element matrices are elements of `sl n R`.

Along with some elements produced by `singleSubSingle`, these form a natural basis of `sl n R`. -/
def single (h : i ≠ j) : R →ₗ[R] sl n R :=
  Matrix.singleLinearMap R i j |>.codRestrict _ fun r => Matrix.trace_single_eq_of_ne i j r h

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