Constructing Chevalley systems from a Lie-algebra basis

Let a Cartan-inverting automorphism act on a normalised root-vector system by ω (x α) = c α • x (-α). If -c α is a square, rescaling x α makes the action equal to the signed Chevalley involution. This file reduces that square condition to the simple roots via RootPairing.Base.induction_add.

For a LieAlgebra.Basis whose simple generators satisfy ω(eᵢ) = -fᵢ, write a normalised simple root vector as x αᵢ = aᵢ eᵢ. Its opposite is aᵢ⁻¹ fᵢ, so c αᵢ = -aᵢ². Thus the simple-root square condition holds automatically and a Chevalley system exists over the ground field.

Main results

• TauCeti.IsSl2System.isSquare_neg_of_forall_mem_base: square classes propagate from the simple roots to every root.
• TauCeti.IsSl2System.isSquare_neg_on_lieBasis_base: a basis exchanged by the automorphism gives the required square class at each simple root.
• TauCeti.IsSl2System.exists_isChevalleySystem_of_lieBasis: such a basis produces a Chevalley system over the ground field.
• TauCeti.IsChevalleySystem.simple_eq_or_eq_neg_of_lieBasis: a Chevalley system for the same involution agrees with the basis at each simple root up to one simultaneous sign.

References

• R. W. Carter, Simple Groups of Lie Type, §4.2.

theorem TauCeti.IsSl2System.isSquare_neg_of_forall_mem_base {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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (omega : L ≃ₗ⁅K⁆ L) (homega : ∀ y ∈ H, omega y = -y) (b : (LieAlgebra.IsKilling.rootSystem H).Base) (c : LieModule.Weight K (↥H) L → K) (hc : ∀ (alpha : LieModule.Weight K (↥H) L), alpha.IsNonZero → omega (x alpha) = c alpha • x (-alpha)) (hsimple : ∀ (i : ↥b.support), IsSquare (-c ↑↑i)) (alpha : LieModule.Weight K (↥H) L) (halpha : alpha.IsNonZero) : IsSquare (-c alpha)

If the negated scalars by which a Cartan-inverting automorphism exchanges root vectors are squares on the simple roots, then they are squares on every root.

theorem TauCeti.IsSl2System.exists_simple_lieBasis_coefficients {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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) {ι : Type u_1} [Fintype ι] (b : LieAlgebra.Basis ι H) (i : ↥b.base.support) : ∃ (a : K) (d : K), x ↑↑i = a • b.e (b.baseSupportEquiv.symm i) ∧ x (-↑↑i) = d • b.f (b.baseSupportEquiv.symm i) ∧ a * d = 1

At a simple root, a normalised root-vector system differs from the raising and lowering generators of a Lie-algebra basis by inverse scalars.

theorem TauCeti.IsSl2System.isSquare_neg_on_lieBasis_base {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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (omega : L ≃ₗ⁅K⁆ L) {ι : Type u_1} [Fintype ι] (b : LieAlgebra.Basis ι H) (i : ↥b.base.support) (he : omega (b.e (b.baseSupportEquiv.symm i)) = -b.f (b.baseSupportEquiv.symm i)) (c : LieModule.Weight K (↥H) L → K) (hc : ∀ (alpha : LieModule.Weight K (↥H) L), alpha.IsNonZero → omega (x alpha) = c alpha • x (-alpha)) : IsSquare (-c ↑↑i)

A Lie-algebra basis whose simple raising and lowering generators are exchanged with a minus sign supplies the simple-root square condition for any normalised root-vector system.

theorem TauCeti.IsSl2System.exists_isChevalleySystem_of_lieBasis {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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (omega : L ≃ₗ⁅K⁆ L) (homega : ∀ y ∈ H, omega y = -y) {ι : Type u_1} [Finite ι] (b : LieAlgebra.Basis ι H) (he : ∀ (i : ι), omega (b.e i) = -b.f i) : ∃ (y : LieModule.Weight K (↥H) L → L), IsChevalleySystem omega y

A basis exchanged by a Cartan-inverting automorphism produces a Chevalley system over the ground field. The simple-root calculation is propagated to all roots through b.base.

theorem TauCeti.IsChevalleySystem.simple_eq_or_eq_neg_of_lieBasis {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] {omega : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem omega x) {ι : Type u_1} [Fintype ι] (b : LieAlgebra.Basis ι H) (i : ↥b.base.support) (he : omega (b.e (b.baseSupportEquiv.symm i)) = -b.f (b.baseSupportEquiv.symm i)) : x ↑↑i = b.e (b.baseSupportEquiv.symm i) ∧ x (-↑↑i) = b.f (b.baseSupportEquiv.symm i) ∨ x ↑↑i = -b.e (b.baseSupportEquiv.symm i) ∧ x (-↑↑i) = -b.f (b.baseSupportEquiv.symm i)

At each simple root, a Chevalley system for the basis involution agrees with the basis raising and lowering generators up to one simultaneous sign.