Orthogonal automorphisms in an orthogonal basis

In an orthogonal basis, polarization against a basis vector extracts its coordinate, and the reflection in that vector negates just that coordinate. The entries of an orthogonal automorphism and its inverse satisfy the weighted transpose identity. These formulas connect the reflection calculus with integrality of matrices over local fields.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §43.

theorem QuadraticMap.polar_basis_left {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (b : Module.Basis ι R V) (hb : ∀ (i j : ι), i ≠ j → IsOrtho Q (b i) (b j)) (i : ι) (x : V) : polar (⇑Q) (b i) x = 2 * Q (b i) * (b.repr x) i

Polarization against a vector of an orthogonal basis extracts the corresponding coordinate. The factor two uses the unhalved polarization.

theorem QuadraticMap.reflection_basis_apply {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (b : Module.Basis ι R V) (hb : ∀ (i j : ι), i ≠ j → IsOrtho Q (b i) (b j)) (i : ι) [Invertible (Q (b i))] (x : V) : (TauCeti.QuadraticMap.reflection Q (b i)) x = x - (2 * (b.repr x) i) • b i

Reflection in a vector of an orthogonal basis subtracts twice its coordinate.

theorem QuadraticMap.basis_value_mul_repr_orthogonal_eq_basis_value_mul_repr_inv {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (b : Module.Basis ι R V) (hb : ∀ (i j : ι), i ≠ j → IsOrtho Q (b i) (b j)) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) (i j : ι) : 2 * Q (b i) * (b.repr (↑g (b j))) i = 2 * Q (b j) * (b.repr (↑g⁻¹ (b i))) j

The entries of an orthogonal automorphism and its inverse are weighted transposes of one another, with weights the quadratic values of the orthogonal basis vectors.