Reducedness of the pinned root data

The pinned simply connected root data of types A, D, E₆, E₇, and E₈ are reduced. Their character and cocharacter lattices use different preferred bases, so reducedness is not obtained by identifying each root with its coroot. Instead, their coordinate constructions all exhibit a symmetric root--coroot pairing. RootPairing.isReduced_of_pairing_comm then rules out nontrivial multiples among their roots.

These instances supply the reducedness hypothesis needed to apply Mathlib's Geck construction to the rational scalar extensions of the pinned data. The non-simply-laced cases are supplied by TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.NonSimplyLaced; the final theorem here joins the two cases uniformly.

Main results

• Reducedness results for DynkinType.typeASimplyConnectedRootDatum, typeDSimplyConnectedRootDatum, e6SimplyConnectedRootDatum, e7SimplyConnectedRootDatum, and e8SimplyConnectedRootDatum.
• DynkinType.isReduced_simplyConnectedRootDatum_of_isSimplyLaced: the uniform reducedness theorem for every valid simply-laced Dynkin type.
• DynkinType.isReduced_simplyConnectedRootDatum: the uniform reducedness theorem for every valid Dynkin type.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates I, IV--VII.
• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups.

instance TauCeti.DynkinType.isReduced_typeASimplyConnectedRootDatum (n : ℕ) : RootPairing.IsReduced (typeASimplyConnectedRootDatum n)

The pinned simply connected root datum of type A is reduced.

instance TauCeti.DynkinType.isReduced_typeDSimplyConnectedRootDatum (n : ℕ) (hn : 4 ≤ n) : RootPairing.IsReduced (typeDSimplyConnectedRootDatum n hn)

The pinned simply connected root datum of type D is reduced.

instance TauCeti.DynkinType.instIsReducedE6SimplyConnectedRootDatum : RootPairing.IsReduced e6SimplyConnectedRootDatum

The pinned simply connected root datum of type E₆ is reduced.

instance TauCeti.DynkinType.instIsReducedE7SimplyConnectedRootDatum : RootPairing.IsReduced e7SimplyConnectedRootDatum

The pinned simply connected root datum of type E₇ is reduced.

instance TauCeti.DynkinType.instIsReducedE8SimplyConnectedRootDatum : RootPairing.IsReduced e8SimplyConnectedRootDatum

The pinned simply connected root datum of type E₈ is reduced.

theorem TauCeti.DynkinType.isReduced_simplyConnectedRootDatum_of_isSimplyLaced (t : DynkinType) (ht : t.Valid) (hs : t.IsSimplyLaced) : RootPairing.IsReduced (t.simplyConnectedRootDatum ht)

The pinned simply connected root datum of every valid simply-laced Dynkin type is reduced.

theorem TauCeti.DynkinType.isReduced_simplyConnectedRootDatum (t : DynkinType) (ht : t.Valid) : RootPairing.IsReduced (t.simplyConnectedRootDatum ht)

The pinned integral datum is reduced, uniformly in the valid Dynkin type. The simply-laced and non-simply-laced halves are proved by different criteria, so this only joins them.