The type A weight torus and its maximality on field-valued points

Over any commutative ring, the standard carrier's weight-torus points are precisely the determinant-one diagonal matrices. Over an infinite field, their centralizer is exactly that diagonal subgroup, so they form a maximal commutative subgroup of the carrier points.

Main declarations

• TauCeti.SlStd.centralizer_range_weightTorusPoints_eq_diagonalPoints: over an infinite field, the centralizer of the weight torus is the determinant-one diagonal subgroup.
• TauCeti.SlStd.range_weightTorusPoints_eq_diagonalPoints: the weight torus consists of all determinant-one diagonal carrier points.
• TauCeti.SlStd.eq_range_weightTorusPoints_of_le_of_isMulCommutative: the weight torus is maximal among commutative subgroups of the carrier points over an infinite field.

References

• R. W. Carter, Simple Groups of Lie Type, §7.1.
• J. E. Humphreys, Linear Algebraic Groups, §§15.3 and 16.1.

theorem TauCeti.SlStd.torusCharacter_weight (r : ℕ) (K : Type u) [CommRing K] (s : Fin r → Kˣ) (k : Fin (r + 1)) : torusCharacter s (weight r k) = (if hk : ↑k < r then s ⟨↑k, hk⟩ else 1) * if hk : 0 < ↑k then (s ⟨↑k - 1, ⋯⟩)⁻¹ else 1

The character of the standard weight at coordinate k is the quotient of the adjacent torus parameters. Missing factors at the two ends are interpreted as one.

theorem TauCeti.SlStd.torusCharacter_partialProd (r : ℕ) {K : Type u} [CommRing K] (t : Fin (r + 1) → Kˣ) (ht : ∏ i : Fin (r + 1), t i = 1) (k : Fin (r + 1)) : torusCharacter (fun (i : Fin r) => Fin.partialProd t i.succ.castSucc) (weight r k) = t k

On a determinant-one diagonal tuple, the partial products evaluate under the standard weight characters to the original tuple.

Diagonal points and the weight-torus range

noncomputable def TauCeti.SlStd.diagonalPoints (r : ℕ) (K : Type u) [CommRing K] : Subgroup ↥(points r K)

The diagonal points of the standard carrier.

Equations

• TauCeti.SlStd.diagonalPoints r K = Subgroup.comap (TauCeti.SlStd.points r K).subtype (TauCeti.diagonalTorus K (r + 1))

@[simp]

theorem TauCeti.SlStd.mem_diagonalPoints_iff (r : ℕ) {K : Type u} [CommRing K] {g : ↥(points r K)} : g ∈ diagonalPoints r K ↔ (↑↑g).IsDiag

A carrier point lies in diagonalPoints exactly when its ambient matrix is diagonal.

theorem TauCeti.SlStd.coe_weightTorusPoints_mem_diagonalTorus (r : ℕ) (K : Type u) [CommRing K] (s : Fin r → Kˣ) : ↑((weightTorusPoints r K) s) ∈ diagonalTorus K (r + 1)

Every standard weight-torus point is diagonal in the ambient general linear group.

theorem TauCeti.SlStd.coe_weightTorusPoints_partialProd (r : ℕ) {K : Type u} [CommRing K] (t : Fin (r + 1) → Kˣ) (ht : ∏ i : Fin (r + 1), t i = 1) : ↑((weightTorusPoints r K) fun (i : Fin r) => Fin.partialProd t i.succ.castSucc) = diagGL t

The partial products of a determinant-one diagonal tuple give an explicit preimage under the standard weight-torus parametrization.

The centralizer and maximality

theorem TauCeti.SlStd.centralizer_range_weightTorusPoints_eq_diagonalPoints_of_weightChar_weight_injective (r : ℕ) (K : Type u) [CommRing K] [IsCancelMulZero K] (hchar : Function.Injective (weightChar K ∘ weight r)) : Subgroup.centralizer ↑(weightTorusPoints r K).range = diagonalPoints r K

If the standard weight characters are distinct over a ring without zero divisors, the centralizer of the weight torus in the carrier points is exactly the diagonal subgroup.

theorem TauCeti.SlStd.centralizer_range_weightTorusPoints_eq_diagonalPoints (r : ℕ) (K : Type u) [Field K] [Infinite K] : Subgroup.centralizer ↑(weightTorusPoints r K).range = diagonalPoints r K

Over an infinite field, the centralizer of the weight torus in the carrier points is exactly the diagonal subgroup.

@[simp]

theorem TauCeti.SlStd.range_weightTorusPoints_eq_diagonalPoints (r : ℕ) (K : Type u) [CommRing K] : (weightTorusPoints r K).range = diagonalPoints r K

Over a commutative ring, the standard weight torus consists of all diagonal carrier points. Thus every diagonal carrier point admits a standard weight-torus parametrization.

theorem TauCeti.SlStd.eq_range_weightTorusPoints_of_weightChar_weight_injective_of_le_of_isMulCommutative (r : ℕ) (K : Type u) [CommRing K] [IsCancelMulZero K] (hchar : Function.Injective (weightChar K ∘ weight r)) (H : Subgroup ↥(points r K)) [IsMulCommutative ↥H] (hle : (weightTorusPoints r K).range ≤ H) : H = (weightTorusPoints r K).range

If its weight characters are distinct over a ring without zero divisors, the standard weight torus is maximal among commutative subgroups of the type A_r carrier.

theorem TauCeti.SlStd.eq_range_weightTorusPoints_of_le_of_isMulCommutative (r : ℕ) (K : Type u) [Field K] [Infinite K] (H : Subgroup ↥(points r K)) [IsMulCommutative ↥H] (hle : (weightTorusPoints r K).range ≤ H) : H = (weightTorusPoints r K).range

The standard weight torus is maximal among commutative subgroups of the type A_r carrier over an infinite field.