Classification of the adjoint roots of the general linear group

For GL_n with its diagonal split torus, this file proves the converse to the matrix-unit weight calculation: every nontrivial adjoint weight is uniquely e_i - e_j for an ordered pair i ≠ j, and its weight space is the line spanned by E_ij. In particular, every such root space has dimension one over the base field.

The proof reads an arbitrary weight vector entrywise. The universal diagonal adjoint action multiplies its (i, j) entry by the group-algebra basis element for e_i - e_j; comparing this with the defining action of its weight shows that every nonzero entry determines the weight.

Main declarations

• TauCeti.GeneralLinear.matrixUnitWeight_eq_of_mem_adjointWeightSpace_of_apply_ne_zero: a nonzero entry of a weight vector determines its weight.
• TauCeti.GeneralLinear.mem_nontrivialAdjointWeights_diagonalTorus_iff: the nontrivial adjoint weights are exactly the characters e_i - e_j with i ≠ j.
• TauCeti.GeneralLinear.adjointWeightSpace_matrixUnitWeight_eq_span_singleton: the e_i - e_j weight space is the line spanned by E_ij.
• TauCeti.GeneralLinear.finrank_adjointWeightSpace_eq_one_of_mem_nontrivialAdjointWeights: every root space has dimension one.

References

• J. S. Milne, Algebraic Groups (2017), §21.1.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3.

This completes the adjoint-root classification for the GL_n worked example in Layer 7, "Root datum of (G,T)", of the ReductiveGroups roadmap.

theorem TauCeti.GeneralLinear.matrixUnitWeight_eq_of_mem_adjointWeightSpace_of_apply_ne_zero {k : Type u} [Field k] {n : ℕ} {alpha : Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ)} {x : Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))} (hx : x ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) alpha) {i j : Fin n} (hentry : cotangentDualMatrixEquiv x i j ≠ 0) : matrixUnitWeight i j = alpha

If the (i, j) entry of an adjoint weight vector is nonzero, then its weight is e_i - e_j.

theorem TauCeti.GeneralLinear.mem_nontrivialAdjointWeights_diagonalTorus_iff {k : Type u} [Field k] {n : ℕ} (alpha : Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ)) : alpha ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) ↔ ∃ (i : Fin n) (j : Fin n), i ≠ j ∧ alpha = matrixUnitWeight i j

The nontrivial adjoint weights of GL_n relative to its diagonal torus are exactly the characters e_i - e_j for ordered pairs i ≠ j.

@[simp]

theorem TauCeti.GeneralLinear.adjointWeightSpace_matrixUnitWeight_eq_span_singleton {k : Type u} [Field k] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) (matrixUnitWeight i j) = k ∙ matrixUnitTangent i j

The adjoint weight space for an off-diagonal character e_i - e_j is exactly the line spanned by the matrix-unit tangent vector E_ij.

@[simp]

theorem TauCeti.GeneralLinear.finrank_adjointWeightSpace_matrixUnitWeight_eq_one {k : Type u} [Field k] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : Module.finrank k ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) (matrixUnitWeight i j)) = 1

Every nontrivial matrix-unit adjoint weight space of GL_n is one-dimensional.

theorem TauCeti.GeneralLinear.finrank_adjointWeightSpace_eq_one_of_mem_nontrivialAdjointWeights {k : Type u} [Field k] {n : ℕ} {alpha : Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ)} (halpha : alpha ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap)) : Module.finrank k ↥(Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) alpha) = 1

Every nontrivial adjoint weight space of GL_n relative to its diagonal torus is one-dimensional.