English
Given an ordered basis bm, one can build a bilinear form B on M × N from a quadratic map Q by setting B(bm_i, bm_j) = Q(bm_i) when i=j, B(bm_i, bm_j) = polar(Q)(bm_i, bm_j) when i<j, and B(bm_i, bm_j) = 0 when i>j. This yields a (generally non-symmetric) bilinear form whose matrix is triangular in the basis order.
Русский
Для заданной упорядоченной базы bm можно из квадратичного отображения Q получить билинейную форму B на M × N: B(bm_i, bm_j) = Q(bm_i) если i=j; B(bm_i, bm_j) = polar(Q)(bm_i, bm_j) если i<j; и B(bm_i, bm_j) = 0 если i>j.
LaTeX
$$$B(i,j) = \\begin{cases} Q(b_i), & i=j, \\\\ polar(Q)(b_i,b_j), & ij. \\end{cases}$$$
Lean4
/-- Given an ordered basis, produce a bilinear form associated with the quadratic form.
Unlike `QuadraticMap.associated`, this is not symmetric; however, as a result it can be used even
in characteristic two. When considered as a matrix, the form is triangular. -/
noncomputable def toBilin (Q : QuadraticMap R M N) (bm : Basis ι R M) : LinearMap.BilinMap R M N :=
bm.constr (S := R) fun i =>
bm.constr (S := R) fun j => if i = j then Q (bm i) else if i < j then polar Q (bm i) (bm j) else 0
