Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Torus.LatticeSymmetry

Lattice symmetries of a Kostant torus #

Suppose an additive automorphism of an abelian group preserves a subgroup with a chosen integral basis and acts monomially on that basis. If the induced basis-index map is compatible with a permutation of the torus coordinates through the supplied weight function, then the scalar extension of that automorphism normalizes the corresponding Kostant torus over every commutative ring.

The result is uniform in the value ring and does not require the basis vectors to have been identified as Cartan eigenvectors: all representation-theoretic information needed by the proof is recorded in the weight-compatibility equation. The intended application is a rational representation with a Kostant lattice; there, a numbered diagram symmetry supplies the monomial basis action and its compatibility with the weights of the pinned Geck construction.

Together with the corresponding permutation formula for numbered root subgroups, this supplies the two carrier calculations needed to extend a diagram symmetry to the root-and-torus-generated group.

Main results #

References #

theorem TauCeti.UniversalEnvelopingAlgebra.baseChangeInvariantRestrictUnit_mul_kostantTorusPoints {V : Type u} [AddCommGroup V] (M : AddSubgroup V) {η : Type v} {κ : Type u_1} [Fintype κ] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type w} [CommRing A] [Algebra ℤ A] (θ : V ≃+ V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (τ : η → η) (σ : Equiv.Perm κ) (c : η → ℤ) (hθb : ∀ (i : η), (θ.invariantRestrict M hθM) (b i) = c i • b (τ i)) (hwt : ∀ (i : η) (j : κ), wt (τ i) (σ j) = wt i j) (s : κ → Aˣ) :

A monomial lattice symmetry intertwines the Kostant torus. If the symmetry sends the basis vector indexed by i to a scalar multiple of the one indexed by τ i, and their weights satisfy wt (τ i) (σ j) = wt i j, then the scalar-extended symmetry carries the torus point s past itself as the point obtained by contragredient reindexing through σ. In the intended pinned application this data comes from a numbered diagram symmetry.

theorem TauCeti.UniversalEnvelopingAlgebra.conj_kostantTorusPoints_of_baseChangeInvariantRestrictUnit {V : Type u} [AddCommGroup V] (M : AddSubgroup V) {η : Type v} {κ : Type u_1} [Fintype κ] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type w} [CommRing A] [Algebra ℤ A] (θ : V ≃+ V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (τ : η → η) (σ : Equiv.Perm κ) (c : η → ℤ) (hθb : ∀ (i : η), (θ.invariantRestrict M hθM) (b i) = c i • b (τ i)) (hwt : ∀ (i : η) (j : κ), wt (τ i) (σ j) = wt i j) (s : κ → Aˣ) :

A compatible monomial lattice symmetry conjugates each Kostant torus point by reindexing its coordinates. In the pinned application the lattice symmetry is induced by a numbered diagram symmetry.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusSubgroup_conj_baseChangeInvariantRestrictUnit {V : Type u} [AddCommGroup V] (M : AddSubgroup V) {η : Type v} {κ : Type u_1} [Fintype κ] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (A : Type w) [CommRing A] [Algebra ℤ A] (θ : V ≃+ V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (τ : η → η) (σ : Equiv.Perm κ) (c : η → ℤ) (hθb : ∀ (i : η), (θ.invariantRestrict M hθM) (b i) = c i • b (τ i)) (hwt : ∀ (i : η) (j : κ), wt (τ i) (σ j) = wt i j) :

A compatible monomial lattice symmetry normalizes the Kostant torus subgroup. Conjugation by the scalar-extended symmetry permutes all torus points through σ, hence maps the range of the torus-points homomorphism onto itself. A numbered diagram symmetry supplies this data in the intended pinned application.