Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.WeightDegree

The height degree of pinned integral weights #

The pinned rational root system of a valid Dynkin type has the simple roots as a basis of its weight space. Summing the coordinates in this basis gives a rational-valued degree on integral weights. This file packages that functional as TauCeti.DynkinType.weightDegree and identifies its value on the weights of Geck's defining representation.

On the coordinate indexed by a root alpha, TauCeti.DynkinType.geckWeight is the vector of Cartan pairings of alpha against the numbered simple coroots. In the pinned fundamental-weight coordinates this is the root itself. Its degree is therefore the height of alpha; in particular, it is positive on every positive root and sends each simple-root Cartan row to one. These are the facts needed to order a finite weight basis so that positive root subgroups act by upper unitriangular matrices, the triangular input to the Borel component of a pinning.

Main definitions #

Main results #

References #

This advances the pinning and Chevalley--Demazure construction targets in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Their pinned ambient group is consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

source
noncomputable def TauCeti.DynkinType.weightDegree (t : DynkinType) (ht : t.Valid) :
(Fin t.rank → ℤ) →+ ℚ

The simple-root height degree on integral weights of a valid Dynkin type. An integral weight is first read in the rational weight space, then evaluated by the linear extension of root height from the pinned simple-root basis.

Equations
Instances For
    source
    theorem TauCeti.DynkinType.weightDegree_apply (t : DynkinType) (ht : t.Valid) (μ : Fin t.rank → ℤ) :
    (t.weightDegree ht) μ = (heightLinearMap (t.rationalRootSystem ht) (t.rationalBase ht)) fun (i : Fin t.rank) => ↑(μ i)

    The weight degree is obtained by casting an integral weight to the rational weight space and applying the height functional there.

    source
    theorem TauCeti.DynkinType.intCast_geckWeight_inr (t : DynkinType) (ht : t.Valid) (k : Fin t.numRoots) :
    (fun (i : Fin t.rank) => ↑(t.geckWeight ht (Sum.inr k) i)) = (t.rationalRootSystem ht).root k

    The integral weight of a root coordinate in Geck's representation, cast to ℚ, is the corresponding root of the pinned rational root system.

    source
    @[simp]
    theorem TauCeti.DynkinType.weightDegree_geckWeight_inr (t : DynkinType) (ht : t.Valid) (k : Fin t.numRoots) :
    (t.weightDegree ht) (t.geckWeight ht (Sum.inr k)) = ↑((t.rationalBase ht).height k)

    The degree of a root coordinate in Geck's defining representation is the height of that root relative to the pinned base.

    source
    theorem TauCeti.DynkinType.weightDegree_geckWeight_inr_pos (t : DynkinType) (ht : t.Valid) {k : Fin t.numRoots} (hk : k ∈ posRoots (t.rationalRootSystem ht) (t.rationalBase ht)) :
    0 < (t.weightDegree ht) (t.geckWeight ht (Sum.inr k))

    A positive-root coordinate in Geck's defining representation has positive degree.

    source
    @[simp]
    theorem TauCeti.DynkinType.weightDegree_geckWeight_inl (t : DynkinType) (ht : t.Valid) (x : ↥(t.rationalBase ht).support) :
    (t.weightDegree ht) (t.geckWeight ht (Sum.inl x)) = 0

    A Cartan-support coordinate in Geck's defining representation has weight zero, hence degree zero.

    source
    @[simp]
    theorem TauCeti.DynkinType.weightDegree_cartanMatrix_row (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
    ((t.weightDegree ht) fun (j : Fin t.rank) => t.cartanMatrix i j) = 1

    Every simple-root Cartan row has degree one. This is the positive-degree input for each numbered raising generator of the pinned Lie algebra.

    source
    @[simp]
    theorem TauCeti.DynkinType.weightDegree_neg_cartanMatrix_row (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
    ((t.weightDegree ht) fun (j : Fin t.rank) => -t.cartanMatrix i j) = -1

    Every negative simple-root Cartan row has degree minus one.