Symmetric unipotent blocks generated by symplectic root subgroups

The upper and lower unipotent block subgroups of the standard symplectic group consist of

u(B) = [1 B; 0 1],        l(C) = [1 0; C 1]

for symmetric matrices B and C. This file proves that every such element is generated by the standard type-C root subgroups. Diagonal entries are the long roots ±2eᵢ, while an off-diagonal symmetric pair is a short sum root ±(eᵢ + eⱼ). The proof decomposes a symmetric matrix into its diagonal entries and its strictly upper-triangular entries together with their transposes.

The result works over every commutative ring, including characteristic two. It is one of the Gaussian-decomposition steps needed to prove that, over a field, the root subgroups generate the full symplectic group. That generation theorem identifies the explicit full-weight type-C Kostant carrier with the standard symplectic group on field-valued points.

Main definitions

• TauCeti.GLSymplecticFin.upperUnipotent: the symplectic element with upper-right symmetric block B.
• TauCeti.GLSymplecticFin.lowerUnipotent: the parallel lower-left construction.

Main results

• TauCeti.GLSymplecticFin.upperUnipotent_mem_of_root_subgroups: every upper unipotent belongs to a submonoid containing the positive long- and sum-root elements.
• TauCeti.GLSymplecticFin.lowerUnipotent_mem_of_root_subgroups: the corresponding submonoid statement for negative roots and lower unipotents.

References

• R. W. Carter, Simple Groups of Lie Type (1972), §5.2.
• R. Steinberg, Lectures on Chevalley Groups (1968), §§3--4.

This advances the Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap. The field-valued generation theorem it feeds is needed to identify the type-C pinned carrier consumed by milestone L0 of the CFSGStatement roadmap.

Symmetric block elements

noncomputable def TauCeti.GLSymplecticFin.upperUnipotent {R : Type u} [CommRing R] {m : ℕ} (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : ↥(GLSymplecticFin m R)

The upper unitriangular symplectic element with symmetric upper-right block B.

The result is transported from Fin m ⊕ Fin m coordinates to the Fin (m + m) coordinates used by TauCeti.GLSymplecticFin.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.GLSymplecticFin.lowerUnipotent {R : Type u} [CommRing R] {m : ℕ} (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm) : ↥(GLSymplecticFin m R)

The lower unitriangular symplectic element with symmetric lower-left block C.

The result is transported from Fin m ⊕ Fin m coordinates to the Fin (m + m) coordinates used by TauCeti.GLSymplecticFin.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_mulEquivGLSymplectic_upperUnipotent {R : Type u} [CommRing R] {m : ℕ} (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : (finSumFinEquiv.symm.reindexGL R) ↑(upperUnipotent B hB) = (GLSymplectic.ofSymplecticGroup (Fin m) R) ⟨Matrix.fromBlocks 1 B 0 1, ⋯⟩

In sum coordinates, upperUnipotent B is the block matrix [1 B; 0 1].

@[simp]

theorem TauCeti.GLSymplecticFin.coe_mulEquivGLSymplectic_lowerUnipotent {R : Type u} [CommRing R] {m : ℕ} (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm) : (finSumFinEquiv.symm.reindexGL R) ↑(lowerUnipotent C hC) = (GLSymplectic.ofSymplecticGroup (Fin m) R) ⟨Matrix.fromBlocks 1 0 C 1, ⋯⟩

In sum coordinates, lowerUnipotent C is the block matrix [1 0; C 1].

@[simp]

theorem TauCeti.GLSymplecticFin.upperUnipotent_apply {R : Type u} [CommRing R] {m : ℕ} (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) (i j : Fin m ⊕ Fin m) : ↑↑(upperUnipotent B hB) (finSumFinEquiv i) (finSumFinEquiv j) = Matrix.fromBlocks 1 B 0 1 i j

The entries of an upper unipotent are the entries of the block matrix [1 B; 0 1].

@[simp]

theorem TauCeti.GLSymplecticFin.lowerUnipotent_apply {R : Type u} [CommRing R] {m : ℕ} (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm) (i j : Fin m ⊕ Fin m) : ↑↑(lowerUnipotent C hC) (finSumFinEquiv i) (finSumFinEquiv j) = Matrix.fromBlocks 1 0 C 1 i j

The entries of a lower unipotent are the entries of the block matrix [1 0; C 1].

@[simp]

theorem TauCeti.GLSymplecticFin.coe_upperUnipotent {R : Type u} [CommRing R] {m : ℕ} (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : ↑↑(upperUnipotent B hB) = (Matrix.fromBlocks 1 B 0 1).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

The underlying matrix of an upper unipotent is [1 B; 0 1], reindexed by finSumFinEquiv.

@[simp]

theorem TauCeti.GLSymplecticFin.coe_lowerUnipotent {R : Type u} [CommRing R] {m : ℕ} (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm) : ↑↑(lowerUnipotent C hC) = (Matrix.fromBlocks 1 0 C 1).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

The underlying matrix of a lower unipotent is [1 0; C 1], reindexed by finSumFinEquiv.

@[simp]

theorem TauCeti.GLSymplecticFin.upperUnipotent_inj {R : Type u} [CommRing R] {m : ℕ} (B C : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) (hC : C.IsSymm) : upperUnipotent B hB = upperUnipotent C hC ↔ B = C

Equality of upper unipotents is equivalent to equality of their symmetric blocks.

@[simp]

theorem TauCeti.GLSymplecticFin.lowerUnipotent_inj {R : Type u} [CommRing R] {m : ℕ} (B C : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) (hC : C.IsSymm) : lowerUnipotent B hB = lowerUnipotent C hC ↔ B = C

Equality of lower unipotents is equivalent to equality of their symmetric blocks.

@[simp]

theorem TauCeti.GLSymplecticFin.map_upperUnipotent {R : Type u} [CommRing R] {m : ℕ} {S : Type u_1} [CommRing S] (f : R →+* S) (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : (map m R f) (upperUnipotent B hB) = upperUnipotent (B.map ⇑f) ⋯

Upper unipotents commute with change of coefficient ring.

@[simp]

theorem TauCeti.GLSymplecticFin.map_lowerUnipotent {R : Type u} [CommRing R] {m : ℕ} {S : Type u_1} [CommRing S] (f : R →+* S) (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm) : (map m R f) (lowerUnipotent C hC) = lowerUnipotent (C.map ⇑f) ⋯

Lower unipotents commute with change of coefficient ring.

@[simp]

theorem TauCeti.GLSymplecticFin.upperUnipotent_add {R : Type u} [CommRing R] {m : ℕ} (B C : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) (hC : C.IsSymm) : upperUnipotent (B + C) ⋯ = upperUnipotent B hB * upperUnipotent C hC

Upper unipotent blocks turn addition of symmetric matrices into multiplication.

@[simp]

theorem TauCeti.GLSymplecticFin.lowerUnipotent_add {R : Type u} [CommRing R] {m : ℕ} (B C : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) (hC : C.IsSymm) : lowerUnipotent (B + C) ⋯ = lowerUnipotent B hB * lowerUnipotent C hC

Lower unipotent blocks turn addition of symmetric matrices into multiplication.

@[simp]

theorem TauCeti.GLSymplecticFin.upperUnipotent_zero {R : Type u} [CommRing R] {m : ℕ} : upperUnipotent 0 ⋯ = 1

The upper unipotent attached to the zero matrix is the identity.

@[simp]

theorem TauCeti.GLSymplecticFin.lowerUnipotent_zero {R : Type u} [CommRing R] {m : ℕ} : lowerUnipotent 0 ⋯ = 1

The lower unipotent attached to the zero matrix is the identity.

@[simp]

theorem TauCeti.GLSymplecticFin.inv_upperUnipotent {R : Type u} [CommRing R] {m : ℕ} (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : (upperUnipotent B hB)⁻¹ = upperUnipotent (-B) ⋯

The inverse of an upper unipotent is the upper unipotent of the negated block.

@[simp]

theorem TauCeti.GLSymplecticFin.inv_lowerUnipotent {R : Type u} [CommRing R] {m : ℕ} (C : Matrix (Fin m) (Fin m) R) (hC : C.IsSymm) : (lowerUnipotent C hC)⁻¹ = lowerUnipotent (-C) ⋯

The inverse of a lower unipotent is the lower unipotent of the negated block.

Root matrices

@[simp]

theorem TauCeti.GLSymplecticFin.upperUnipotent_single_self {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (c : R) : upperUnipotent (Matrix.single i i c) ⋯ = positiveLongRootTransvectionUnit i c

A diagonal upper unipotent summand is a positive long-root element.

@[simp]

theorem TauCeti.GLSymplecticFin.lowerUnipotent_single_self {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (c : R) : lowerUnipotent (Matrix.single i i c) ⋯ = negativeLongRootTransvectionUnit i c

A diagonal lower unipotent summand is a negative long-root element.

@[simp]

theorem TauCeti.GLSymplecticFin.upperUnipotent_single_add_transpose {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) : upperUnipotent (Matrix.single i j c + Matrix.single j i c) ⋯ = positiveSumShortRootUnit hij c

An off-diagonal symmetric upper unipotent summand is a positive sum-root element.

@[simp]

theorem TauCeti.GLSymplecticFin.lowerUnipotent_single_add_transpose {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (hij : i ≠ j) (c : R) : lowerUnipotent (Matrix.single i j c + Matrix.single j i c) ⋯ = negativeSumShortRootUnit hij c

An off-diagonal symmetric lower unipotent summand is a negative sum-root element.

Generation

theorem TauCeti.GLSymplecticFin.upperUnipotent_mem_of_root_subgroups {R : Type u} [CommRing R] {m : ℕ} (H : Submonoid ↥(GLSymplecticFin m R)) (hLong : ∀ (i : Fin m) (c : R), positiveLongRootTransvectionUnit i c ∈ H) (hSum : ∀ {i j : Fin m} (hij : i < j) (c : R), positiveSumShortRootUnit ⋯ c ∈ H) (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : upperUnipotent B hB ∈ H

Every upper unipotent block belongs to a submonoid containing the positive long- and sum-root elements for canonically ordered pairs.

theorem TauCeti.GLSymplecticFin.lowerUnipotent_mem_of_root_subgroups {R : Type u} [CommRing R] {m : ℕ} (H : Submonoid ↥(GLSymplecticFin m R)) (hLong : ∀ (i : Fin m) (c : R), negativeLongRootTransvectionUnit i c ∈ H) (hSum : ∀ {i j : Fin m} (hij : i < j) (c : R), negativeSumShortRootUnit ⋯ c ∈ H) (B : Matrix (Fin m) (Fin m) R) (hB : B.IsSymm) : lowerUnipotent B hB ∈ H

Every lower unipotent block belongs to a submonoid containing the negative long- and sum-root elements for canonically ordered pairs.