Automorphisms normalising a Cartan subalgebra

Let σ be an automorphism of a Lie algebra L which normalises a nilpotent subalgebra H, in the sense that H.map σ = H. Then Mathlib's LieEquiv.ofSubalgebras restricts σ to an automorphism σ|H of H, and it carries the root space of χ : H → R onto the root space of χ ∘ (σ|H)⁻¹: root-space membership is the condition ∀ y, ∃ k, ((ad y - χ y) ^ k) z = 0, and it is transported by rewriting y as σ (σ⁻¹ y). So σ permutes the weights, and in the Killing setting it also transports the sl₂ data attached to a root, sending the coroot of α to the coroot of the permuted root and a normalised system of root vectors to a normalised system again.

This is the input the diagram automorphisms of a split semisimple Lie algebra need. A graph symmetry of the Dynkin diagram is realised on the Serre presentation as an automorphism permuting the Chevalley generators, hence normalising the Cartan subalgebra they span, and the Chevalley--Demazure construction has to know what it does to the remaining root vectors.

The Weyl automorphism TauCeti.weylAut of an sl₂ triple also permutes root spaces, by TauCeti.weylAut_map_rootSpace, which is proved directly from the exponential formula. This repository has no lemma H.map weylAut = H, so that statement is not currently derived from TauCeti.map_rootSpace_eq.

Main definitions

• TauCeti.weightPerm: the induced permutation of the weights of H acting on L.

Main results

• TauCeti.map_mem_rootSpace and TauCeti.map_rootSpace_eq: a normalising automorphism carries the root space of χ onto the root space of χ ∘ (σ|H)⁻¹.
• TauCeti.weightPerm_neg: the induced permutation commutes with negation of weights.
• TauCeti.weightPerm_eq_neg: an automorphism acting by -1 on H inverts every weight.
• TauCeti.map_coroot_weightPerm: a normalising automorphism sends the coroot of a root to the coroot of the permuted root.
• TauCeti.IsSl2System.map: the family obtained by transporting a normalised system of root vectors along a normalising automorphism is again a normalised system.
• TauCeti.IsSl2System.exists_map_eq_smul: a normalising automorphism scales each root vector, and TauCeti.IsSl2System.mul_eq_one_of_map_eq_smul: the scalars at α and -α are inverse.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §16.5.
• R. W. Carter, Simple Groups of Lie Type, §12.2.

This supplies part of the pinning data for the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which is consumed by milestones L0 and L1 of the CFSGStatement roadmap.

theorem TauCeti.map_mem_rootSpace {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : ↥H → R} {z : L} (hz : z ∈ LieAlgebra.rootSpace H χ) : σ z ∈ LieAlgebra.rootSpace H (χ ∘ ⇑(LieEquiv.ofSubalgebras H H σ hσ).symm)

A normalising automorphism carries the root space of χ into the root space of the weight χ ∘ (σ|H)⁻¹ obtained by precomposing with the inverse of its restriction.

theorem TauCeti.map_rootSpace_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (χ : ↥H → R) : Submodule.map ↑σ.toLinearEquiv ↑(LieAlgebra.rootSpace H χ) = ↑(LieAlgebra.rootSpace H (χ ∘ ⇑(LieEquiv.ofSubalgebras H H σ hσ).symm))

A normalising automorphism carries the root space of χ onto the root space of χ ∘ (σ|H)⁻¹: the inverse automorphism normalises H too, and transports the second root space back into the first.

def TauCeti.weightPerm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) : Equiv.Perm (LieModule.Weight R (↥H) L)

The permutation of the weights of H acting on L induced by an automorphism of L normalising H.

Equations

• TauCeti.weightPerm σ hσ = { toFun := TauCeti.weightMap✝ σ hσ, invFun := TauCeti.weightMap✝ σ.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.coe_weightPerm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (χ : LieModule.Weight R (↥H) L) : ⇑((weightPerm σ hσ) χ) = ⇑χ ∘ ⇑(LieEquiv.ofSubalgebras H H σ hσ).symm

@[simp]

theorem TauCeti.weightPerm_apply_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (χ : LieModule.Weight R (↥H) L) (y : ↥H) : ((weightPerm σ hσ) χ) y = χ ((LieEquiv.ofSubalgebras H H σ hσ).symm y)

theorem TauCeti.weightPerm_symm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) : Equiv.symm (weightPerm σ hσ) = weightPerm σ.symm ⋯

The inverse of the induced permutation is the permutation induced by the inverse automorphism.

@[simp]

theorem TauCeti.coe_weightPerm_symm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (χ : LieModule.Weight R (↥H) L) : ⇑((Equiv.symm (weightPerm σ hσ)) χ) = ⇑χ ∘ ⇑(LieEquiv.ofSubalgebras H H σ hσ)

The inverse of the induced permutation precomposes a weight with the restriction of σ itself.

@[simp]

theorem TauCeti.weightPerm_symm_apply_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (χ : LieModule.Weight R (↥H) L) (y : ↥H) : ((Equiv.symm (weightPerm σ hσ)) χ) y = χ ((LieEquiv.ofSubalgebras H H σ hσ) y)

theorem TauCeti.map_mem_rootSpace_weightPerm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : LieModule.Weight R (↥H) L} {z : L} (hz : z ∈ LieAlgebra.rootSpace H ⇑χ) : σ z ∈ LieAlgebra.rootSpace H ⇑((weightPerm σ hσ) χ)

A normalising automorphism carries the root space of a weight into the root space of its image under the induced permutation.

theorem TauCeti.map_mem_rootSpace_weightPerm_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : LieModule.Weight R (↥H) L} {z : L} : σ z ∈ LieAlgebra.rootSpace H ⇑((weightPerm σ hσ) χ) ↔ z ∈ LieAlgebra.rootSpace H ⇑χ

Membership of the image in the image root space detects membership in the original one, the inverse automorphism transporting it back.

@[simp]

theorem TauCeti.weightPerm_isZero_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : LieModule.Weight R (↥H) L} : ((weightPerm σ hσ) χ).IsZero ↔ χ.IsZero

A weight is zero exactly when its image under the induced permutation is.

@[simp]

theorem TauCeti.weightPerm_symm_isZero_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : LieModule.Weight R (↥H) L} : ((Equiv.symm (weightPerm σ hσ)) χ).IsZero ↔ χ.IsZero

A weight is zero exactly when its preimage under the induced permutation is.

theorem TauCeti.weightPerm_isNonZero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : LieModule.Weight R (↥H) L} (hχ : χ.IsNonZero) : ((weightPerm σ hσ) χ).IsNonZero

The induced permutation of the weights carries roots to roots.

theorem TauCeti.weightPerm_symm_isNonZero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] (σ : L ≃ₗ⁅R⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {χ : LieModule.Weight R (↥H) L} (hχ : χ.IsNonZero) : ((Equiv.symm (weightPerm σ hσ)) χ).IsNonZero

The inverse of the induced permutation of the weights carries roots to roots.

theorem TauCeti.weightPerm_eq_neg {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (ω : L ≃ₗ⁅K⁆ L) (hω : ∀ y ∈ H, ω y = -y) (α : LieModule.Weight K (↥H) L) : (weightPerm ω ⋯) α = -α

An automorphism acting by -1 on the Cartan subalgebra inverts every weight. The induced permutation of the weights is negation, so the automorphism carries the root space of α onto the root space of -α.

@[simp]

theorem TauCeti.weightPerm_neg {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (σ : L ≃ₗ⁅K⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (α : LieModule.Weight K (↥H) L) : (weightPerm σ hσ) (-α) = -(weightPerm σ hσ) α

The induced permutation of the weights commutes with negation, since precomposition with the restricted automorphism is linear in the weight.

@[simp]

theorem TauCeti.weightPerm_symm_neg {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (σ : L ≃ₗ⁅K⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) (α : LieModule.Weight K (↥H) L) : (Equiv.symm (weightPerm σ hσ)) (-α) = -(Equiv.symm (weightPerm σ hσ)) α

The inverse of the induced permutation of the weights also commutes with negation.

theorem TauCeti.map_coroot_weightPerm {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (σ : L ≃ₗ⁅K⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {α : LieModule.Weight K (↥H) L} : σ ↑(LieAlgebra.IsKilling.coroot α) = ↑(LieAlgebra.IsKilling.coroot ((weightPerm σ hσ) α))

A normalising automorphism sends the coroot of a root to the coroot of the permuted root.

theorem TauCeti.IsSl2System.map {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (σ : L ≃ₗ⁅K⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) : IsSl2System fun (α : LieModule.Weight K (↥H) L) => σ (x ((Equiv.symm (weightPerm σ hσ)) α))

Transporting a normalised family of root vectors along an automorphism normalising the Cartan subalgebra gives a normalised family again: the root vector at α is the image of the root vector at the preimage of α.

The normalisation survives because a normalising automorphism sends the coroot of a root to the coroot of the permuted root, by TauCeti.map_coroot_weightPerm.

theorem TauCeti.IsSl2System.exists_map_eq_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (σ : L ≃ₗ⁅K⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) : ∃ (c : K), c ≠ 0 ∧ σ (x α) = c • x ((weightPerm σ hσ) α)

A normalising automorphism scales each root vector: the image of x α is a nonzero multiple of the root vector at the permuted root, because the root spaces are lines.

theorem TauCeti.IsSl2System.mul_eq_one_of_map_eq_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (σ : L ≃ₗ⁅K⁆ L) (hσ : LieSubalgebra.map σ.toLieHom H = H) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) {c d : K} (hc : σ (x α) = c • x ((weightPerm σ hσ) α)) (hd : σ (x (-α)) = d • x (-(weightPerm σ hσ) α)) : c * d = 1

The scalars by which a normalising automorphism scales the root vectors at α and at -α are inverse to one another. This is the only constraint the normalisation imposes on them.