Documentation

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

Numbered symmetries of the Kostant toral-closure group scheme #

The closed subgroup scheme of GLₙ generated by the represented Kostant root subgroups together with the weight torus of an integral weight family is the carrier of the Chevalley--Demazure construction. This file makes it inherit the automorphism that a symmetry of the numbered Kostant data induces on GLₙ.

Two hypotheses are needed beyond those of the root-generated case, and they are exactly what the torus contributes. The rational automorphism θ must act monomially on the chosen lattice basis, by a permutation π of Fin n and integral scaling coefficients; and the weights must be equivariant for π and a permutation τ of the torus index, wt (π i) (τ k) = wt i k. The scaling coefficients cancel from diagonal conjugation, so the symmetry normalizes the diagonal torus of GLₙ, and equivariance identifies the relabelled weight family with the original one. On the represented generators the resulting automorphism acts by

γ ∘ xᵢ = x_{σ i},        γ ∘ (weight torus) = (weight torus) ∘ relabel(τ⁻¹),

and it has order dividing any m for which σ iterates and τ powers to the identity.

The invariance of the defining Hopf ideal that makes all of this work also says that conjugation by the numbered-symmetry matrix preserves the algebra-valued points of the toral closure. That form of the statement is proved here too, since it is the one a consumer working with a point group rather than with the group scheme needs, and it rests on the same ideal computation. The two are compared: on an algebra-valued point of the carrier, composing with the automorphism of the group scheme and including into GLₙ is that same matrix conjugation.

Both hypotheses hold for the coordinate permutation that a Dynkin-diagram symmetry induces on Geck's lattice: it permutes the coordinate basis by the induced permutation of the Cartan coordinates and of the roots, and it permutes the Geck weights contragrediently. Allowing monomial basis actions also covers pinned lifts, such as the graph symmetry used for ²E₆, that require signs.

Nothing here assumes that σ or τ comes from a diagram symmetry, that the weights are those of an admissible lattice, or that the carrier is reductive.

Main declarations #

Main results #

All of these live in the TauCeti.UniversalEnvelopingAlgebra namespace.

References #

This is the graph-automorphism construction of R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15, and J. E. Humphreys, Linear Algebraic Groups, §27, carried out on the carrier assembled from a torus and root subgroups in R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.

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.kostantToralNumberedSymmetryIso {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) :
CategoryTheory.Aut (kostantToralGroupScheme e h ρ M hM hnil b wt)

The automorphism of the Kostant toral-closure group scheme induced by a numbered symmetry which acts monomially on the chosen lattice basis compatibly with the weights.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToToral_comp_numberedSymmetryIso_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (i : I) :
    CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt).hom = kostantRootSubgroupToToral e h ρ M hM hnil b wt (σ i)

    The toral symmetry carries the ith root subgroup to the one numbered σ i, without changing its additive parameter.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToToral_comp_numberedSymmetryIso_inv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (i : I) :
    CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt (σ i)) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt).inv = kostantRootSubgroupToToral e h ρ M hM hnil b wt i

    The inverse toral symmetry carries the σ ith root subgroup back to the ith one.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral_comp_numberedSymmetryIso_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) :
    CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt).hom = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ torusPerm⁻¹) (kostantWeightTorusToToral e h ρ M hM hnil b wt)

    The toral symmetry normalizes the represented weight torus, acting on it by the relabelling attached to the torus permutation.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral_comp_numberedSymmetryIso_inv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) :
    CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt).inv = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ torusPerm) (kostantWeightTorusToToral e h ρ M hM hnil b wt)

    The inverse toral symmetry acts on the represented weight torus by the inverse relabelling.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedToToral_comp_numberedSymmetryIso_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) :
    CategoryTheory.CategoryStruct.comp (kostantGeneratedToToral e h ρ M hM hnil b wt) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt).hom = CategoryTheory.CategoryStruct.comp (kostantGeneratedNumberedSymmetryIso e h ρ M hM hnil b σ θ hθM hθe hσ).hom (kostantGeneratedToToral e h ρ M hM hnil b wt)

    The root-generated and toral numbered symmetries agree along the canonical closed immersion from the generated carrier into the toral closure.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToToral_comp_numberedSymmetryIso_pow_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (m : ℕ) (i : I) :
    CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt ^ m).hom = kostantRootSubgroupToToral e h ρ M hM hnil b wt (σ^[m] i)

    Iterating the toral symmetry carries the ith root subgroup to the root subgroup numbered by the corresponding iterate of σ.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral_comp_numberedSymmetryIso_pow_hom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (m : ℕ) :
    CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt ^ m).hom = CategoryTheory.CategoryStruct.comp (SplitTorus.relabel ℤ (torusPerm⁻¹ ^ m)) (kostantWeightTorusToToral e h ρ M hM hnil b wt)

    Iterating the toral symmetry acts on the weight torus by the corresponding power of the relabelling.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralNumberedSymmetryIso_pow_eq_one {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (m : ℕ) (hσm : σ^[m] = id) (hτm : torusPerm ^ m = 1) :
    kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt ^ m = 1

    If the numbering permutation and the torus permutation both have order dividing m, so does the induced automorphism of the toral closure. An involution or a triality of the numbered data therefore produces a symmetry with γ ^ 2 = 1 or γ ^ 3 = 1.

    The symmetry on algebra-valued points #

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.conj_kostantNumberedSymmetryMatrix_mem_kostantToralPointsSubgroup_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (A : Type v) [CommRing A] (g : GL (Fin n) A) :
    kostantNumberedSymmetryMatrix M b θ hθM A * g * (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹ ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A ↔ g ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A

    Conjugating by the matrix of a numbered symmetry preserves the algebra-valued points of the toral closure, in both directions. The symmetry permutes the represented root subgroups and carries the represented weight torus to itself, so it preserves the Hopf ideal cut out by them and hence the matrices which kill that ideal.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantToralPointsSubgroup_conj_numberedSymmetryMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (A : Type v) [CommRing A] :
    Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM A))) (kostantToralPointsSubgroup e h ρ M hM hnil b wt A) = kostantToralPointsSubgroup e h ρ M hM hnil b wt A

    The matrix of a numbered symmetry normalizes the algebra-valued points of the toral closure. This is the form in which conjugation by that matrix restricts to an automorphism of the point group.

    The symmetry on scheme-valued points #

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantToralNumberedSymmetryIso {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {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 → 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 σ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (torusPerm : Equiv.Perm κ) (hwt : ∀ (i : Fin n) (k : κ), wt (basisPerm i) (torusPerm k) = wt i k) (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (kostantToralGroupScheme e h ρ M hM hnil b wt).X) :
    (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (kostantToralNumberedSymmetryIso e h ρ M hM hnil b wt σ θ hθM hθe hσ basisPerm basisScale hbasis torusPerm hwt).hom.hom.hom (kostantToralGroupSchemeι e h ρ M hM hnil b wt).hom.hom)) = kostantNumberedSymmetryMatrix M b θ hθM A * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (kostantToralGroupSchemeι e h ρ M hM hnil b wt).hom.hom) * (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹

    On every algebra-valued point of the toral closure, the numbered-symmetry automorphism of the group scheme is conjugation by the numbered-symmetry matrix. This identifies the automorphism kostantToralNumberedSymmetryIso of the carrier with the matrix conjugation that conj_kostantNumberedSymmetryMatrix_mem_kostantToralPointsSubgroup_iff shows preserves the point group: the two constructions, one through the defining Hopf ideal and one through the coordinate automorphism, agree.