The Cartan--Dieudonne theorem

Every orthogonal automorphism of a finite-dimensional nondegenerate quadratic space over a field of characteristic not two is generated by reflections in vectors of nonzero norm. The proof uses dimension induction: after making an anisotropic vector fixed, it restricts to the nondegenerate orthogonal complement. An exceptional isotropic-displacement case is reduced to this step by precomposing with a reflection and using determinant parity to retain the sharp bound.

Main results

• TauCeti.QuadraticMap.subgroup_eq_top_of_reflection_mem: any subgroup containing every reflection in a vector of invertible norm is the full orthogonal group.
• TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_eq: every orthogonal transformation is a product of at most the dimension many reflections.

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

theorem TauCeti.QuadraticMap.det_list_prod_of_reflectionOrthogonal {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (l : List ↥(orthogonalGroup Q)) (hl : ∀ r ∈ l, ∃ (v : V) (x : Invertible (Q v)), reflectionOrthogonal Q v = r) : LinearEquiv.det ↑l.prod = (-1) ^ l.length

The determinant of a product of orthogonal reflections is the sign determined by the number of factors.

theorem TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_eq {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (g : ↥(orthogonalGroup Q)) : ∃ (l : List ↥(orthogonalGroup Q)), (∀ r ∈ l, ∃ (v : V) (x : Invertible (Q v)), reflectionOrthogonal Q v = r) ∧ l.length ≤ Module.finrank K V ∧ l.prod = g

Every orthogonal transformation of a nondegenerate quadratic space is a product of at most the dimension many reflections.

theorem TauCeti.QuadraticMap.subgroup_eq_top_of_reflection_mem {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NeZero 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (H : Subgroup ↥(orthogonalGroup Q)) (hreflection : ∀ (v : V) [inst : Invertible (Q v)], reflectionOrthogonal Q v ∈ H) : H = ⊤

Cartan--Dieudonné generation. Any subgroup of the orthogonal group that contains every reflection in a vector of invertible norm is the whole orthogonal group.