Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Basic

Root subgroups from Kostant-stable integral modules #

Let U_ℤ = kostantForm e h be a Kostant integral form acting on a rational vector space V, and let M ≤ V be an additive subgroup preserved by U_ℤ. If a designated root vector eᵢ acts nilpotently, its integral divided powers define, over every commutative ring A, an additive one-parameter subgroup

A⁺ → Aut_A(A ⊗[ℤ] M),    t ↦ ∑ₙ tⁿ ρ(eᵢ)⁽ⁿ⁾.

This file proves that these homomorphisms are natural in A, turning the ring-by-ring exponential actions from TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.BaseChangeAction into a natural root-subgroup map on points. Its realization in a finite base-changed basis is provided by TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Coordinate. Integral PBW must still supply a finite free admissible lattice, after which the existing full-faithfulness theorem for the functor of points can recover the scheme morphism 𝔾ₐ → GLₙ.

Main declarations #

References #

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] :
WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A) →* LinearMap.GeneralLinearGroup A (TensorProduct ℤ A ↥M)

The root subgroup attached to a nilpotent root-vector action, on points valued in a commutative ring A.

Under the usual equivalence 𝔾ₐ(A) ≃ A⁺, the parameter t acts on A ⊗[ℤ] M by the finite divided-power exponential of ρ(eᵢ).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_toLinearEquiv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) :
    ((kostantRootSubgroupPoints e h ρ M hM i hnil) f).toLinearEquiv = (baseChangeKostantExpHom e h ρ M hM i hnil) (AdditiveGroup.gaPointsMulEquiv f)

    The linear equivalence underlying a Kostant root-subgroup point is the integral divided-power exponential with the corresponding 𝔾ₐ parameter.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_val {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) :
    ↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) = baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

    The invertible linear map underlying a Kostant root-subgroup point is the base-changed divided-power exponential at the corresponding parameter.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_tmul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_2} [CommRing A] [Algebra ℤ A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (a : A) (m : ↥M) :
    ↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) (a ⊗ₜ[ℤ] m) = ∑ n ∈ Finset.range (nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))), (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ n * a) ⊗ₜ[ℤ] (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M n ⋯) m

    On an elementary tensor, a Kostant root-subgroup point acts by the expected finite divided-power formula.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantRootSubgroupPoints_algHom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra ℤ A] [Algebra ℤ B] (φ : A →ₐ[ℤ] B) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (z : TensorProduct ℤ A ↥M) :
    (TensorProduct.map φ.toLinearMap LinearMap.id) (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) z) = ↑((kostantRootSubgroupPoints e h ρ M hM i hnil) ((AlgHom.mapValue φ) f)) ((TensorProduct.map φ.toLinearMap LinearMap.id) z)

    Kostant root-subgroup points are natural between value rings carrying explicit ℤ-algebra structures.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantRootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] (φ : A →+* B) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (z : TensorProduct ℤ A ↥M) :
    (TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) z) = ↑((kostantRootSubgroupPoints e h ρ M hM i hnil) ((AlgHom.mapValue φ.toIntAlgHom) f)) ((TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) z)

    Kostant root-subgroup points are natural in the value ring. Applying φ to the scalar coordinate of every tensor intertwines the automorphism attached to t : A with the automorphism attached to φ(t) : B.