The standard general-linear subgroup of the symplectic group

For a commutative ring R, an invertible matrix A acts on a free module and contragrediently on its dual. On the direct sum this gives the symplectic matrix

             [ A       0    ]
levi(A)  =   [              ].
             [ 0   (A⁻¹)ᵀ ]

This file packages that construction as the injective homomorphism TauCeti.GLSymplectic.leviHom : GL l R →* GLSymplectic l R, transports it to the Fin (m + m) coordinates used by the symplectic group scheme, and identifies the images of elementary transvections with the difference-root subgroups. It follows that over a field the image of SL_m under the Levi embedding belongs to every subgroup containing all difference-root elements, and that the full Levi image belongs once the diagonal Levi subgroup is also included.

The full-Levi result supplies the diagonal-block factor in symplectic Gaussian decomposition, alongside the upper- and lower-unipotent factors.

Main definitions

• TauCeti.GLSymplectic.leviHom: the general-linear Levi embedding in sum coordinates.
• TauCeti.GLSymplecticFin.leviHom: the same embedding in Fin (m + m) coordinates.

Main results

• TauCeti.GLSymplectic.leviHom_injective and TauCeti.GLSymplecticFin.leviHom_injective: both presentations are embeddings.
• TauCeti.GLSymplecticFin.leviHom_transvection: an elementary transvection maps to the corresponding difference-root element.
• TauCeti.GLSymplecticFin.leviHom_toGL_mem_of_difference: over a field, every element of the determinant-one Levi subgroup lies in any subgroup containing the difference-root elements.
• TauCeti.GLSymplecticFin.leviHom_mem_of_difference_of_diagonal: adding the diagonal Levi subgroup gives every general-linear Levi element.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 5.2.
• T. A. Springer, Linear Algebraic Groups, 2nd ed., §8.1.

This advances the explicit type-C Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. The type-C branch of milestone L0 of TauCetiRoadmap/CFSGStatement/README.md consumes the resulting pinned carrier; the next carrier step is the field-valued symplectic generation theorem, whose Levi factor is supplied here.

noncomputable def TauCeti.GLSymplectic.leviHom {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] : GL l R →* ↥(GLSymplectic l R)

The general-linear group embedded as the standard Levi subgroup of the symplectic group: A ↦ diag(A, (A⁻¹)ᵀ).

Equations

• TauCeti.GLSymplectic.leviHom = { toFun := TauCeti.GLSymplectic.leviElement✝, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GLSymplectic.coe_leviHom {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] (A : GL l R) : ↑↑(leviHom A) = Matrix.fromBlocks (↑A) 0 0 (↑A⁻¹).transpose

The matrix underlying the Levi embedding is diag(A, (A⁻¹)ᵀ).

theorem TauCeti.GLSymplectic.leviHom_injective {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] : Function.Injective ⇑leviHom

The general-linear Levi homomorphism is injective.

@[simp]

theorem TauCeti.GLSymplectic.map_leviHom {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (A : GL l R) : (map l f) (leviHom A) = leviHom ((Matrix.GeneralLinearGroup.map f) A)

The Levi embedding commutes with extension of the value ring.

noncomputable def TauCeti.GLSymplecticFin.leviHom {m : ℕ} {R : Type u} [CommRing R] : GL (Fin m) R →* ↥(GLSymplecticFin m R)

The standard general-linear Levi embedding in the Fin (m + m) coordinates used by the symplectic group scheme.

Equations

• TauCeti.GLSymplecticFin.leviHom = (TauCeti.GLSymplecticFin.mulEquivGLSymplectic m R).symm.toMonoidHom.comp TauCeti.GLSymplectic.leviHom

@[simp]

theorem TauCeti.GLSymplecticFin.mulEquivGLSymplectic_leviHom {m : ℕ} {R : Type u} [CommRing R] (A : GL (Fin m) R) : (mulEquivGLSymplectic m R) (leviHom A) = GLSymplectic.leviHom A

Transporting the Fin-indexed Levi embedding to sum coordinates recovers TauCeti.GLSymplectic.leviHom.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_leviHom {m : ℕ} {R : Type u} [CommRing R] (A : GL (Fin m) R) : ↑↑(leviHom A) = (Matrix.fromBlocks (↑A) 0 0 (↑A⁻¹).transpose).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

The matrix underlying the Fin-indexed Levi embedding is the block-diagonal Levi matrix, transported from sum coordinates along finSumFinEquiv.

@[simp]

theorem TauCeti.GLSymplecticFin.map_leviHom {m : ℕ} {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (A : GL (Fin m) R) : (map m R f) (leviHom A) = leviHom ((Matrix.GeneralLinearGroup.map f) A)

The Fin-indexed Levi embedding commutes with extension of the value ring.

theorem TauCeti.GLSymplecticFin.leviHom_injective {m : ℕ} {R : Type u} [CommRing R] : Function.Injective ⇑leviHom

The Fin-indexed Levi homomorphism is injective.

@[simp]

theorem TauCeti.GLSymplecticFin.leviHom_transvection {m : ℕ} {R : Type u} [CommRing R] {i j : Fin m} (hij : i ≠ j) (c : R) : leviHom (Matrix.SpecialLinearGroup.toGL (Matrix.SpecialLinearGroup.transvection hij c)) = differenceShortRootUnit hij c

An elementary transvection maps under the symplectic Levi embedding to the corresponding difference-root element.

theorem TauCeti.GLSymplecticFin.leviHom_toGL_mem_of_difference {m : ℕ} {K : Type u_1} [Field K] (H : Subgroup ↥(GLSymplecticFin m K)) (hdifference : ∀ {i j : Fin m} (hij : i ≠ j) (c : K), differenceShortRootUnit hij c ∈ H) (A : Matrix.SpecialLinearGroup (Fin m) K) : leviHom (Matrix.SpecialLinearGroup.toGL A) ∈ H

Over a field, every determinant-one element of the general-linear Levi subgroup belongs to any subgroup containing all difference-root elements.

theorem TauCeti.GLSymplecticFin.leviHom_mem_of_difference_of_diagonal {m : ℕ} {K : Type u_1} [Field K] (H : Subgroup ↥(GLSymplecticFin m K)) (hdifference : ∀ {i j : Fin m} (hij : i ≠ j) (c : K), differenceShortRootUnit hij c ∈ H) (hdiagonal : ∀ (s : Fin m → Kˣ), leviHom (diagGL s) ∈ H) (A : GL (Fin m) K) : leviHom A ∈ H

Every general-linear Levi element belongs to a subgroup containing all difference-root elements and every diagonal Levi element.