Matrix coordinates of the parametrized Kostant root subgroups

The root subgroup map x_α with its parameter read in the value ring, kostantRootSubgroupParam, takes values in the automorphisms of a scalar extension A ⊗[ℤ] M. A finite basis b : Basis η ℤ M turns those automorphisms into invertible matrices, and kostantRootSubgroupMatrix is the resulting matrix-valued root subgroup. This file compares the two: in the coordinates of b.baseChange A, a parametrized root-subgroup element is exactly its represented root-subgroup matrix.

The comparison involves neither the represented GLₙ presentation nor any group scheme, so it is stated for an arbitrary finite basis index and lives below the scheme layer.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.basisMatrix_kostantRootSubgroupParam: in basis coordinates, a parametrized Kostant root-subgroup element is its represented root-subgroup matrix.

References

• R. W. Carter, Simple Groups of Lie Type, §4.4.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.basisMatrix_kostantRootSubgroupParam {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type u_3} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_4} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) (A : Type v) [CommRing A] (i : ι) (t : Multiplicative A) : (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) ((kostantRootSubgroupParam e h ρ M hM i ⋯ ↧A) t) = (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm t)

In basis coordinates, a parametrized Kostant root-subgroup element is its represented root-subgroup matrix.