The integral weight lattice and the coroot pairings of a weight #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of
characteristic zero and let H be a splitting Cartan subalgebra. A linear form
lam : Module.Dual K H is integral when lam (α^∨) is an integer for every root α
(TauCeti.IsIntegralWeight). This file records the two structures that condition carries: the
integer ⟨lam, αᵢ^∨⟩ itself, and the integral weight lattice of all integral weights.
The point of naming the integer is that K carries no order. Statements such as "lam is
dominant" or "⟨lam + ρ, α^∨⟩ is positive" are not about K at all: they are about the integers
that integrality produces, and over an arbitrary characteristic-zero field they can only be made
by naming those integers. TauCeti.coweightPairing lam i is that name. Being ℤ-valued it is
total in lam: it is the integer that lam (αᵢ^∨) names whenever that one value is an integer,
and it is unconstrained only at the roots where that value is not. Integrality is what guarantees
this at every root at once, so the cast equation TauCeti.intCast_coweightPairing saying what the
integer is -- a statement about all of lam -- and the algebraic laws that follow from it carry
the integrality hypothesis. What needs no hypothesis is a single coroot value already displayed as
an integer -- exhibiting that integer is integrality at that root -- and that is how the pairing
is computed here (TauCeti.coweightPairing_eq_of_apply_coroot_eq_intCast).
The integral weights are closed under the operations of TauCeti.IsIntegralWeight.add,
TauCeti.IsIntegralWeight.neg and TauCeti.IsIntegralWeight.zsmul, so they form a ℤ-submodule
TauCeti.integralWeightLattice of Module.Dual K H -- a lattice and not a K-subspace, the
integrality condition being arithmetic rather than linear. The roots lie in it; that the Weyl
vector ρ of a base does too is proved with the rest of the dominance theory, in
TauCeti/Algebra/Lie/HighestWeight/Weight/Lattice.lean.
Main definitions #
TauCeti.coweightPairing lam i: the integer⟨lam, αᵢ^∨⟩pairing a weight with the coroot of the rooti; the value oflamon that coroot whenever that value is an integer -- so at every root whenlamis integral -- and unconstrained where it is not.TauCeti.integralWeightLattice H: the integral weights, as aℤ-submodule ofModule.Dual K H.
Main results #
TauCeti.intCast_coweightPairing: the defining property,(⟨lam, αᵢ^∨⟩ : K) = lam (αᵢ^∨)for an integral weightlam. Together withTauCeti.coweightPairing_eq_iffit pins the pairing down,Khaving characteristic zero.TauCeti.coweightPairing_add,TauCeti.coweightPairing_neg,TauCeti.coweightPairing_subandTauCeti.coweightPairing_zsmul: the pairing is additive in an integral weight.TauCeti.coweightPairing_root_eq_pairingIn: at a root the pairing is the Cartan integer, in Mathlib's crystallographic root-pairing spelling.TauCeti.root_mem_integralWeightLattice: the roots are integral weights.
Implementation notes #
TauCeti.coweightPairing is the inverse image of lam (αᵢ^∨) under the integer cast, taken with
Function.invFun; the cast is injective in characteristic zero, so wherever that value is an
integer -- in particular at every root of an integral weight -- this is the unique integer with the
right image, and no further choice is made.
TauCeti.rootCartanWeight of TauCeti/Algebra/Lie/Weights/Root/CorootSpan.lean is the same
integer for a root in the first argument, where the root-chain coefficients compute it outright.
Neither subsumes the other: the Cartan integers of TauCeti.rootCartanWeight are available with no
hypothesis, while the pairing here accepts the weight of a module, a sum lam + ρ, or any other
integral weight, which is what the dominance and dimension statements pair against a coroot. The
lemma identifying the two, TauCeti.coweightPairing_toLinear_eq_rootCartanWeight, is stated beside
TauCeti.rootCartanWeight, so that nothing here depends on the root-chain theory.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §13.2.
The coroot pairings of a weight #
The coroot pairing ⟨lam, αᵢ^∨⟩ of a weight, as an integer. Whenever lam (αᵢ^∨) lies in
the image of ℤ this is the unique integer mapping to it
(TauCeti.coweightPairing_eq_of_apply_coroot_eq_intCast), which for an integral weight lam is the
case at every root (TauCeti.intCast_coweightPairing); at a root where lam (αᵢ^∨) is not an
integer the value is unconstrained.
Making the pairing ℤ-valued is what lets dominance and positivity be stated over a field with no
order: see the module docstring.
Equations
- TauCeti.coweightPairing lam i = Function.invFun Int.cast (lam ((LieAlgebra.IsKilling.rootSystem H).coroot i))
Instances For
An integer value of lam on a coroot is its coroot pairing. This is the only way the
pairing is ever computed, and it needs no integrality hypothesis: exhibiting the integer is
integrality at that root.
The defining property of the coroot pairing: on an integral weight it casts back to the value of the weight on the coroot.
The coroot pairing is characterized by its cast. Characteristic zero makes the integer
unique, so this is the equation to reason with when the value is known in K.
The zero weight pairs to zero.
The coroot pairing is additive in the weight.
The coroot pairing negates with the weight.
The coroot pairing subtracts with the weight.
The coroot pairing commutes with integer scaling of the weight.
At a root the coroot pairing is the Cartan integer, in the spelling of Mathlib's
crystallographic root-pairing API: the root system of a splitting Cartan subalgebra is valued in
ℤ, and RootPairing.pairingIn names the same integers this file names for a general weight.
The integral weight lattice #
The integral weight lattice X: the integral weights, as a ℤ-submodule of
Module.Dual K H.
It is a lattice and not a K-subspace: integrality asks a value to be an integer, which is an
arithmetic condition and is destroyed by scaling by a general element of K.
Equations
- TauCeti.integralWeightLattice H = { carrier := {lam : Module.Dual K ↥H | TauCeti.IsIntegralWeight lam}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
Membership in the integral weight lattice is integrality.
The roots lie in the integral weight lattice. A root is a weight of the adjoint module, so its coroot pairings are the Cartan integers.