Coordinate roots for the diagonal torus in the general linear group

This file specializes SplitTorus.coordinateRootDatum to the coordinate lattice ULift (Fin n). Its roots and coroots are the vectors e_i - e_j, and reflections transpose the two coordinates indexed by the reflecting root.

The construction supplies the expected coordinate root datum and proves that each of its roots, viewed as a multiplicative character, occurs among the nontrivial adjoint weights of GL_n. Only this inclusion into Derivation.nontrivialAdjointWeights is proved here; the converse identification with the packaged root set is proved in GeneralLinear.Root.Adjoint.

The character and cocharacter lattices are the established split-torus coordinate models

X*(T) = ULift (Fin n) →₀ ℤ,    X_*(T) = ULift (Fin n) → ℤ.

Main declarations

• TauCeti.GeneralLinear.DiagonalRootIndex: ordered off-diagonal coordinate pairs.
• TauCeti.GeneralLinear.diagonalRoot and diagonalCoroot: the vectors e_i - e_j, defined for arbitrary pairs of matrix indices.
• TauCeti.GeneralLinear.diagonalRootDatum: the coordinate-difference root datum specialized to the diagonal torus lattice of GL_n.
• TauCeti.GeneralLinear.diagonalRootDatum_pairing_apply: the closed Cartan-integer formula.
• TauCeti.GeneralLinear.diagonalRootDatum_reflection_apply and diagonalRootDatum_coreflection_apply: reflections transpose arbitrary character and cocharacter coordinates.
• TauCeti.GeneralLinear.diagonalRootDatum_reflectionPerm: reflections act by simultaneous coordinate transposition on the two indices.
• TauCeti.GeneralLinear.ofAdd_root_mem_nontrivialAdjointWeights: every packaged root occurs as a nontrivial adjoint weight.
• TauCeti.GeneralLinear.diagonalCorootCocharacter: the genuine split-torus cocharacter with a prescribed coordinate coroot.
• TauCeti.GeneralLinear.pairing_matrixUnitWeight_diagonalCorootCocharacter: evaluation of a matrix-unit weight on such a cocharacter agrees with the root-datum pairing.

References

• J. S. Milne, Algebraic Groups (2017), Example 19.7 and Section 21.1.
• J. E. Humphreys, Linear Algebraic Groups (1975), Sections 16.1 and 26.3.

This advances Layer 7, "Root datum of (G, T)", of the ReductiveGroups roadmap through its standard GL_n split-coordinate example.

@[reducible, inline]

abbrev TauCeti.GeneralLinear.DiagonalRootIndex (n : ℕ) : Type u

Ordered pairs of distinct lifted matrix coordinates indexing the packaged roots.

Equations

• TauCeti.GeneralLinear.DiagonalRootIndex n = TauCeti.SplitTorus.CoordinateRootIndex (ULift.{?u.1, 0} (Fin n))

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

The character-lattice vector e_i - e_j, defined for arbitrary matrix indices.

Equations

• TauCeti.GeneralLinear.diagonalRoot i j = Multiplicative.toAdd (TauCeti.GeneralLinear.matrixUnitWeight i j)

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

The cocharacter-lattice vector e_i - e_j, defined for arbitrary matrix indices.

Equations

• TauCeti.GeneralLinear.diagonalCoroot i j = ⇑(TauCeti.GeneralLinear.diagonalRoot i j)

@[simp]

theorem TauCeti.GeneralLinear.diagonalRoot_apply {n : ℕ} (i j : Fin n) (a : ULift.{u, 0} (Fin n)) : (diagonalRoot i j) a = (if a = { down := i } then 1 else 0) - if a = { down := j } then 1 else 0

Evaluation of a diagonal root at a torus coordinate.

@[simp]

theorem TauCeti.GeneralLinear.diagonalCoroot_apply {n : ℕ} (i j : Fin n) (a : ULift.{u, 0} (Fin n)) : diagonalCoroot i j a = (if a = { down := i } then 1 else 0) - if a = { down := j } then 1 else 0

Evaluation of a diagonal coroot at a torus coordinate.

theorem TauCeti.GeneralLinear.coe_diagonalRoot {n : ℕ} (i j : Fin n) : ⇑(diagonalRoot i j) = diagonalCoroot i j

A diagonal coroot is the function underlying the corresponding diagonal root.

theorem TauCeti.GeneralLinear.diagonalRoot_eq_coordinateRoot {n : ℕ} (i j : Fin n) : diagonalRoot i j = SplitTorus.coordinateRoot { down := i } { down := j }

A diagonal root is the corresponding root of the coordinate root datum.

theorem TauCeti.GeneralLinear.diagonalCoroot_eq_coordinateCoroot {n : ℕ} (i j : Fin n) : diagonalCoroot i j = SplitTorus.coordinateCoroot { down := i } { down := j }

A diagonal coroot is the corresponding coroot of the coordinate root datum.

noncomputable def TauCeti.GeneralLinear.diagonalRootDatum (n : ℕ) : RootDatum (DiagonalRootIndex n) (ULift.{u, 0} (Fin n) →₀ ℤ) (ULift.{u, 0} (Fin n) → ℤ)

The coordinate root datum on the diagonal split-torus lattices of GL_n.

This package is constructed directly from the coordinate differences. The theorem ofAdd_root_mem_nontrivialAdjointWeights proves that its roots are adjoint weights; the converse classification is mem_nontrivialAdjointWeights_iff_exists_diagonalRoot in GeneralLinear.Root.Adjoint.

Equations

• TauCeti.GeneralLinear.diagonalRootDatum n = TauCeti.SplitTorus.coordinateRootDatum (ULift.{?u.1, 0} (Fin n))

theorem TauCeti.GeneralLinear.diagonalRootDatum_eq_coordinateRootDatum (n : ℕ) : diagonalRootDatum n = SplitTorus.coordinateRootDatum (ULift.{u, 0} (Fin n))

The diagonal root datum is the coordinate root datum on the universe-lifted indices.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_toLinearMap (n : ℕ) : (diagonalRootDatum n).toLinearMap = SplitTorus.dotPairing

The underlying bilinear map is the split-torus character--cocharacter dot pairing.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_root {n : ℕ} (p : DiagonalRootIndex n) : (diagonalRootDatum n).root p = diagonalRoot (↑p).1.down (↑p).2.down

The roots of diagonalRootDatum are the matrix-coordinate differences e_i - e_j.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_coroot {n : ℕ} (p : DiagonalRootIndex n) : (diagonalRootDatum n).coroot p = diagonalCoroot (↑p).1.down (↑p).2.down

The coroots of diagonalRootDatum are the matrix-coordinate differences e_i - e_j.

theorem TauCeti.GeneralLinear.diagonalRootDatum_pairing {n : ℕ} (p q : DiagonalRootIndex n) : RootPairing.pairing (diagonalRootDatum n) p q = (SplitTorus.dotPairing (diagonalRoot (↑p).1.down (↑p).2.down)) (diagonalCoroot (↑q).1.down (↑q).2.down)

The root-datum pairing is the split-torus dot product on diagonal root and coroot vectors. This bridge is not a simp lemma; diagonalRootDatum_pairing_apply is the normal form.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_pairing_apply {n : ℕ} (p q : DiagonalRootIndex n) : RootPairing.pairing (diagonalRootDatum n) p q = ((if (↑p).1 = (↑q).1 then 1 else 0) - if (↑p).1 = (↑q).2 then 1 else 0) - ((if (↑p).2 = (↑q).1 then 1 else 0) - if (↑p).2 = (↑q).2 then 1 else 0)

Closed formula for the Cartan integers of the diagonal coordinate root datum.

noncomputable def TauCeti.GeneralLinear.diagonalReflectionIndex {n : ℕ} (p q : DiagonalRootIndex n) : DiagonalRootIndex n

The index of the root obtained by applying the reflection in the root indexed by p to the root indexed by q: both entries of q are transposed by Equiv.swap p.1.1 p.1.2.

Equations

• TauCeti.GeneralLinear.diagonalReflectionIndex p q = (TauCeti.SplitTorus.coordinatePermRootIndex (Equiv.swap (↑p).1 (↑p).2)) q

@[simp]

theorem TauCeti.GeneralLinear.diagonalReflectionIndex_coe {n : ℕ} (p q : DiagonalRootIndex n) : ↑(diagonalReflectionIndex p q) = ((Equiv.swap (↑p).1 (↑p).2) (↑q).1, (Equiv.swap (↑p).1 (↑p).2) (↑q).2)

The two entries of diagonalReflectionIndex p q are the corresponding coordinate swaps.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_reflectionPerm {n : ℕ} (p q : DiagonalRootIndex n) : ((diagonalRootDatum n).reflectionPerm p) q = diagonalReflectionIndex p q

The reflection associated to a root acts on indices by transposing both coordinates.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_reflection_apply {n : ℕ} (p : DiagonalRootIndex n) (x : ULift.{u, 0} (Fin n) →₀ ℤ) (a : ULift.{u, 0} (Fin n)) : ((RootPairing.reflection (diagonalRootDatum n) p) x) a = x ((Equiv.swap (↑p).1 (↑p).2) a)

Reflection in the diagonal root indexed by p precomposes an arbitrary character with the corresponding coordinate transposition.

@[simp]

theorem TauCeti.GeneralLinear.diagonalRootDatum_coreflection_apply {n : ℕ} (p : DiagonalRootIndex n) (x : ULift.{u, 0} (Fin n) → ℤ) (a : ULift.{u, 0} (Fin n)) : (RootPairing.coreflection (diagonalRootDatum n) p) x a = x ((Equiv.swap (↑p).1 (↑p).2) a)

Coreflection in the diagonal root indexed by p precomposes an arbitrary cocharacter with the corresponding coordinate transposition.

instance TauCeti.GeneralLinear.isReduced_diagonalRootDatum (n : ℕ) : RootPairing.IsReduced (diagonalRootDatum n)

The diagonal coordinate root datum is reduced.

@[simp]

theorem TauCeti.GeneralLinear.ofAdd_diagonalRoot {n : ℕ} (i j : Fin n) : Multiplicative.ofAdd (diagonalRoot i j) = matrixUnitWeight i j

A diagonal root, viewed multiplicatively, is the corresponding matrix-unit weight.

theorem TauCeti.GeneralLinear.ofAdd_root_mem_nontrivialAdjointWeights {k : Type u} [Field k] {n : ℕ} (p : DiagonalRootIndex n) : Multiplicative.ofAdd ((diagonalRootDatum n).root p) ∈ Derivation.nontrivialAdjointWeights (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap)

Every root in the diagonal coordinate root datum occurs as a nontrivial adjoint weight of GL_n. This is the proved inclusion from the packaged root set into the adjoint weight set.

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

The genuine cocharacter whose coordinate vector is the coroot e_i - e_j.

Equations

• TauCeti.GeneralLinear.diagonalCorootCocharacter i j = TauCeti.SplitTorus.cocharEquiv.symm (TauCeti.GeneralLinear.diagonalCoroot i j)

@[simp]

theorem TauCeti.GeneralLinear.cocharEquiv_diagonalCorootCocharacter {n : ℕ} (i j : Fin n) : SplitTorus.cocharEquiv (diagonalCorootCocharacter i j) = diagonalCoroot i j

The coordinates of diagonalCorootCocharacter i j are the coroot e_i - e_j.

theorem TauCeti.GeneralLinear.pairing_matrixUnitWeight_diagonalCorootCocharacter {n : ℕ} (p q : DiagonalRootIndex n) : DiagonalizableGroup.pairing (matrixUnitWeight (↑p).1.down (↑p).2.down) (diagonalCorootCocharacter (↑q).1.down (↑q).2.down) = RootPairing.pairing (diagonalRootDatum n) p q

Evaluation of a matrix-unit weight on a diagonal coroot cocharacter is the pairing of the diagonal coordinate root datum.