The last-vector stabilizer in a special orthogonal group

Let Q be a quadratic form on a finite free module M. Extending an element of SO(Q) by the identity on a rank-one summand embeds it into SO(Q.prod QuadraticMap.sq). If two acts regularly on the base ring, its image is exactly the stabilizer of the last basis vector (0, 1).

The inverse map restricts a stabilizer element to the first summand. Orthogonality and fixation of (0, 1) force that summand to be preserved: polarizing the image of (m, 0) against (0, 1) shows that twice its last coordinate vanishes. The determinant-one condition then descends because the original map is the product of its restriction with the identity of the last summand.

This calculation is useful for inductive comparisons of orthogonal and Spin groups: after applying a Spin action, it turns fixation of the last vector into a lower-rank special orthogonal transformation.

Main definitions

• specialOrthogonalGroupProdLastInclusion: extend a special orthogonal transformation by the identity on the square line.
• specialOrthogonalGroupProdLastInclusionToStabilizer: the same extension, codrestricted to the last-vector stabilizer.
• specialOrthogonalGroupProdLastStabilizer: the subgroup fixing (0, 1).
• specialOrthogonalGroupEquivProdLastStabilizer: the extension-restriction equivalence between SO(Q) and that stabilizer.

noncomputable def QuadraticMap.specialOrthogonalGroupProdLastInclusion {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Module.Free R M] [Module.Finite R M] : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) →* ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (prod Q sq))

Extend a special orthogonal transformation by the identity on the square line.

@[simp]

theorem QuadraticMap.specialOrthogonalGroupProdLastInclusion_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Module.Free R M] [Module.Finite R M] (f : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) (x : M × R) : ↑((specialOrthogonalGroupProdLastInclusion Q) f) x = (↑f x.1, x.2)

Extending a special orthogonal transformation acts componentwise and fixes the square-line coordinate.

theorem QuadraticMap.specialOrthogonalGroupProdLastInclusion_injective {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Module.Free R M] [Module.Finite R M] : Function.Injective ⇑(specialOrthogonalGroupProdLastInclusion Q)

Extension by the identity on the square line is injective.

noncomputable def QuadraticMap.specialOrthogonalGroupProdLastStabilizer {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Subgroup ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (prod Q sq))

The stabilizer of the last basis vector (0, 1) in the special orthogonal group of Q.prod QuadraticMap.sq.

@[simp]

theorem QuadraticMap.mem_specialOrthogonalGroupProdLastStabilizer_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (prod Q sq))} : g ∈ specialOrthogonalGroupProdLastStabilizer Q ↔ ↑g (0, 1) = (0, 1)

Membership in the last-vector stabilizer means exactly that the underlying linear transformation fixes (0, 1).

theorem QuadraticMap.orthogonalGroupProdLast_apply_snd_of_fixed {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsRegular 2) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup (prod Q sq))) (hfix : ↑g (0, 1) = (0, 1)) (m : M) : (↑g (m, 0)).2 = 0

An orthogonal transformation fixing the last basis vector maps the first summand back into the first summand.

@[simp]

theorem QuadraticMap.specialOrthogonalGroupProdLastStabilizer_apply_snd {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsRegular 2) (g : ↥(specialOrthogonalGroupProdLastStabilizer Q)) (m : M) : (↑↑g (m, 0)).2 = 0

A last-vector stabilizer element maps the first summand back into the first summand.

noncomputable def QuadraticMap.specialOrthogonalGroupProdLastInclusionToStabilizer {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Module.Free R M] [Module.Finite R M] : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) →* ↥(specialOrthogonalGroupProdLastStabilizer Q)

Extend a special orthogonal transformation by the identity, as an element of the last-vector stabilizer.

@[simp]

theorem QuadraticMap.specialOrthogonalGroupProdLastInclusionToStabilizer_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Module.Free R M] [Module.Finite R M] (f : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) (x : M × R) : ↑↑((specialOrthogonalGroupProdLastInclusionToStabilizer Q) f) x = (↑f x.1, x.2)

The stabilizer-valued identity extension acts componentwise.

noncomputable def QuadraticMap.specialOrthogonalGroupEquivProdLastStabilizer {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsRegular 2) [Module.Free R M] [Module.Finite R M] : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) ≃* ↥(specialOrthogonalGroupProdLastStabilizer Q)

Extension by the identity identifies SO(Q) with the last-vector stabilizer in SO(Q.prod QuadraticMap.sq).

The inverse sends a stabilizer element g to its restriction m ↦ (g (m, 0)).1. Regularity of 2 ensures that fixation of (0, 1) forces g to preserve the first summand.

@[simp]

theorem QuadraticMap.coe_specialOrthogonalGroupEquivProdLastStabilizer_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsRegular 2) [Module.Free R M] [Module.Finite R M] (f : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) (x : M × R) : ↑↑((specialOrthogonalGroupEquivProdLastStabilizer Q h2) f) x = (↑f x.1, x.2)

The stabilizer equivalence sends f to its extension by the identity.

@[simp]

theorem QuadraticMap.coe_specialOrthogonalGroupEquivProdLastStabilizer_symm_apply {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsRegular 2) [Module.Free R M] [Module.Finite R M] (g : ↥(specialOrthogonalGroupProdLastStabilizer Q)) (m : M) : ↑((specialOrthogonalGroupEquivProdLastStabilizer Q h2).symm g) m = (↑↑g (m, 0)).1

The inverse stabilizer equivalence restricts to the first summand.