Documentation

TauCeti.Algebra.Lie.AdjointAction.GradingAut

The grading automorphisms attached to an integral semisimple element #

Let L be a Lie algebra over a commutative ring R and let h ∈ L be an element whose adjoint action is diagonalizable with integer eigenvalues: L is the internal direct sum of the eigenspaces L(j) of ad h at the integers j. The bracket adds eigenvalues (TauCeti.lie_mem_eigenspace_toEnd_add, in TauCeti.Algebra.Lie.Weights.Eigenvector), so L = ⨁ⱼ L(j) is a ℤ-graded Lie algebra, and every unit s of R defines a Lie automorphism TauCeti.gradingAut of L acting on L(j) by s ^ j.

When L is the Lie algebra of an algebraic group G over a field of characteristic zero and h is the differential of a cocharacter λ : 𝔾ₘ → G, the eigenspace L(j) is the weight space of Ad ∘ λ of weight j, so Ad (λ s) acts on L(j) by s ^ j. Since the L(j) span L, Ad (λ s) is the grading automorphism at s. This is how the adjoint action of the cocharacter attached to an sl₂ triple enters the geometry of nilpotent orbits, for instance in the contracting action on a Slodowy slice (TauCeti.Algebra.Lie.Sl2.SlodowySlice.Basic).

Main definitions #

Main results #

source
theorem TauCeti.subsingleton_of_isInternal_eigenspace_of_charP_pos {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) {q : ℕ} [CharP R q] (hq : 0 < q) :
Subsingleton L

In positive characteristic the grading forces L to be trivial. In characteristic q > 0, the eigenspaces of ad h at the integers j and j + q coincide for every j, so independence of the integer eigenspaces makes them all trivial, and L is trivial.

source
noncomputable def TauCeti.gradingAut {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) (s : Rˣ) :
L ≃ₗ⁅R⁆ L

The grading automorphism. If L is the internal direct sum of the integer eigenspaces L(j) of ad h, then for a unit s of R this is the Lie automorphism of L acting on L(j) by s ^ j. It is characterized by TauCeti.gradingAut_apply_of_mem.

When h is the differential of a cocharacter λ of an algebraic group with Lie algebra L, this is the adjoint action Ad (λ s).

Instances For
    source
    theorem TauCeti.gradingAut_apply_of_mem {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) (s : Rˣ) {j : ℤ} {x : L} (hx : x ∈ ((LieAlgebra.ad R L) h).eigenspace ↑j) :
    (gradingAut hh s) x = ↑(s ^ j) • x

    The grading automorphism at s acts on the j-eigenspace of ad h by s ^ j.

    source
    theorem TauCeti.eq_gradingAut {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) {s : Rˣ} {φ : L →ₗ[R] L} (hφ : ∀ (j : ℤ), ∀ x ∈ ((LieAlgebra.ad R L) h).eigenspace ↑j, φ x = ↑(s ^ j) • x) :
    φ = ↑(gradingAut hh s).toLinearEquiv

    A linear map out of L acting on each integer eigenspace L(j) of ad h by s ^ j is the grading automorphism at s.

    source
    theorem TauCeti.gradingAut_mul_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) (s r : Rˣ) (x : L) :
    (gradingAut hh (s * r)) x = (gradingAut hh s) ((gradingAut hh r) x)

    The grading automorphisms compose like the units: gradingAut (s * r) = gradingAut s ∘ gradingAut r.

    source
    @[simp]
    theorem TauCeti.gradingAut_one_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) (x : L) :
    (gradingAut hh 1) x = x

    The grading automorphism at 1 is the identity.

    source
    @[simp]
    theorem TauCeti.gradingAut_symm {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) (s : Rˣ) :
    (gradingAut hh s).symm = gradingAut hh s⁻¹

    The inverse of the grading automorphism at s is the grading automorphism at s⁻¹.

    source
    @[simp]
    theorem TauCeti.gradingAut_apply_self {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} (hh : DirectSum.IsInternal fun (j : ℤ) => ((LieAlgebra.ad R L) h).eigenspace ↑j) (s : Rˣ) :
    (gradingAut hh s) h = h

    The grading automorphisms fix h, which lies in the 0-eigenspace of ad h.