Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.Generated.NumberedSymmetry

Numbered symmetries of the generated Kostant group scheme #

A symmetry of numbered Kostant data acts on every scalar extension by conjugation and permutes the represented root subgroups. This file descends that action from algebra-valued matrices to an automorphism of the closed group scheme generated by the root subgroups.

The construction is scheme-theoretic, and its ambient half is TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryCoordinateIso, the automorphism of the coordinate Hopf algebra of GLₙ that conjugation by the base-changed lattice automorphism induces. What this file adds is the descent: that automorphism permutes the root-subgroup coordinate maps, hence preserves their common-kernel Hopf ideal, hence descends to the quotient defining kostantGeneratedGroupScheme.

Main declarations #

References #

This is the graph-automorphism construction used in R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15, and J. E. Humphreys, Linear Algebraic Groups, §27. It advances the pinnings and pinned-isomorphism targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md; the resulting automorphisms are required by milestone L1 of TauCetiRoadmap/CFSGStatement/README.md.

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedNumberedSymmetryIso {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) :
CategoryTheory.Aut (kostantGeneratedGroupScheme e h ρ M hM hnil b)

The automorphism of the generated Kostant group scheme induced by a numbered symmetry.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_comp_numberedSymmetryIso_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (i : I) :
    CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b i) (kostantGeneratedNumberedSymmetryIso e h ρ M hM hnil b σ θ hθM hθe hσ).hom = kostantRootSubgroupToGenerated e h ρ M hM hnil b (σ i)

    The generated group-scheme symmetry carries the ith root subgroup to the one numbered σ i, without changing its additive parameter.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_comp_numberedSymmetryIso_inv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (i : I) :
    CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b (σ i)) (kostantGeneratedNumberedSymmetryIso e h ρ M hM hnil b σ θ hθM hθe hσ).inv = kostantRootSubgroupToGenerated e h ρ M hM hnil b i

    The inverse generated group-scheme symmetry carries the σ ith root subgroup back to the ith root subgroup, without changing its additive parameter.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_comp_numberedSymmetryIso_pow_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (m : ℕ) (i : I) :
    CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b i) (kostantGeneratedNumberedSymmetryIso e h ρ M hM hnil b σ θ hθM hθe hσ ^ m).hom = kostantRootSubgroupToGenerated e h ρ M hM hnil b (σ^[m] i)

    Iterating the generated group-scheme symmetry carries the ith root subgroup to the root subgroup numbered by the corresponding iterate of σ.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedNumberedSymmetryIso_pow_eq_one {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (hσ : Function.Surjective σ) (m : ℕ) (hσm : σ^[m] = id) :
    kostantGeneratedNumberedSymmetryIso e h ρ M hM hnil b σ θ hθM hθe hσ ^ m = 1

    If the numbering permutation has order dividing m, then so does its automorphism of the generated Kostant group scheme.