Gram forms and matrix reflection

This file records the basic symmetry and quadratic-form preservation identities for the bilinear and quadratic forms attached to a symmetric matrix.

Main results

• TauCeti.vecMul_dotProduct_comm: the bilinear form (v, w) ↦ (v ᵥ* M) ⬝ᵥ w of a symmetric matrix M is symmetric.
• TauCeti.reflect_vecMul_dotProduct_self: reflection in a vector of norm two preserves the value (v ᵥ* M) ⬝ᵥ v of the form at every vector.

theorem TauCeti.vecMul_dotProduct_comm {n : Type u_1} [Fintype n] {R : Type u_2} [NonUnitalCommSemiring R] {M : Matrix n n R} (hM : M.IsSymm) (v w : n → R) : Matrix.vecMul v M ⬝ᵥ w = Matrix.vecMul w M ⬝ᵥ v

The bilinear form carried by a symmetric matrix is symmetric.

theorem TauCeti.reflect_vecMul_dotProduct_self {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] {M : Matrix n n R} (hM : M.IsSymm) {u : n → R} (hu : Matrix.vecMul u M ⬝ᵥ u = 2) (v : n → R) : Matrix.vecMul (v - (Matrix.vecMul v M ⬝ᵥ u) • u) M ⬝ᵥ (v - (Matrix.vecMul v M ⬝ᵥ u) • u) = Matrix.vecMul v M ⬝ᵥ v

Reflection in a vector of norm two preserves the value of the quadratic form. For a symmetric matrix M and a vector u with (u ᵥ* M) ⬝ᵥ u = 2, reflection in u preserves the value (v ᵥ* M) ⬝ᵥ v of the form at every vector v. This is what makes a family of norm-two vectors stable under its own reflections once the family exhausts the norm-two vectors.