Unitary transvection groups of isotropic points

Let h(x, y) = (σ ∘ x) ⬝ᵥ (Q *ᵥ y) be the σ-sesquilinear form of a Gram matrix Q (Matrix.specialIsometryGroup), and τ_{v,a} = 1 + a v (vᵀ ^ σ Q) the unitary transvection Matrix.unitaryTransvection Q σ v a. When v is isotropic, h(v, v) = 0, the matrix τ_{v,a} has determinant one, and if σ is an involution and Q is ε-Hermitian, (Q ^ σ)ᵀ = ε • Q, it lies in the special isometry group when a + ε σ(a) = 0. Over a field, for a nondegenerate Q and v ≠ 0, only then. For a Hermitian form (ε = 1) the admissible parameters are the elements of trace zero. An isometry g conjugates τ_{v,a} to τ_{g v,a}.

To an isotropic point p of projective space this attaches the group Matrix.unitaryTransvectionSubgroup Q σ p of isometries that are unitary transvections along a representative of p. It does not depend on the representative, it is abelian, and conjugation by an isometry g carries it to the group of g • p. These are the commutativity and conjugacy axioms of an Iwasawa structure (MulAction.IwasawaStructure) for the action of a special unitary group on its isotropic points, the action from which the simplicity of the projective special unitary groups is deduced.

The Iwasawa structure of the symplectic groups in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Iwasawa, built from the symplectic transvections of TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Transvection, served as the model for this file.

Main definitions

• Matrix.unitaryTransvectionSubgroup Q σ p: the unitary transvections along an isotropic point.

Main results

• Matrix.exists_mem_specialIsometryGroup_coe_eq_unitaryTransvection: for a + ε σ(a) = 0 the transvection τ_{v,a} along an isotropic vector is a special isometry.
• Matrix.exists_coe_eq_unitaryTransvection_iff: for a nondegenerate ε-Hermitian Q, the transvection τ_{v,a} along an isotropic point is an isometry exactly when a + ε σ(a) = 0.
• Matrix.coe_mul_unitaryTransvection_mul_coe_inv: an isometry g conjugates τ_{v,a} to τ_{g v,a}.
• Matrix.unitaryTransvectionSubgroup_smul: T(g • p) = g T(p) g⁻¹.

References

• D. E. Taylor, The Geometry of the Classical Groups (1992), Chapters 10 and 11.
• L. C. Grove, Classical Groups and Geometric Algebra (2002), Chapter 11.

theorem Matrix.coe_mul_unitaryTransvection_mul_coe_inv {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] {Q : Matrix n n K} {σ : K →+* K} {g : SpecialLinearGroup n K} (hg : g ∈ Q.specialIsometryGroup σ) (v : n → K) (a : K) : ↑g * Q.unitaryTransvection σ v a * ↑g⁻¹ = Q.unitaryTransvection σ ((↑g).mulVec v) a

An isometry conjugates τ_{v,a} to τ_{g v,a}.

theorem Matrix.exists_mem_specialIsometryGroup_coe_eq_unitaryTransvection {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [CommRing K] {Q : Matrix n n K} {σ : K →+* K} (hσ : Function.Involutive ⇑σ) {ε : K} (hQ : (Q.map ⇑σ).transpose = ε • Q) {v : n → K} (hv : ⇑σ ∘ v ⬝ᵥ Q.mulVec v = 0) {a : K} (ha : a + ε * σ a = 0) : ∃ g ∈ Q.specialIsometryGroup σ, ↑g = Q.unitaryTransvection σ v a

Admissible unitary transvections are isometries. If σ is an involution, Q is ε-Hermitian, v is isotropic and a + ε σ(a) = 0, then τ_{v,a} is the matrix of an element of the special isometry group of Q.

def Matrix.unitaryTransvectionSubgroup {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] (Q : Matrix n n K) (σ : K →+* K) (p : ↥(Q.isotropicPoints σ)) : Subgroup ↥(Q.specialIsometryGroup σ)

The unitary transvection group of an isotropic point p: the isometries that are unitary transvections τ_{v,a} along a representative v of p. It does not depend on the representative (Matrix.mem_unitaryTransvectionSubgroup_mk_iff), and is abelian.

theorem Matrix.mem_unitaryTransvectionSubgroup_iff {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {p : ↥(Q.isotropicPoints σ)} {g : ↥(Q.specialIsometryGroup σ)} : g ∈ Q.unitaryTransvectionSubgroup σ p ↔ ∃ (a : K), ↑↑g = Q.unitaryTransvection σ (↑p).rep a

An isometry lies in the transvection group of p exactly when it is a unitary transvection along the chosen representative of p.

@[simp]

theorem Matrix.mem_unitaryTransvectionSubgroup_mk_iff {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {v : n → K} (hv : v ≠ 0) (hp : Projectivization.mk K v hv ∈ Q.isotropicPoints σ) {g : ↥(Q.specialIsometryGroup σ)} : g ∈ Q.unitaryTransvectionSubgroup σ ⟨Projectivization.mk K v hv, hp⟩ ↔ ∃ (a : K), ↑↑g = Q.unitaryTransvection σ v a

The transvection group does not depend on the representative: an isometry lies in the transvection group of the point [v] exactly when it is a unitary transvection along v.

instance Matrix.instIsMulCommutativeSubtypeSpecialLinearGroupMemSubgroupSpecialIsometryGroupUnitaryTransvectionSubgroup {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} (p : ↥(Q.isotropicPoints σ)) : IsMulCommutative ↥(Q.unitaryTransvectionSubgroup σ p)

The transvection group of an isotropic point is abelian.

theorem Matrix.unitaryTransvectionSubgroup_smul {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} (g : ↥(Q.specialIsometryGroup σ)) (p : ↥(Q.isotropicPoints σ)) : Q.unitaryTransvectionSubgroup σ (g • p) = MulAut.conj g • Q.unitaryTransvectionSubgroup σ p

Conjugation moves transvection groups along the action: T(g • p) = g T(p) g⁻¹.

theorem Matrix.exists_coe_eq_unitaryTransvection {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {ε : K} (hσ : Function.Involutive ⇑σ) (hQ : (Q.map ⇑σ).transpose = ε • Q) (p : ↥(Q.isotropicPoints σ)) {a : K} (ha : a + ε * σ a = 0) : ∃ (g : ↥(Q.unitaryTransvectionSubgroup σ p)), ↑↑↑g = Q.unitaryTransvection σ (↑p).rep a

Every admissible parameter gives an isometry. If σ is an involution and Q is ε-Hermitian, then for every a with a + ε σ(a) = 0 the transvection τ_{v,a} along the representative v of an isotropic point lies in its transvection group.

theorem Matrix.exists_coe_eq_unitaryTransvection_iff {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {Q : Matrix n n K} {σ : K →+* K} {ε : K} (hσ : Function.Involutive ⇑σ) (hQ : (Q.map ⇑σ).transpose = ε • Q) (hdet : Q.det ≠ 0) (p : ↥(Q.isotropicPoints σ)) (a : K) : (∃ (g : ↥(Q.unitaryTransvectionSubgroup σ p)), ↑↑↑g = Q.unitaryTransvection σ (↑p).rep a) ↔ a + ε * σ a = 0

The parameters of the transvection group of an isotropic point. If σ is an involution and Q is a nondegenerate ε-Hermitian matrix, the transvection τ_{v,a} along the representative v of an isotropic point is an isometry exactly when a + ε σ(a) = 0. For a Hermitian form these are the elements of trace zero.