Reducedness of the non-simply-laced pinned root data

The pinned simply connected root data of types B, C, F₄, and G₂ are reduced. For B, C, and F₄, the proof uses a criterion tailored to crystallographic root data over ℤ: if every Cartan integer has absolute value at most two, then two dependent roots have equal or opposite signs. Indeed, dependence forces the product of the two Cartan integers to be four, and the bound leaves only the pairs (2, 2) and (-2, -2). Type G₂ also has Cartan integers of absolute value three, so its small explicit coordinate table is checked directly instead.

For the classical families, the bound follows uniformly from their signed-coordinate models. For F₄, it is checked against the explicit coordinate table that defines its root datum. These instances provide the remaining reducedness hypotheses needed to apply Mathlib's Geck construction to the rational scalar extensions of the pinned data.

Main results

• DynkinType.instIsReducedTypeBSimplyConnectedRootDatum and DynkinType.instIsReducedTypeCSimplyConnectedRootDatum: reducedness in every rank.
• DynkinType.instIsReducedF4SimplyConnectedRootDatum and DynkinType.instIsReducedG2SimplyConnectedRootDatum: reducedness of the exceptional data.
• DynkinType.isReduced_simplyConnectedRootDatum_of_not_isSimplyLaced: the uniform theorem for every valid non-simply-laced Dynkin type.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates II, III, VIII, and IX.
• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups.

instance TauCeti.DynkinType.instIsReducedTypeBSimplyConnectedRootDatum (n : ℕ) : RootPairing.IsReduced (typeBSimplyConnectedRootDatum n)

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

instance TauCeti.DynkinType.instIsReducedTypeCSimplyConnectedRootDatum (n : ℕ) : RootPairing.IsReduced (typeCSimplyConnectedRootDatum n)

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

instance TauCeti.DynkinType.instIsReducedF4SimplyConnectedRootDatum : RootPairing.IsReduced f4SimplyConnectedRootDatum

The pinned simply connected root datum of type F₄ is reduced.

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

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