Height and integral relations among roots

The height of a root relative to a base of a root pairing is the sum of the coefficients of its expansion in the simple roots. This file records that height respects every integral relation among the roots: a vanishing integral combination of roots has a vanishing combination of heights, so two integral combinations with the same value have the same combination of heights. When the roots span the weight space, it also extends height to the linear functional which sums the coordinates in the simple-root basis.

Main definitions

• Ado.heightLinearMap is the linear extension of root height to the weight space of a root system.

Main results

• Ado.apply_root_eq_height_zsmul says that an additive map taking the constant value c on the simple roots takes the value ht(α) • c on every root.
• Ado.sum_mul_height_eq_zero_of_sum_zsmul_root_eq_zero says that height respects integral relations among roots.
• Ado.sum_mul_height_eq_of_sum_zsmul_root_eq compares the heights of two integral combinations of roots with the same value.

References

This supports “Simple-root lowering” in Layer 1 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The argument follows Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6.

theorem Ado.apply_root_eq_height_zsmul {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] {A : Type y} [AddCommGroup A] (b : P.Base) (g : M →+ A) {c : A} (hg : ∀ j ∈ b.support, g (P.root j) = c) (i : ι) : g (P.root i) = b.height i • c

A map constant on the simple roots is the height acting on that constant. Expanding a root in the simple roots and applying the map termwise turns the value c on every simple root into the value ht(α) • c on every root. Only additivity is used, so the target is an arbitrary additive group.

noncomputable def Ado.heightLinearMap {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] (b : P.Base) : M →ₗ[R] R

The height functional on the weight space of a root system. A base of a root system is a basis of its weight space; summing the coordinates in that basis extends the integer-valued height of roots to an R-linear map on the whole weight space.

Equations

• Ado.heightLinearMap P b = b.toWeightBasis.sumCoords

theorem Ado.heightLinearMap_apply {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] (b : P.Base) (m : M) : (heightLinearMap P b) m = (b.toWeightBasis.repr m).sum fun (x : ↥b.support) => id

The height functional is the coordinate sum in the simple-root basis.

@[simp]

theorem Ado.heightLinearMap_simpleRoot {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] (b : P.Base) (i : ↥b.support) : (heightLinearMap P b) (P.root ↑i) = 1

The height functional sends every simple root to one.

@[simp]

theorem Ado.heightLinearMap_root {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsRootSystem] [CharZero R] (b : P.Base) (i : ι) : (heightLinearMap P b) (P.root i) = ↑(b.height i)

On a root, the height functional agrees with the integer-valued height of the root.

theorem Ado.sum_mul_height_eq_zero_of_sum_zsmul_root_eq_zero {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {s : Finset ι} {e : ι → ℤ} (he : ∑ i ∈ s, e i • P.root i = 0) : ∑ i ∈ s, e i * b.height i = 0

If an integral combination of roots vanishes, the same combination of their heights vanishes.

theorem Ado.sum_mul_height_eq_of_sum_zsmul_root_eq {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) {s t : Finset ι} {e f : ι → ℤ} (h : ∑ i ∈ s, e i • P.root i = ∑ i ∈ t, f i • P.root i) : ∑ i ∈ s, e i * b.height i = ∑ i ∈ t, f i * b.height i

Two integral combinations of roots with the same value have the same combination of heights.