Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Adjoint.RootSpace

Adjoint root spaces of the general linear group #

For GL_n over a field, restrict the adjoint representation to its diagonal split torus. The matrix unit E_ij is a weight vector of character e_i - e_j: conjugation by diag(t_0, ..., t_{n-1}) multiplies it by t_i t_j⁻¹. This file turns the pointwise matrix calculation in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Adjoint.Basic into membership in the actual comodule weight space Derivation.adjointWeightSpace.

The character is written multiplicatively because the coordinate algebra of the split torus is the group algebra on Multiplicative (ULift (Fin n) →₀ ℤ). Off the diagonal it is nontrivial, so every ordered pair i ≠ j gives an element of Derivation.nontrivialAdjointWeights. On the diagonal the matrix units have trivial weight, identifying the diagonal tangent directions as torus-fixed vectors.

Main declarations #

References #

This is the first worked root calculation for Layer 7, "Root datum of (G,T)", of the ReductiveGroups roadmap. It connects the diagonal torus of GL_n to the abstract adjoint weight-space API from which the root set of a split pair is read.

source
noncomputable def TauCeti.GeneralLinear.matrixUnitWeight {n : ℕ} (i j : Fin n) :
Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ)

The diagonal-torus weight e_i - e_j of the matrix unit E_ij, written as an element of the multiplicative character group of the rank-n split torus.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.toAdd_matrixUnitWeight_apply {n : ℕ} (i j : Fin n) (a : ULift.{u, 0} (Fin n)) :
    (Multiplicative.toAdd (matrixUnitWeight i j)) a = (if a = { down := i } then 1 else 0) - if a = { down := j } then 1 else 0

    The exponent of e_i - e_j at a torus coordinate.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.matrixUnitWeight_self {n : ℕ} (i : Fin n) :
    matrixUnitWeight i i = 1

    The diagonal character e_i - e_i is trivial.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.matrixUnitWeight_eq_one_iff {n : ℕ} (i j : Fin n) :
    matrixUnitWeight i j = 1 ↔ i = j

    The matrix-unit weight e_i - e_j is trivial exactly on the diagonal.

    source
    theorem TauCeti.GeneralLinear.matrixUnitWeight_ne_one {n : ℕ} {i j : Fin n} (hij : i ≠ j) :
    matrixUnitWeight i j ≠ 1

    An off-diagonal root character e_i - e_j is nontrivial.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.matrixUnitWeight_eq_matrixUnitWeight_iff {n : ℕ} {i j : Fin n} (hij : i ≠ j) (a b : Fin n) :
    matrixUnitWeight a b = matrixUnitWeight i j ↔ a = i ∧ b = j

    Off the diagonal, the character e_i - e_j determines the ordered pair (i, j). This follows in the torsion-free character lattice ULift (Fin n) →₀ ℤ, independently of the base field.

    source
    noncomputable def TauCeti.GeneralLinear.matrixUnitTangent {k : Type u} [Field k] {n : ℕ} (i j : Fin n) :
    Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))

    The cotangent-dual tangent vector of GL_n corresponding to the matrix unit E_ij.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.cotangentDualMatrixEquiv_matrixUnitTangent {k : Type u} [Field k] {n : ℕ} (i j : Fin n) :
      cotangentDualMatrixEquiv (matrixUnitTangent i j) = Matrix.single i j 1

      The matrix of matrixUnitTangent i j is the matrix unit E_ij.

      source
      theorem TauCeti.GeneralLinear.tangentMatrix_tangentScalarExtensionEquiv_adjointAction_diagonalTorus_apply {k : Type u} [Field k] {n : ℕ} (x : Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))) (i j : Fin n) :
      (tangentMatrix n) (Derivation.tangentScalarExtensionEquiv (↑((CategoryTheory.ConcreteCategory.hom (Derivation.adjointAction ↧(MonoidAlgebra k (Multiplicative (ULift.{u, 0} (Fin n) →₀ ℤ))))) (WithConv.toConv ↑(CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap))) (1 ⊗ₜ[k] x))) i j = MonoidAlgebra.single (matrixUnitWeight i j) (cotangentDualMatrixEquiv x i j)

      The universal diagonal-torus adjoint action multiplies the (i, j) matrix entry by the character e_i - e_j. Unlike the matrix-unit specialization below, this formula applies to an arbitrary tangent vector and is the coefficient calculation used to classify all nontrivial adjoint weight spaces of GL_n.

      source
      theorem TauCeti.GeneralLinear.matrixUnitTangent_mem_adjointWeightSpace {k : Type u} [Field k] {n : ℕ} (i j : Fin n) :
      matrixUnitTangent i j ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) (matrixUnitWeight i j)

      The matrix unit E_ij belongs to the adjoint weight space of the diagonal-torus character e_i - e_j. This is the formal root-space version of diagonal conjugation scaling the (i, j) matrix entry by t_i t_j⁻¹.

      source
      theorem TauCeti.GeneralLinear.matrixUnitTangent_mem_trivialAdjointWeightSpace {k : Type u} [Field k] {n : ℕ} (i : Fin n) :
      matrixUnitTangent i i ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) 1

      A diagonal matrix unit is fixed by the adjoint action of the diagonal torus.

      source
      theorem TauCeti.GeneralLinear.matrixUnitTangent_ne_zero {k : Type u} [Field k] {n : ℕ} (i j : Fin n) :
      matrixUnitTangent i j ≠ 0

      Every matrix-unit tangent vector is nonzero.

      source
      theorem TauCeti.GeneralLinear.matrixUnitWeight_mem_nontrivialAdjointWeights {k : Type u} [Field k] {n : ℕ} {i j : Fin n} (hij : i ≠ j) :
      matrixUnitWeight i j ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap)

      Every off-diagonal character e_i - e_j occurs as a nontrivial adjoint weight of GL_n relative to its diagonal torus.