Exponentials along the filtration of a centralizer

Let L be a Lie algebra, e ∈ L, and 𝔲ₖ = ker (ad e) ⊓ range ((ad e) ^ k) the filtration of the centralizer of e from TauCeti.Algebra.Lie.AdjointAction.CentralizerFiltration. For an ad-nilpotent y ∈ 𝔲₁ = ker (ad e) ⊓ [e, L] the inner automorphism exp (ad y) fixes e.

This file introduces the subgroup of linear automorphisms of L generated by these exp (ad y), the group in which Kostant's conjugacy theorem for sl₂ triples takes place, and records how exp (ad y) moves vectors along the filtration: over a field of characteristic zero, if y and ⁅y, v⁆ lie in 𝔲ₖ then exp (ad y) v = v + ⁅y, v⁆ modulo 𝔲₂ₖ, because the bracket compatibility ⁅𝔲ᵢ, 𝔲ⱼ⁆ ⊆ 𝔲ᵢ₊ⱼ pushes every higher term of the exponential series into 𝔲₂ₖ.

Main definitions

• TauCeti.expAdSubgroup: the subgroup generated by the exp (ad y) with y ∈ ker (ad e) ⊓ [e, L].

Main results

• TauCeti.expAdSubgroup_le_iff: the universal property of TauCeti.expAdSubgroup.
• TauCeti.expAdSubgroup_le_stabilizer: TauCeti.expAdSubgroup fixes e.
• TauCeti.map_expAdSubgroup_le_intLieAlgebra: TauCeti.expAdSubgroup lies in the group TauCeti.intLieAlgebra K L of inner automorphisms.
• TauCeti.expAd_apply_sub_sub_mem: exp (ad y) v - v - ⁅y, v⁆ ∈ 𝔲₂ₖ when y, ⁅y, v⁆ ∈ 𝔲ₖ.

References

• B. Kostant, The principal three-dimensional subgroup and the Betti numbers of a complex simple Lie group, Amer. J. Math. 81 (1959), 973–1032.
• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §3.4.

The subgroup generated by the exp (ad y)

def TauCeti.expAdSubgroup (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (e : L) : Subgroup (L ≃ₗ[K] L)

The subgroup of linear automorphisms of L generated by the automorphisms exp (ad y) with y ∈ ker (ad e) ⊓ [e, L]. Kostant's conjugacy theorem takes place in this subgroup.

theorem TauCeti.expAd_toLinearEquiv_mem_expAdSubgroup {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {e y : L} (hy : IsNilpotent ((LieAlgebra.ad K L) y)) (hye : y ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e)) : (expAd y ⋯).toLinearEquiv ∈ expAdSubgroup K e

Each generator exp (ad y), y ∈ ker (ad e) ⊓ [e, L], lies in TauCeti.expAdSubgroup.

theorem TauCeti.expAdSubgroup_le_iff {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {e : L} {H : Subgroup (L ≃ₗ[K] L)} : expAdSubgroup K e ≤ H ↔ ∀ (y : L) (hy : IsNilpotent ((LieAlgebra.ad K L) y)), y ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e) → (expAd y ⋯).toLinearEquiv ∈ H

TauCeti.expAdSubgroup K e lies in a subgroup H if and only if every generator exp (ad y), y ∈ ker (ad e) ⊓ [e, L], does.

theorem TauCeti.expAdSubgroup_le_stabilizer {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (e : L) : expAdSubgroup K e ≤ MulAction.stabilizer (L ≃ₗ[K] L) e

TauCeti.expAdSubgroup K e lies in the stabilizer of e: each generator exp (ad y) fixes e because ⁅y, e⁆ = 0.

theorem TauCeti.apply_eq_self_of_mem_expAdSubgroup {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {e : L} {ψ : L ≃ₗ[K] L} (hψ : ψ ∈ expAdSubgroup K e) : ψ e = e

Every element of TauCeti.expAdSubgroup K e fixes e.

theorem TauCeti.map_expAdSubgroup_le_intLieAlgebra {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (e : L) : Subgroup.map (LinearMap.GeneralLinearGroup.generalLinearEquiv K L).symm.toMonoidHom (expAdSubgroup K e) ≤ intLieAlgebra K L

Kostant's subgroup lies in Int L: the subgroup TauCeti.expAdSubgroup K e of linear automorphisms generated by the exp (ad y) with y ∈ ker (ad e) ⊓ [e, L] is contained in Int L under the identification of linear automorphisms with the general linear group.

exp (ad y) along the filtration

theorem TauCeti.expAd_apply_sub_sub_mem {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {e y v : L} {k : ℕ} (hy : IsNilpotent ((LieAlgebra.ad K L) y)) (hyk : y ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ k)) (hyv : ⁅y, v⁆ ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ k)) : (expAd y ⋯) v - v - ⁅y, v⁆ ∈ LinearMap.ker ((LieAlgebra.ad K L) e) ⊓ LinearMap.range ((LieAlgebra.ad K L) e ^ (k + k))

If y lies in the k-th step of the filtration of the centralizer of e and ⁅y, v⁆ does too, then exp (ad y) v = v + ⁅y, v⁆ up to the 2k-th step.