The root--simple-coroot basis of an integral root--coroot lattice

For a base b of the root system, the integral root--coroot span of an IsSl2System has the expected basis: one root vector for every nonzero root and one coroot for every member of b.support. The index is therefore H.root ⊕ b.support. A Chevalley Lie lattice receives the same basis through its canonical identification with the root--coroot span.

This is the coordinate source for reducing a Chevalley lattice modulo a prime: root coordinates and simple-coroot coordinates remain named after scalar extension.

Main declarations

• TauCeti.IsSl2System.rootSimpleCorootBasis: the corresponding basis of the root--coroot lattice, indexed by H.root ⊕ b.support.
• TauCeti.IsChevalleySystem.rootSimpleCorootBasis: the transported basis of the Chevalley Lie lattice.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §25.2.
• M. Geck, Lie algebras and Chevalley groups, Cambridge Studies in Advanced Mathematics 165, §4.1.

noncomputable def TauCeti.IsSl2System.rootSimpleCorootBasis {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (b : (LieAlgebra.IsKilling.rootSystem H).Base) : Module.Basis (↥LieSubalgebra.root ⊕ ↥b.support) ℤ ↥(rootCorootSpan x)

The integral basis of the root--coroot span consisting of one root vector for every nonzero root and the simple coroots belonging to b.

Equations

• hx.rootSimpleCorootBasis b = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.IsSl2System.coe_rootSimpleCorootBasis_inl {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (b : (LieAlgebra.IsKilling.rootSystem H).Base) (alpha : ↥LieSubalgebra.root) : ↑((hx.rootSimpleCorootBasis b) (Sum.inl alpha)) = x ↑alpha

@[simp]

theorem TauCeti.IsSl2System.coe_rootSimpleCorootBasis_inr {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (b : (LieAlgebra.IsKilling.rootSystem H).Base) (i : ↥b.support) : ↑((hx.rootSimpleCorootBasis b) (Sum.inr i)) = ↑(LieAlgebra.IsKilling.coroot ↑↑i)

noncomputable def TauCeti.IsChevalleySystem.rootSimpleCorootBasis {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (b : (LieAlgebra.IsKilling.rootSystem H).Base) : Module.Basis (↥LieSubalgebra.root ⊕ ↥b.support) ℤ ↥hx.chevalleyLieLattice

The root--simple-coroot basis of the Chevalley Lie lattice, transported from the canonical basis of its underlying root--coroot span.

Equations

• hx.rootSimpleCorootBasis b = (⋯.rootSimpleCorootBasis b).map (LinearEquiv.ofEq (TauCeti.rootCorootSpan x) hx.chevalleyLieLattice.toSubmodule ⋯)

@[simp]

theorem TauCeti.IsChevalleySystem.coe_rootSimpleCorootBasis_inl {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (b : (LieAlgebra.IsKilling.rootSystem H).Base) (alpha : ↥LieSubalgebra.root) : ↑((hx.rootSimpleCorootBasis b) (Sum.inl alpha)) = x ↑alpha

@[simp]

theorem TauCeti.IsChevalleySystem.coe_rootSimpleCorootBasis_inr {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (b : (LieAlgebra.IsKilling.rootSystem H).Base) (i : ↥b.support) : ↑((hx.rootSimpleCorootBasis b) (Sum.inr i)) = ↑(LieAlgebra.IsKilling.coroot ↑↑i)