Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.Weyl

Weyl representatives in the Kostant toral closure #

The Weyl element attached to an sl₂ root pair is the product

nᵢ = xᵢ(1) x₋ᵢ(-1) xᵢ(1).

Each factor is a point of the Kostant toral closure, so this product gives a canonical point of the assembled Chevalley carrier over every commutative ring. This file packages that point in the carrier, identifies its matrix with the integral Weyl automorphism of the admissible lattice, and proves that it normalizes the represented split torus. Its conjugation action is the reflection attached to the root and coroot of the sl₂ pair.

These representatives supply the point-level Weyl group data used to transport simple-root subgroups to arbitrary roots and to compare the normalizer of the represented torus with the Weyl group of the root datum.

Main declarations #

References #

The Weyl representative in the carrier #

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralWeylPoint {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (i j : I) (A : Type v) [CommRing A] :
↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)

The Weyl representative xᵢ(1) xⱼ(-1) xᵢ(1) as a point of the Kostant toral closure.

The intended indices i and j are opposite roots in an sl₂ pair. The definition itself only uses their represented root subgroups; the sl₂ relations enter when describing conjugation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantToralWeylPoint {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (φ : A →+* B) (i j : I) :
    (GeneralLinear.mapHopfIdealPointsSubgroup n (kostantToralDefiningIdeal e h ρ M hM hnil b wt) φ.toIntAlgHom) ((MulEquiv.subgroupCongr ⋯) (kostantToralWeylPoint e h ρ M hM hnil b wt i j A)) = (MulEquiv.subgroupCongr ⋯) (kostantToralWeylPoint e h ρ M hM hnil b wt i j B)

    The carrier's Weyl representative is natural in the value ring. Applying a ring homomorphism entrywise sends the representative over the source ring to the representative over the target ring.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralWeylPoint {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (i j : I) (A : Type v) [CommRing A] :
    ↑(kostantToralWeylPoint e h ρ M hM hnil b wt i j A) = (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) (kostantWeylGL e h ρ M hM ⋯ ⋯ A)

    In the chosen basis, the carrier's Weyl representative is the matrix of the integral Weyl automorphism of the admissible lattice.

    Normalization of the represented torus #

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralWeylPoint_conj_rootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {i j : I} {c : κ} (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (A : Type v) [CommRing A] (u : A) :
    kostantToralWeylPoint e h ρ M hM hnil b wt i j A * (kostantToralRootSubgroupPoints e h ρ M hM hnil b wt i A) (Multiplicative.ofAdd u) * (kostantToralWeylPoint e h ρ M hM hnil b wt i j A)⁻¹ = (kostantToralRootSubgroupPoints e h ρ M hM hnil b wt j A) (Multiplicative.ofAdd (-u))

    Conjugation by the carrier's Weyl representative sends the i root subgroup to the j root subgroup, negating the parameter: nᵢ xᵢ(u) nᵢ⁻¹ = xⱼ(-u).

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralWeylPoint_conj_weightTorusPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {i j : I} {c : κ} {α : κ → ℤ} (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (q : κ), ⁅h q, e i⁆ = ↑(α q) • e i) (hαneg : ∀ (q : κ), ⁅h q, e j⁆ = -(↑(α q) • e j)) [DecidableEq κ] (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (A : Type v) [CommRing A] (s : κ → Aˣ) :
    kostantToralWeylPoint e h ρ M hM hnil b wt i j A * (kostantToralWeightTorusPoints e h ρ M hM hnil b wt A) s * (kostantToralWeylPoint e h ρ M hM hnil b wt i j A)⁻¹ = (kostantToralWeightTorusPoints e h ρ M hM hnil b wt A) ((weylReflectTorusPoint α c) s)

    Conjugating a represented weight-torus point by the carrier's Weyl representative reflects the torus point by the root α and its coroot coordinate c.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralWeylPoint_mem_normalizer_weightTorusPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {i j : I} {c : κ} {α : κ → ℤ} (hT : IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hα : ∀ (q : κ), ⁅h q, e i⁆ = ↑(α q) • e i) (hαneg : ∀ (q : κ), ⁅h q, e j⁆ = -(↑(α q) • e j)) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (A : Type v) [CommRing A] :
    kostantToralWeylPoint e h ρ M hM hnil b wt i j A ∈ Subgroup.normalizer ↑(kostantToralWeightTorusPoints e h ρ M hM hnil b wt A).range

    The Weyl representative is in the normalizer of the represented weight torus inside the Kostant toral closure.