The rational root system of a Dynkin type

TauCeti.DynkinType.simplyConnectedRootDatum pins one integral root datum per valid Dynkin type, on the lattices Fin t.rank → ℤ. The constructions which build a semisimple Lie algebra out of a root system want instead a root system over a field of characteristic zero: the roots must span the ambient space, which they do not in general over the simply connected character lattice, since that lattice is the weight lattice and the roots only span the root lattice inside it. The two lattices agree exactly when the Cartan matrix is unimodular, so integrally the roots do span for E₈, F₄ and G₂, and fail to span for every other valid type.

This file base-changes the pinned datum to ℚ, using TauCeti.rootPairingBaseChange, and proves that the result is a genuine root system: the roots span, because the t.rank simple roots are linearly independent in a space of dimension t.rank, and the coroots span, because they already did over ℤ. The pinned base and the Bourbaki-numbered Cartan matrix survive the base change unchanged, so the rational system realizes the same Dynkin type as the datum it comes from.

The rational system is also reduced and irreducible, which are the two remaining hypotheses of Geck's Chevalley basis RootPairing.GeckConstruction.basis. Reducedness holds already over ℤ, where it is a property of the explicit root tables, and transports by the general theorem TauCeti.isReduced_rootPairingBaseChange. Irreducibility is not available integrally and is instead deduced over ℚ from connectedness of the pinned Dynkin diagram.

Main definitions

• TauCeti.DynkinType.rationalRootSystem: the pinned datum of a valid Dynkin type, base-changed to ℚ.
• TauCeti.DynkinType.rationalBase: its Bourbaki-numbered base.
• TauCeti.DynkinType.simpleSupportEquiv: the Bourbaki numbering of the support of that base.

Main results

• TauCeti.DynkinType.instIsRootSystemRationalRootSystem: the roots and coroots span.
• TauCeti.DynkinType.hasCartanType_rationalRootSystem: the rational system realizes its own Dynkin type against the pinned numbering.
• TauCeti.DynkinType.pairingIn_rationalRootSystem: its Cartan integers are those of the datum.
• TauCeti.DynkinType.instIsReducedRationalRootSystem and TauCeti.DynkinType.instIsIrreducibleRationalRootSystem: the rational system is reduced and irreducible.
• TauCeti.DynkinType.cartanMatrix_rationalBase: read through the Bourbaki numbering, the Cartan matrix of the pinned base is the standard Cartan matrix of the Dynkin type.

References

The passage from a root datum over ℤ to the root system over ℚ it determines is standard; see N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1. This supplies the root-system input of the Chevalley basis in Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md, whose consumer is milestone L0 of the CFSGStatement roadmap.

The base change to ℚ

noncomputable def TauCeti.DynkinType.rationalRootSystem (t : DynkinType) (ht : t.Valid) : RootPairing (Fin t.numRoots) ℚ (Fin t.rank → ℚ) (Fin t.rank → ℚ)

The rational root system of a valid Dynkin type: the pinned simply connected root datum with its roots and coroots read in Fin t.rank → ℚ. The pairing is again the dot product, and the reflection permutation is unchanged.

Equations

• t.rationalRootSystem ht = TauCeti.rootPairingBaseChange ℚ (t.simplyConnectedRootDatum ht) ⋯

noncomputable def TauCeti.DynkinType.rationalBase (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).Base

The Bourbaki-numbered base of TauCeti.DynkinType.rationalRootSystem, supported on the same first t.rank root indices as the base of the integral datum.

Equations

• t.rationalBase ht = TauCeti.rootPairingBaseChangeBase ℚ (t.simplyConnectedRootDatum ht) ⋯ (t.simplyConnectedBase ht)

@[simp]

theorem TauCeti.DynkinType.root_rationalRootSystem (t : DynkinType) (ht : t.Valid) (i : Fin t.numRoots) (k : Fin t.rank) : (t.rationalRootSystem ht).root i k = ↑((t.simplyConnectedRootDatum ht).root i k)

theorem TauCeti.DynkinType.root_rationalRootSystem_eq_add_zsmul_iff (t : DynkinType) (ht : t.Valid) (α β γ : Fin t.numRoots) (n : ℤ) : (t.rationalRootSystem ht).root γ = (t.rationalRootSystem ht).root β + ↑n • (t.rationalRootSystem ht).root α ↔ (t.simplyConnectedRootDatum ht).root γ = (t.simplyConnectedRootDatum ht).root β + n • (t.simplyConnectedRootDatum ht).root α

Rational base change preserves and reflects integral root-string relations.

@[simp]

theorem TauCeti.DynkinType.coroot_rationalRootSystem (t : DynkinType) (ht : t.Valid) (i : Fin t.numRoots) (k : Fin t.rank) : (t.rationalRootSystem ht).coroot i k = ↑((t.simplyConnectedRootDatum ht).coroot i k)

@[simp]

theorem TauCeti.DynkinType.reflectionPerm_rationalRootSystem (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).reflectionPerm = (t.simplyConnectedRootDatum ht).reflectionPerm

@[simp]

theorem TauCeti.DynkinType.toLinearMap_rationalRootSystem (t : DynkinType) (ht : t.Valid) (x y : Fin t.rank → ℚ) : ((t.rationalRootSystem ht).toLinearMap x) y = x ⬝ᵥ y

The pairing of the rational system is the dot product of Fin t.rank → ℚ with itself.

@[simp]

theorem TauCeti.DynkinType.pairing_rationalRootSystem (t : DynkinType) (ht : t.Valid) (i j : Fin t.numRoots) : (t.rationalRootSystem ht).pairing i j = ↑(RootPairing.pairing (t.simplyConnectedRootDatum ht) i j)

@[simp]

theorem TauCeti.DynkinType.support_rationalBase (t : DynkinType) (ht : t.Valid) : (t.rationalBase ht).support = (t.simplyConnectedBase ht).support

instance TauCeti.DynkinType.instIsCrystallographicRationalRootSystem (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).IsCrystallographic

@[simp]

theorem TauCeti.DynkinType.chainBotCoeff_rationalRootSystem (t : DynkinType) (ht : t.Valid) (i j : Fin t.numRoots) : RootPairing.chainBotCoeff i j = RootPairing.chainBotCoeff i j

Extension to the rationals preserves descending root-string lengths.

@[simp]

theorem TauCeti.DynkinType.chainTopCoeff_rationalRootSystem (t : DynkinType) (ht : t.Valid) (i j : Fin t.numRoots) : RootPairing.chainTopCoeff i j = RootPairing.chainTopCoeff i j

Extension to the rationals preserves ascending root-string lengths.

@[simp]

theorem TauCeti.DynkinType.pairingIn_rationalRootSystem (t : DynkinType) (ht : t.Valid) (i j : Fin t.numRoots) : (t.rationalRootSystem ht).pairingIn ℤ i j = RootPairing.pairingIn (t.simplyConnectedRootDatum ht) ℤ i j

The Cartan integers of the rational system are those of the integral datum.

The rational system is a root system

theorem TauCeti.DynkinType.span_range_coroot_rationalRootSystem_eq_top (t : DynkinType) (ht : t.Valid) : Submodule.span ℚ (Set.range ⇑(t.rationalRootSystem ht).coroot) = ⊤

The coroots of the rational system span the rational cocharacter space, because the coroots of the simply connected datum already span the cocharacter lattice.

theorem TauCeti.DynkinType.span_range_root_rationalRootSystem_eq_top (t : DynkinType) (ht : t.Valid) : Submodule.span ℚ (Set.range ⇑(t.rationalRootSystem ht).root) = ⊤

The simple roots of the rational system are t.rank linearly independent vectors in a space of dimension t.rank, so the roots span the rational character space. This is the statement which fails integrally outside the unimodular types E₈, F₄ and G₂: over ℤ the roots span only the root lattice, which is a proper sublattice of the weight lattice whenever the Cartan matrix has determinant other than 1.

instance TauCeti.DynkinType.instIsRootSystemRationalRootSystem (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).IsRootSystem

The rational system is reduced and irreducible

instance TauCeti.DynkinType.instIsReducedRationalRootSystem (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).IsReduced

The rational system is reduced. This is reducedness of the pinned integral datum transported along the injective base change from ℤ to ℚ.

Acceptance: the rational system realizes its own Dynkin type

theorem TauCeti.DynkinType.hasCartanType_rationalRootSystem (t : DynkinType) (ht : t.Valid) : HasCartanType (t.rationalRootSystem ht) (t.rationalBase ht) t

The rational system has Cartan type t. The base change leaves both the support of the pinned base and every Cartan integer alone, so the relabelling exhibited by the integral datum still works.

instance TauCeti.DynkinType.instIsIrreducibleRationalRootSystem (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).IsIrreducible

The rational system is irreducible. The pinned Dynkin diagram of a valid type is connected, which over a field of characteristic zero forces irreducibility.

The Bourbaki numbering of the base support

theorem TauCeti.DynkinType.mem_support_rationalBase (t : DynkinType) (ht : t.Valid) {k : Fin t.numRoots} : k ∈ (t.rationalBase ht).support ↔ ↑k < t.rank

noncomputable def TauCeti.DynkinType.simpleSupportEquiv (t : DynkinType) (ht : t.Valid) : Fin t.rank ≃ ↥(t.rationalBase ht).support

The Bourbaki numbering of the pinned base. Bourbaki node i, at Fin index i - 1, is the element t.simpleIndex ht i of the support of TauCeti.DynkinType.rationalBase. Downstream constructions index simple roots by Fin t.rank and reach the support through this equivalence, so that no second numbering of the nodes is introduced.

Equations

• t.simpleSupportEquiv ht = (t.simpleSupportEquivSimplyConnectedBase ht).trans (TauCeti.supportEquivRootPairingBaseChangeBase ℚ (t.simplyConnectedRootDatum ht) ⋯ (t.simplyConnectedBase ht)).symm

@[simp]

theorem TauCeti.DynkinType.coe_simpleSupportEquiv (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : ↑((t.simpleSupportEquiv ht) i) = t.simpleIndex ht i

@[simp]

theorem TauCeti.DynkinType.cartanMatrix_rationalBase (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) : (t.rationalBase ht).cartanMatrix ((t.simpleSupportEquiv ht) i) ((t.simpleSupportEquiv ht) j) = t.cartanMatrix i j

The Cartan matrix of the pinned base is the standard Cartan matrix of the Dynkin type, read through the Bourbaki numbering. This is what lets a construction stated against RootPairing.Base.cartanMatrix be read off TauCeti.DynkinType.cartanMatrix.