Generation of the special orthogonal group by pairs of reflections

For a finite-dimensional nondegenerate quadratic space in characteristic different from two, the special orthogonal group is generated, even as a monoid, by products of two reflections. This is the determinant-one form of the Cartan--Dieudonné theorem. It reduces questions about all special orthogonal transformations to reflection pairs, as needed when proving connectedness by putting those pairs in the identity component.

The full orthogonal group is generated as a monoid by individual reflections, as expressed by closure_reflectionOrthogonal_eq_top; consequently a homomorphism out of it is determined by its values on reflections, orthogonalGroup_hom_ext.

Main results

• TauCeti.QuadraticMap.exists_even_reflectionOrthogonal_list_prod_eq gives a dimension-bounded even reflection word for every determinant-one isometry of a nondegenerate space.

References

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

noncomputable def QuadraticMap.reflectionPairSpecialOrthogonal {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (u v : V) [Invertible (Q u)] [Invertible (Q v)] : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)

The product of two reflections, as an element of the special orthogonal group.

Equations

• QuadraticMap.reflectionPairSpecialOrthogonal Q u v = ⟨↑(TauCeti.QuadraticMap.reflectionOrthogonal Q u) * ↑(TauCeti.QuadraticMap.reflectionOrthogonal Q v), ⋯⟩

@[simp]

theorem QuadraticMap.reflectionPairSpecialOrthogonal_toOrthogonal {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (u v : V) [Invertible (Q u)] [Invertible (Q v)] : (specialOrthogonalToOrthogonal Q) (reflectionPairSpecialOrthogonal Q u v) = TauCeti.QuadraticMap.reflectionOrthogonal Q u * TauCeti.QuadraticMap.reflectionOrthogonal Q v

The underlying orthogonal isometry of a pair of reflections.

@[simp]

theorem QuadraticMap.reflectionPairSpecialOrthogonal_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (u v x : V) [Invertible (Q u)] [Invertible (Q v)] : ↑(reflectionPairSpecialOrthogonal Q u v) x = (TauCeti.QuadraticMap.reflection Q u) ((TauCeti.QuadraticMap.reflection Q v) x)

A pair of reflections acts by applying the second reflection, then the first.

theorem TauCeti.QuadraticMap.exists_even_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 : ↥(specialOrthogonalGroup Q)) : ∃ (l : List ↥(orthogonalGroup Q)), (∀ r ∈ l, ∃ (v : V) (x : Invertible (Q v)), reflectionOrthogonal Q v = r) ∧ l.length ≤ Module.finrank K V ∧ Even l.length ∧ l.prod = ⟨↑g, ⋯⟩

Every special orthogonal transformation of a nondegenerate quadratic space is a product of an even number of reflections, with length at most the dimension.

theorem TauCeti.QuadraticMap.closure_reflectionOrthogonal_eq_top {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) : Submonoid.closure {g : ↥(orthogonalGroup Q) | ∃ (v : V) (x : Invertible (Q v)), reflectionOrthogonal Q v = g} = ⊤

Reflections generate the full orthogonal group as a monoid.

theorem TauCeti.QuadraticMap.orthogonalGroup_hom_ext {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) {M : Type u_1} [MulOneClass M] {f g : ↥(orthogonalGroup Q) →* M} (h : ∀ (v : V) [inst : Invertible (Q v)], f (reflectionOrthogonal Q v) = g (reflectionOrthogonal Q v)) : f = g

Two monoid homomorphisms out of the orthogonal group are equal as soon as they agree on every reflection in a vector of invertible norm.

theorem TauCeti.QuadraticMap.specialOrthogonalGroup_le_of_reflection_mul_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) (M : Submonoid (V ≃ₗ[K] V)) (hM : ∀ (v w : V) [inst : Invertible (Q v)] [inst_1 : Invertible (Q w)], reflection Q v * reflection Q w ∈ M) : (specialOrthogonalGroup Q).toSubmonoid ≤ M

Every determinant-one orthogonal transformation belongs to any submonoid containing all products of two reflections. No nonzero-dimensional hypothesis is required.

theorem TauCeti.QuadraticMap.closure_reflection_mul_eq_specialOrthogonalGroup {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) : Submonoid.closure {g : V ≃ₗ[K] V | ∃ (v : V) (w : V) (x : Invertible (Q v)) (x_1 : Invertible (Q w)), reflection Q v * reflection Q w = g} = (specialOrthogonalGroup Q).toSubmonoid

The monoid generated by pairs of reflections is exactly the special orthogonal group of a finite-dimensional nondegenerate quadratic space in characteristic different from two.