The group of inner automorphisms of a Lie algebra

For an element x of a Lie algebra L whose adjoint action is nilpotent, exp (ad x) is an automorphism of L (TauCeti.expAd). The group Int L of inner automorphisms is the subgroup of the general linear group of L generated by these exponentials. This file defines it as TauCeti.intLieAlgebra K L and proves:

• every element of Int L preserves the bracket, so it is an automorphism of L (TauCeti.intLieAlgebraLieEquiv);
• an automorphism φ of L conjugates exp (ad x) to exp (ad (φ x)), so Int L is normalized by every automorphism of L.

The Weyl automorphisms of sl₂ triples and Kostant's subgroup TauCeti.expAdSubgroup are placed inside Int L in the files defining them (IsSl2Triple.ofLinearEquiv_weylAut_mem_intLieAlgebra and TauCeti.map_expAdSubgroup_le_intLieAlgebra).

For a split semisimple Lie algebra over a field of characteristic zero, Int L is the group whose invariant polynomial functions on L Chevalley's restriction theorem describes: the conjugates of a Cartan subalgebra under Int L are dense in L, so such a function is determined by its restriction to the Cartan subalgebra.

Main definitions

• TauCeti.intLieAlgebra K L: the subgroup of LinearMap.GeneralLinearGroup K L generated by the automorphisms exp (ad x) with ad x nilpotent.
• TauCeti.intLieAlgebraLieEquiv: an element of Int L, as an automorphism of the Lie algebra.

Main results

• TauCeti.coe_ofLinearEquiv_expAd: the generator exp (ad x) of Int L is the exponential of ad x, as a linear map.
• TauCeti.intLieAlgebra_le_iff: the universal property of TauCeti.intLieAlgebra.
• TauCeti.map_lie_of_mem_intLieAlgebra: elements of Int L preserve the bracket.
• LieEquiv.map_conj_intLieAlgebra: conjugation by an automorphism of L maps Int L onto itself.

References

• J. Humphreys, Introduction to Lie Algebras and Representation Theory, §2.3, where Int L is introduced and shown to be normal in the automorphism group of L.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter VII, §3.1, where the same group is the group Aut_e(L) of elementary automorphisms.

def TauCeti.intLieAlgebra (K : Type u_1) (L : Type u_2) [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] : Subgroup (LinearMap.GeneralLinearGroup K L)

The group Int L of inner automorphisms of a Lie algebra L: the subgroup of the general linear group of L generated by the automorphisms exp (ad x) with ad x nilpotent. Its elements preserve the bracket (TauCeti.map_lie_of_mem_intLieAlgebra).

theorem TauCeti.ofLinearEquiv_expAd_mem_intLieAlgebra {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : LinearMap.GeneralLinearGroup.ofLinearEquiv (expAd x ⋯).toLinearEquiv ∈ intLieAlgebra K L

Each generator exp (ad x) lies in Int L.

theorem TauCeti.coe_ofLinearEquiv_expAd {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv (expAd x ⋯).toLinearEquiv) = IsNilpotent.exp ((LieAlgebra.ad K L) x)

The linear map underlying the generator exp (ad x) of Int L is the exponential of ad x.

theorem TauCeti.intLieAlgebra_le_iff {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {G : Subgroup (LinearMap.GeneralLinearGroup K L)} : intLieAlgebra K L ≤ G ↔ ∀ (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)), LinearMap.GeneralLinearGroup.ofLinearEquiv (expAd x ⋯).toLinearEquiv ∈ G

Int L lies in a subgroup G if and only if every generator exp (ad x) does.

Elements of Int L are Lie automorphisms

theorem TauCeti.map_lie_of_mem_intLieAlgebra {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] {g : LinearMap.GeneralLinearGroup K L} (hg : g ∈ intLieAlgebra K L) (x y : L) : g • ⁅x, y⁆ = ⁅g • x, g • y⁆

Elements of Int L preserve the bracket.

def TauCeti.intLieAlgebraLieEquiv {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (g : ↥(intLieAlgebra K L)) : L ≃ₗ⁅K⁆ L

An element of Int L, as an automorphism of the Lie algebra L.

@[simp]

theorem TauCeti.intLieAlgebraLieEquiv_apply {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (g : ↥(intLieAlgebra K L)) (x : L) : (intLieAlgebraLieEquiv g) x = ↑g • x

TauCeti.intLieAlgebraLieEquiv g acts as g does.

@[simp]

theorem TauCeti.intLieAlgebraLieEquiv_toLinearEquiv {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (g : ↥(intLieAlgebra K L)) : (intLieAlgebraLieEquiv g).toLinearEquiv = (↑g).toLinearEquiv

The underlying linear equivalence of TauCeti.intLieAlgebraLieEquiv g is that of g.

@[simp]

theorem TauCeti.intLieAlgebraLieEquiv_expAd {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (x : L) (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : intLieAlgebraLieEquiv ⟨LinearMap.GeneralLinearGroup.ofLinearEquiv (expAd x ⋯).toLinearEquiv, ⋯⟩ = expAd x ⋯

On a generator, TauCeti.intLieAlgebraLieEquiv is exp (ad x).

@[simp]

theorem TauCeti.intLieAlgebraLieEquiv_one {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] : intLieAlgebraLieEquiv 1 = LieEquiv.refl

The identity of Int L is the identity automorphism.

theorem TauCeti.intLieAlgebraLieEquiv_mul {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (g h : ↥(intLieAlgebra K L)) : intLieAlgebraLieEquiv (g * h) = (intLieAlgebraLieEquiv h).trans (intLieAlgebraLieEquiv g)

A product in Int L is the composite of the automorphisms, the right factor acting first.

@[simp]

theorem TauCeti.intLieAlgebraLieEquiv_inv {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (g : ↥(intLieAlgebra K L)) : intLieAlgebraLieEquiv g⁻¹ = (intLieAlgebraLieEquiv g).symm

An inverse in Int L is the inverse automorphism.

Normality

theorem LieEquiv.ofLinearEquiv_mul_ofLinearEquiv_expAd {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (φ : L ≃ₗ⁅K⁆ L) {x : L} (hx : IsNilpotent ((LieAlgebra.ad K L) x)) : LinearMap.GeneralLinearGroup.ofLinearEquiv φ.toLinearEquiv * LinearMap.GeneralLinearGroup.ofLinearEquiv (TauCeti.expAd x ⋯).toLinearEquiv = LinearMap.GeneralLinearGroup.ofLinearEquiv (TauCeti.expAd (φ x) ⋯).toLinearEquiv * LinearMap.GeneralLinearGroup.ofLinearEquiv φ.toLinearEquiv

An automorphism φ of L intertwines the generator exp (ad x) with the generator exp (ad (φ x)).

theorem LieEquiv.map_conj_intLieAlgebra {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (φ : L ≃ₗ⁅K⁆ L) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (LinearMap.GeneralLinearGroup.ofLinearEquiv φ.toLinearEquiv))) (TauCeti.intLieAlgebra K L) = TauCeti.intLieAlgebra K L

Int L is normalized by every automorphism of L: conjugation by an automorphism maps Int L onto itself.

theorem LieEquiv.conj_mem_intLieAlgebra_iff {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] [LieAlgebra ℚ L] (φ : L ≃ₗ⁅K⁆ L) {g : LinearMap.GeneralLinearGroup K L} : LinearMap.GeneralLinearGroup.ofLinearEquiv φ.toLinearEquiv * g * (LinearMap.GeneralLinearGroup.ofLinearEquiv φ.toLinearEquiv)⁻¹ ∈ TauCeti.intLieAlgebra K L ↔ g ∈ TauCeti.intLieAlgebra K L

Membership in Int L is invariant under conjugation by an automorphism of L.