Bilinear forms attached to matrices

Mathlib's Matrix.toBilin' reads a square matrix M over a commutative semiring R as the bilinear form (x, y) ↦ xᵀ M y on n → R. This file records facts about these forms that Mathlib lacks. The identity matrix gives the standard form ∑ i, x i * y i, which takes the value 1 on every standard basis vector, so over a nontrivial R it is alternating only when the index type is empty (over the trivial semiring 1 = 0 and every form is alternating). Since the identity matrix is symmetric and invertible, the standard form over a nontrivial R is in every positive dimension a nondegenerate symmetric form that is not alternating, the model for the orthonormal normal form of such forms.

In the other direction, LinearMap.BilinForm.toMatrix reads a bilinear form in a basis as its Gram matrix. For a nondegenerate form, the Gram matrix in the B-dual basis is the inverse transpose of the Gram matrix in the original basis; for a symmetric form it is the inverse Gram matrix, which is how the dual of a lattice is described in coordinates.

Main results

• Matrix.isAlt_toBilin'_one_iff: for R nontrivial, the standard form on n → R is alternating exactly when n is empty.
• LinearMap.BilinForm.toMatrix_dualBasis: the Gram matrix of a nondegenerate form in a B-dual basis is the inverse transpose of its Gram matrix in the original basis.

@[simp]

theorem Matrix.isAlt_toBilin'_one_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommSemiring R] [Nontrivial R] : (toBilin' 1).IsAlt ↔ IsEmpty n

Over a nontrivial commutative semiring R, the standard form ∑ i, x i * y i on n → R is alternating only when n is empty: it takes the value 1 ≠ 0 on every standard basis vector.

theorem LinearMap.BilinForm.toMatrix_dualBasis {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Field K] [AddCommGroup V] [Module K V] [Fintype ι] [DecidableEq ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Module.Basis ι K V) : (toMatrix (B.dualBasis hB b)) B = ((toMatrix b) B).transpose⁻¹

The Gram matrix of a nondegenerate bilinear form in the B-dual basis of b is the inverse of the transpose of its Gram matrix in b. For a symmetric form this is the inverse Gram matrix.