Documentation

TauCeti.Algebra.Lie.Weights.Chevalley.Twist

Rescaling a normalised system against an automorphism inverting the Cartan subalgebra #

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, let H be a splitting Cartan subalgebra, and let ω be a Lie automorphism of L acting by -1 on H. Such an ω inverts every weight, so it carries the root space of α onto the root space of -α; since those spaces are lines, a normalised family x of root vectors is scaled by ω:

ω (x α) = c α • x (-α).

A Chevalley system is the special case c ≡ -1, which is what TauCeti.IsSl2System.isChevalleyNormalized_iff_exists_isChevalleySystem shows to be the same thing as having the Chevalley integers ±(p + 1) as structure constants. The family in hand need not satisfy c ≡ -1, and this file is about what has to be true for a rescaling of it to.

Two facts govern the scalars, and both are proved here.

They are almost multiplicative. Applying ω to ⁅x α, x β⁆ = N(α, β) • x γ for γ = α + β gives

c γ * N(α, β) = c α * c β * N(-α, -β),

and multiplying by N(α, β) turns the right-hand factor into the invariant N(α, β) N(-α, -β) = -(p + 1)² of TauCeti.IsSl2System.structureConstant_mul_structureConstant_neg_neg. So -c γ differs from (-c α) (-c β) by the square ((p + 1) / N(α, β))², and the integrality of N(α, β) is exactly the equation c γ = -(c α * c β). In particular the square class of -c α is multiplicative along root sums, which is the induction step of a reduction to the simple roots.

Square roots of them rescale the family. Rescaling x α to s α • x α preserves the normalisation exactly when s α * s (-α) = 1, and it multiplies c α by s α ^ 2. So c α can be moved to -1 precisely when -c α is a square, and choosing one root out of each opposite pair with TauCeti.exists_rootPairRepresentatives makes the rescaling factors used at α and -α inverse to each other. This is TauCeti.IsSl2System.exists_isChevalleySystem_of_forall_exists_sq.

Together these reduce the existence of a Chevalley system for a given ω to the statement that -c α is a square at every root, and make that statement multiplicative along root sums. Two things are deliberately left out. The automorphism ω is an input and is not produced here; and no induction over root heights is carried out, so the reduction of the square condition from all roots to a base is available as a step and is not taken. Carter builds a Chevalley basis by a different route, a sign recursion over the extraspecial pairs enumerated in TauCeti/LinearAlgebra/RootSystem/ExtraspecialPair.lean; going through an automorphism is the route Bourbaki's definition of a Chevalley system suggests, and it is the one available when the Chevalley involution is already visible on a presentation of L.

Main results #

References #

Roadmap #

Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md builds the split reductive group scheme over ℤ "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra", and TauCeti.IsChevalleySystem is that Chevalley basis. Everything downstream of it — TauCeti.IsChevalleySystem.chevalleyLieLattice, the adjoint admissible lattice, and the adjoint elementary Chevalley group — takes one as a hypothesis, so producing one is the open step. This file supplies the route through an automorphism inverting the Cartan subalgebra. Milestone L0 of TauCetiRoadmap/CFSGStatement/README.md is the downstream consumer of the assembled pinned group scheme.

The scalars by which the automorphism moves a normalised family #

source
theorem TauCeti.IsSl2System.ne_zero_of_map_eq_smul_neg {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) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) {c : K} (hc : ω (x α) = c • x (-α)) :
c ≠ 0

A scalar witnessing the action of the automorphism on a root vector is nonzero.

source
theorem TauCeti.IsSl2System.mul_eq_one_of_map_eq_smul_neg {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ω : ∀ y ∈ H, ω y = -y) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) {c d : K} (hc : ω (x α) = c • x (-α)) (hd : ω (x (-α)) = d • x α) :
c * d = 1

The scalars at α and -α are inverse to one another. This is the constraint the normalisation ⁅x α, x (-α)⁆ = α^∨ imposes on an opposite pair; the constraints coming from a root sum are recorded separately below.

source
theorem TauCeti.IsSl2System.structureConstant_eq_natCast_or_eq_neg_natCast_iff_of_map_eq_smul_neg {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) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) {a b c : K} (ha : ω (x α) = a • x (-α)) (hb : ω (x β) = b • x (-β)) (hc : ω (x γ) = c • x (-γ)) :
hx.structureConstant α β γ hγ hαβ = ↑(LieModule.chainBotCoeff (⇑α) β + 1) ∨ hx.structureConstant α β γ hγ hαβ = -↑(LieModule.chainBotCoeff (⇑α) β + 1) ↔ c = -(a * b)

Integrality of a structure constant is multiplicativity of the scalars. The structure constant at (α, β) is one of the Chevalley integers ±(p + 1) exactly when the scalar at γ = α + β is the negative of the product of the scalars at α and β.

Taking every scalar to be -1, which is what a Chevalley system does, makes the right-hand condition hold at every root sum; this is the mechanism behind TauCeti.IsSl2System.isChevalleyNormalized_iff_exists_isChevalleySystem.

source
theorem TauCeti.IsSl2System.neg_eq_mul_sq_of_map_eq_smul_neg {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) (e : L →ₗ⁅K⁆ L) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) {a b c : K} (ha : e (x α) = a • x (-α)) (hb : e (x β) = b • x (-β)) (hc : e (x γ) = c • x (-γ)) :
-c = -a * -b * (↑(LieModule.chainBotCoeff (⇑α) β + 1) / hx.structureConstant α β γ hγ hαβ) ^ 2

The square class of the negated scalar is multiplicative along a root sum. The correcting factor is the square of the ratio between the root-string coefficient and the structure constant.

source
theorem TauCeti.IsSl2System.isSquare_neg_of_map_eq_smul_neg {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) (e : L →ₗ⁅K⁆ L) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) {a b c : K} (ha : e (x α) = a • x (-α)) (hb : e (x β) = b • x (-β)) (hc : e (x γ) = c • x (-γ)) (hsa : IsSquare (-a)) (hsb : IsSquare (-b)) :
IsSquare (-c)

If the negated scalars at α and β are squares, so is the one at α + β. Iterating this along a decomposition of a positive root into simple roots would reduce the square condition of TauCeti.IsSl2System.exists_isChevalleySystem_of_forall_exists_sq to the simple roots; that induction is not carried out here.

Rescaling to a Chevalley system #

source
theorem TauCeti.IsSl2System.exists_sq_map_eq_smul_neg_of_isSquare {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] {x : LieModule.Weight K (↥H) L → L} {α : LieModule.Weight K (↥H) L} {c : K} (e : L → L) (hc : e (x α) = c • x (-α)) (hsq : IsSquare (-c)) :
∃ (t : K), e (x α) = -t ^ 2 • x (-α)

A square-class witness for the negated scalar can be rewritten as the square-root form used by the rescaling construction.

source
theorem TauCeti.IsSl2System.exists_isChevalleySystem_of_forall_exists_sq {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ω : ∀ y ∈ H, ω y = -y) {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (hsq : ∀ (α : LieModule.Weight K (↥H) L), α.IsNonZero → ∃ (t : K), ω (x α) = -t ^ 2 • x (-α)) :
∃ (y : LieModule.Weight K (↥H) L → L), IsChevalleySystem ω y

A normalised family rescales to a Chevalley system when the negated scalars are squares. Writing ω (x α) = c α • x (-α), the hypothesis is that -c α is a square at every root; the conclusion is a normalised family y with ω (y α) = -y (-α), that is, a Chevalley system for the given automorphism.

The constraint c α * c (-α) = 1 forces the chosen square roots to satisfy t α ^ 2 * t (-α) ^ 2 = 1. Choosing one root from each opposite pair with TauCeti.exists_rootPairRepresentatives then makes the rescaling factors used at α and -α inverse, which keeps the normalisation ⁅y α, y (-α)⁆ = α^∨ intact.