Reflection-pair generation in matrix coordinates #
The determinant-one matrices preserving the standard symmetric form are generated by pairs of
reflections. This file translates the abstract quadratic-space generation theorem into the
matrix model Matrix.specialOrthogonalGroup, the model represented by the special orthogonal
coordinate Hopf algebra. Generation holds over every field of characteristic different from
two, with no positivity hypothesis on the dimension.
References #
- H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.
theorem
TauCeti.closure_reflection_mul_eq_matrixSpecialOrthogonalGroup
{n : Type v}
[Fintype n]
[DecidableEq n]
{K : Type u}
[Field K]
[NeZero 2]
:
have Q := Matrix.toQuadraticForm' 1;
Submonoid.closure
{A : Matrix n n K | ∃ (v : n → K) (w : n → K) (x : Invertible (Q v)) (x_1 : Invertible (Q w)),
LinearMap.toMatrix' ↑(QuadraticMap.reflection Q v) * LinearMap.toMatrix' ↑(QuadraticMap.reflection Q w) = A} = Matrix.specialOrthogonalGroup n K
The matrix special orthogonal group is generated, as a monoid, by the matrices of products of two reflections in the standard quadratic form.