A quadratic form on a free module as a polynomial (GPR 11.8)

If M is free with basis bm : Basis (Fin n) R M, a quadratic form q : M → R is a homogeneous quadratic polynomial in n variables, and evaluating that polynomial over any R-algebra S computes q base-changed to S. This is what lets the LG axiom — which speaks about MvPolynomial (Fin n) R — say anything about quadratic forms.

Main definitions

• QuadraticForm.toMvPolynomial q bm : ∑ i, ∑ j, C (B (bm i) (bm j)) * X i * X j, where B is the bilinear representative QuadraticMap.bilinRepr q used to define QuadraticForm.baseChangeOfProjective.

Main results

• QuadraticForm.aeval_toMvPolynomial_self : aeval t (toMvPolynomial q bm) = q (∑ i, t i • bm i).
• QuadraticForm.aeval_toMvPolynomial : the same after base change, aeval s (toMvPolynomial q bm) = (q.baseChangeOfProjective S) (∑ i, s i • (1 ⊗ₜ bm i)).
• QuadraticForm.totalDegree_toMvPolynomial_le : the polynomial has total degree at most two.

Implementation notes

The polynomial is built from QuadraticMap.bilinRepr q rather than from QuadraticMap.toBilin (mathlib's triangular representative) purely so that the base-change statement is immediate: QuadraticForm.baseChangeOfProjective is defined as the diagonal of LinearMap.BilinForm.baseChange applied to bilinRepr, so both sides of aeval_toMvPolynomial expand to the same double sum without needing baseChangeOfProjective_eq_of_toQuadraticMap_eq. The polynomial is not canonical — a different bilinear representative gives a different polynomial — but its evaluations are, which is all the LG axiom cares about.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.8.

noncomputable def QuadraticForm.toMvPolynomial {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} (q : QuadraticForm R M) (bm : Module.Basis (Fin n) R M) : MvPolynomial (Fin n) R

The quadratic polynomial of q in the basis bm (GPR 11.8), built from the bilinear representative that QuadraticForm.baseChangeOfProjective uses.

Equations

• q.toMvPolynomial bm = ∑ i : Fin n, ∑ j : Fin n, MvPolynomial.C (((QuadraticMap.bilinRepr q) (bm i)) (bm j)) * MvPolynomial.X i * MvPolynomial.X j

theorem QuadraticForm.totalDegree_toMvPolynomial_le {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} (q : QuadraticForm R M) (bm : Module.Basis (Fin n) R M) : (q.toMvPolynomial bm).totalDegree ≤ 2

The polynomial of a quadratic form in a basis is quadratic: its total degree is at most two. Each summand C (B (bm i) (bm j)) * X i * X j is a constant times two variables.

theorem QuadraticForm.aeval_toMvPolynomial_eq_sum {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} {q : QuadraticForm R M} {bm : Module.Basis (Fin n) R M} {S : Type w} [CommRing S] [Algebra R S] (s : Fin n → S) : (MvPolynomial.aeval s) (q.toMvPolynomial bm) = ∑ i : Fin n, ∑ j : Fin n, (algebraMap R S) (((QuadraticMap.bilinRepr q) (bm i)) (bm j)) * s i * s j

Evaluating toMvPolynomial over an R-algebra S gives a double sum in the Gram matrix of the bilinear representative.

theorem QuadraticForm.aeval_toMvPolynomial_self {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} {q : QuadraticForm R M} {bm : Module.Basis (Fin n) R M} (t : Fin n → R) : (MvPolynomial.aeval t) (q.toMvPolynomial bm) = q (∑ i : Fin n, t i • bm i)

GPR 11.8, over R itself.

theorem QuadraticForm.aeval_toMvPolynomial {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} {q : QuadraticForm R M} {bm : Module.Basis (Fin n) R M} {S : Type w} [CommRing S] [Algebra R S] (s : Fin n → S) : (MvPolynomial.aeval s) (q.toMvPolynomial bm) = (baseChangeOfProjective S q) (∑ i : Fin n, s i • 1 ⊗ₜ[R] bm i)

GPR 11.8. The polynomial of q in a basis computes q after every base change: its value at s : Fin n → S is q_S evaluated at the corresponding point of S ⊗[R] M.