Documentation

TauCeti.Algebra.Lie.Weights.Chevalley.Involution

A Chevalley involution exists exactly when the structure constants are integral #

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, let H be a splitting Cartan subalgebra, and let x be a normalised family of root vectors, so ⁅x α, x (-α)⁆ = α∨. A Chevalley system asks in addition for a Lie automorphism ω with

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

TauCeti.IsChevalleySystem carries ω as data, and every construction consuming a Chevalley system therefore has to be handed one. This file removes that obligation: ω exists precisely when the structure constants of x are the Chevalley integers ±(p + 1), and it is then unique.

The equivalence rests on the rescaling invariant TauCeti.IsSl2System.structureConstant_mul_structureConstant_neg_neg, which says that N(α, β) N(-α, -β) = -(p + 1)² for every normalised family. Integrality of N(α, β) is thus the same condition as the sign symmetry N(-α, -β) = -N(α, β), and the sign symmetry is exactly what makes the linear map sending x α to -x (-α) and acting by -1 on H respect the bracket.

The map itself is assembled from the weight-space decomposition L = ⨁ χ, L χ: on L χ for a root χ it is v ↦ -(B(v, x (-χ)) / B(x χ, x (-χ))) • x (-χ), which sends x χ to -x (-χ), and on the zero weight space H it is -1. Since only its existence is asserted, the construction stays inside the proof.

Main definitions #

Main results #

References #

This advances the Chevalley-basis input to the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

source
def TauCeti.IsSl2System.IsChevalleyNormalized {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) :
Prop

A normalised family of root vectors is integrally normalised when every genuine root-sum structure constant is one of the Chevalley integers ±(p + 1), with p = chainBotCoeff α β.

Only root-sums of two roots are constrained: at a zero weight the family vanishes, so its structure constants are 0 and carry no information.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.IsSl2System.exists_isChevalleySystem {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) (hn : hx.IsChevalleyNormalized) :
    ∃ (ω : L ≃ₗ⁅K⁆ L), IsChevalleySystem ω x

    A Chevalley involution exists for an integrally normalised family. If every genuine root-sum structure constant of the normalised family x is ±(p + 1), then there is a Lie algebra automorphism exchanging each root vector with the negative of its opposite, so x is the root-vector family of a Chevalley system.

    The automorphism is built from the weight-space decomposition of L: it is -1 on the Cartan subalgebra, and on the root space of χ it sends v to -(B(v, x (-χ)) / B(x χ, x (-χ))) • x (-χ). Only its existence is asserted, since TauCeti.IsChevalleySystem.unique shows there is nothing to choose.

    source
    theorem TauCeti.IsChevalleySystem.isChevalleyNormalized {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 : IsChevalleySystem ω x) :
    ⋯.IsChevalleyNormalized

    A Chevalley system is integrally normalised: the compatibility with ω forces every genuine root-sum structure constant to be ±(p + 1).

    source
    theorem TauCeti.IsChevalleySystem.unique {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} {ω₁ ω₂ : L ≃ₗ⁅K⁆ L} (h₁ : IsChevalleySystem ω₁ x) (h₂ : IsChevalleySystem ω₂ x) :
    ω₁ = ω₂

    The Chevalley involution is unique. Two Lie automorphisms exchanging each root vector of the same normalised family with the negative of its opposite are equal: they agree on the root vectors by hypothesis and on the Cartan subalgebra because both negate the coroots, and those span L.

    source
    theorem TauCeti.IsSl2System.isChevalleyNormalized_iff_exists_isChevalleySystem {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) :
    hx.IsChevalleyNormalized ↔ ∃ (ω : L ≃ₗ⁅K⁆ L), IsChevalleySystem ω x

    Chevalley systems are the integrally normalised families. A normalised family of root vectors extends to a Chevalley system exactly when its genuine root-sum structure constants are the Chevalley integers ±(p + 1), and the extending automorphism is then unique.

    This turns the Chevalley involution from data that a consumer must supply into a property of the structure constants that a consumer can check.