The root system of the pinned rational Lie algebra

This file identifies the rational root system attached to a valid Dynkin type with the Killing root system of its pinned rational Geck Lie algebra. The identification is pinned: on simple roots it follows the common Bourbaki numbering supplied by Fin t.rank. Unlike RootPairing.GeckConstruction.equivRootSystem, which assumes an algebraically closed coefficient field, this construction works over ℚ by using the rational splitting and distinguished basis already established for the pinned Lie algebra.

Main declarations

• TauCeti.DynkinType.rationalRootSystemEquiv: the pinned equivalence from the rational root system to the Killing root system of the rational Lie algebra.

noncomputable def TauCeti.DynkinType.rationalRootSystemEquiv (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).Equiv (LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht))

The pinned rational root system is equivalent to the Killing root system of the pinned rational Lie algebra. The equivalence sends each rational simple root to the root attached to the correspondingly numbered generator of the distinguished Lie-algebra basis.

Equations

• t.rationalRootSystemEquiv ht = (t.rationalBase ht).equivOfCartanMatrixEq (t.lieBasis ht).base (TauCeti.DynkinType.rationalLieBaseSupportEquiv✝ t ht) ⋯

@[simp]

theorem TauCeti.DynkinType.rationalRootSystemEquiv_indexEquiv_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (↑(t.rationalRootSystemEquiv ht)).indexEquiv (t.simpleIndex ht i) = ↑((t.lieBasis ht).baseSupportEquiv i)

The pinned root-system equivalence sends a Bourbaki-numbered simple root to the simple root of the distinguished Lie-algebra basis with the same number.

@[simp]

theorem TauCeti.DynkinType.rationalRootSystemEquiv_weightMap_root_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (↑(t.rationalRootSystemEquiv ht)).weightMap ((t.rationalRootSystem ht).root (t.simpleIndex ht i)) = (LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht)).root ↑((t.lieBasis ht).baseSupportEquiv i)

On a Bourbaki-numbered simple root, the weight equivalence lands at the simple Killing root of the correspondingly numbered Lie-algebra generator.

@[simp]

theorem TauCeti.DynkinType.rationalRootSystemEquiv_coweightEquiv_symm_coroot_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.rationalRootSystemEquiv ht).coweightEquiv.symm ((t.rationalRootSystem ht).coroot (t.simpleIndex ht i)) = (LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht)).coroot ↑((t.lieBasis ht).baseSupportEquiv i)

On a Bourbaki-numbered simple coroot, the covariant inverse coweight equivalence lands at the simple Killing coroot of the correspondingly numbered Lie-algebra generator.