The Killing form of the pinned Dynkin-type Lie algebra

For a valid Dynkin type t, TauCeti.DynkinType.lieAlgebra t ht is the explicit rational matrix Lie algebra obtained by applying Geck's construction to TauCeti.DynkinType.simplyConnectedRootDatum t ht. This file proves that its Killing form is nondegenerate.

Mathlib proves that Geck's Lie algebra has trivial solvable radical over an algebraically closed field, hence has nondegenerate Killing form in characteristic zero. The rational carrier itself does not satisfy the algebraic-closure hypothesis. We therefore extend scalars to AlgebraicClosure ℚ, identify that scalar extension with Geck's construction over the extended root system via TauCeti.DynkinType.lieAlgebraBaseChangeEquiv, and descend nondegeneracy along ℚ → AlgebraicClosure ℚ using TauCeti.isKilling_of_isKilling_baseChange.

The result is installed as an instance because the root-space and Chevalley-system APIs take LieAlgebra.IsKilling as a typeclass assumption. The final instance transports it to TauCeti.DynkinType.lieAlgebraBaseChange t ht K over every integral domain carrying a rational algebra structure; algebraic closedness is needed only once, in the descent argument over ℚ.

Main declarations

• TauCeti.DynkinType.instIsKillingLieAlgebra: the rational pinned Dynkin-type Lie algebra has nondegenerate Killing form.
• TauCeti.DynkinType.instIsKillingLieAlgebraBaseChange: its explicit Geck realization after extension to any rational integral domain also has nondegenerate Killing form.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247, Lemma 4.3.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §5.1.

instance TauCeti.DynkinType.instIsKillingLieAlgebra (t : DynkinType) (ht : t.Valid) : LieAlgebra.IsKilling ℚ ↥(t.lieAlgebra ht)

The pinned rational Lie algebra of a valid Dynkin type has nondegenerate Killing form.

instance TauCeti.DynkinType.instIsKillingLieAlgebraBaseChange (t : DynkinType) (ht : t.Valid) (K : Type u_1) [CommRing K] [IsDomain K] [Algebra ℚ K] : LieAlgebra.IsKilling K ↥(t.lieAlgebraBaseChange ht K)

Every characteristic-zero scalar extension of the pinned Dynkin-type Lie algebra has nondegenerate Killing form. This is stated for the explicit Geck realization over K, rather than for the tensor product, using TauCeti.DynkinType.lieAlgebraBaseChangeEquiv.