Documentation

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

Numbered symmetries of a Kostant elementary group #

Let U_ℤ = kostantForm e h act on a rational representation V preserving an additive subgroup M ≤ V, so that the divided-power exponentials of the distinguished root vectors eᵢ generate the elementary group E(A) ≤ Aut_A(A ⊗[ℤ] M) of TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Elementary.Basic.

A symmetry of the numbered data is a surjective self-map σ of the index set together with a ℚ-linear automorphism θ of V that preserves M and carries the action of eᵢ to the action of e_{σ i}. Conjugating by the scalar extension of θ is then an automorphism of E(A) which sends each root subgroup to the one indexed by σ without touching its parameters:

γ (xᵢ(t)) = x_{σ i}(t).

These include the equations that a graph automorphism of a Chevalley group is pinned by, restricted to the simple root subgroups, when the numbered symmetry comes from a Dynkin-diagram symmetry. Here γ is defined from a symmetry of the underlying data rather than obtained from the isomorphism theorem for pinned groups, and no uniqueness statement is claimed. Two further properties are what a Steinberg endomorphism built from γ needs. The automorphism commutes with every base change of the value ring, hence in particular with the q-power Frobenius endomorphism of E(A); and if θ ^ n = 1 then γ ^ n = 1, so an involution or a triality of the numbered data produces a γ with γ ^ 2 = 1 or γ ^ 3 = 1.

Nothing here assumes that σ is induced by a symmetry of a Dynkin diagram, nor that θ is unique: both are supplied by the caller as data, and the intertwining hypothesis is the whole input.

Main declarations #

References #

The pinning equation #

source
theorem TauCeti.UniversalEnvelopingAlgebra.baseChangeInvariantRestrictUnit_mul_kostantRootSubgroupParam {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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)) (A : CommAlgCat ℤ) (i : I) (t : Multiplicative ↑A) :
θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM * (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t = (kostantRootSubgroupParam e h ρ M hM (σ i) ⋯ A) t * θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM

Conjugation by the scalar extension of θ carries the root subgroup at i to the root subgroup at σ i, leaving the parameter untouched.

This is the multiplicative form of the pinning equation; the conjugated form is baseChangeInvariantRestrictUnit_conj_kostantRootSubgroupParam.

source
theorem TauCeti.UniversalEnvelopingAlgebra.baseChangeInvariantRestrictUnit_conj_kostantRootSubgroupParam {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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)) (A : CommAlgCat ℤ) (i : I) (t : Multiplicative ↑A) :
θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM * (kostantRootSubgroupParam e h ρ M hM i ⋯ A) t * (θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM)⁻¹ = (kostantRootSubgroupParam e h ρ M hM (σ i) ⋯ A) t

The pinning equation for a numbered symmetry: conjugation by the scalar extension of θ sends xᵢ(t) to x_{σ i}(t).

The automorphism of the elementary group #

source
theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_conj {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) (A : CommAlgCat ℤ) :
Subgroup.map (↑(MulAut.conj (θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM))) (kostantElementarySubgroup e h ρ M hM hnil A) = kostantElementarySubgroup e h ρ M hM hnil A

Conjugation by the scalar extension of θ preserves the elementary group.

Both inclusions come from the pinning equation: the generators at i go to the generators at σ i, and every generator is hit because σ is surjective.

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantElementaryNumberedSymmetryAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) (A : CommAlgCat ℤ) :
MulAut ↥(kostantElementarySubgroup e h ρ M hM hnil A)

The automorphism of the elementary group attached to a symmetry (σ, θ) of the numbered Kostant data: conjugation by the scalar extension of θ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.val_kostantElementaryNumberedSymmetryAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) (A : CommAlgCat ℤ) (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) :
    ↑((kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A) g) = θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM * ↑g * (θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM)⁻¹

    The numbered symmetry acts by conjugation inside the ambient automorphism group.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryNumberedSymmetryAut_kostantRootSubgroupParam {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) (A : CommAlgCat ℤ) (i : I) (t : Multiplicative ↑A) :
    (kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A) ⟨(kostantRootSubgroupParam e h ρ M hM i ⋯ A) t, ⋯⟩ = ⟨(kostantRootSubgroupParam e h ρ M hM (σ i) ⋯ A) t, ⋯⟩

    The numbered symmetry sends the root subgroup at i to the one at σ i, leaving parameters untouched.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryNumberedSymmetryAut_pow_eq_one {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) (A : CommAlgCat ℤ) {n : ℕ} (hn : ∀ (v : V), (θ ^ n) v = v) :
    kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A ^ n = 1

    A numbered symmetry of order n produces an automorphism of order dividing n.

    This is what makes the order relations γ ^ 2 = 1 and γ ^ 3 = 1 available for the graph-twisted families, where θ realizes an involution or a triality of the numbered data.

    Compatibility with base change and Frobenius #

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryMap_kostantElementaryNumberedSymmetryAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) {A B : CommAlgCat ℤ} (φ : A ⟶ B) (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) :
    (kostantElementaryMap e h ρ M hM hnil φ) ((kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A) g) = (kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ B) ((kostantElementaryMap e h ρ M hM hnil φ) g)

    The numbered symmetry commutes with base change of the value ring.

    The scalar extension of θ is defined over ℤ, so extending scalars along φ leaves it unchanged, and conjugation by it is therefore natural.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantElementaryFrobenius_kostantElementaryNumberedSymmetryAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type u_1} {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (σ : 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 σ) (p n : ℕ) (A : CommAlgCat ℤ) [ExpChar (↑A) p] (g : ↥(kostantElementarySubgroup e h ρ M hM hnil A)) :
    (kostantElementaryFrobenius e h ρ M hM hnil p n A) ((kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A) g) = (kostantElementaryNumberedSymmetryAut e h ρ M hM hnil σ θ hθM hθe hσ A) ((kostantElementaryFrobenius e h ρ M hM hnil p n A) g)

    The numbered symmetry commutes with the p ^ n-power Frobenius endomorphism.

    Together with the pinning equation and the order relation, this is the compatibility a Steinberg endomorphism of the form γ ∘ Frob_q is built from.