coe_J — Mathlib

English

Let l be a finite type and R a commutative ring. The canonical matrix associated to the symplectic form, symJ l R, maps to the standard symplectic matrix J l R under the natural inclusion into matrices. In other words, the matrix representing symJ is exactly J.

Русский

Пусть l — конечный тип, R — коммутативное кольцо. Каноническая матрица, соответствующая симплексной форме, symJ l R, отображается в стандартную симпликтическую матрицу J l R через естественное вложение в матрицы. То есть матрица, представляющая symJ, равна J.

LaTeX

$$$\\uparrow(\\mathrm{symJ}\\, l\\, R) = J\\, l\\, R$$$

Lean4

@[simp]
theorem coe_J : ↑(symJ l R) = J l R :=
  rfl

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