The pinned split Lie algebra of a Dynkin type

TauCeti.DynkinType.simplyConnectedRootDatum pins one integral root datum per valid Dynkin type, and TauCeti.DynkinType.rationalRootSystem reads it as a root system over ℚ. This file feeds that root system to Geck's construction and names the resulting Lie algebra: TauCeti.DynkinType.lieAlgebra is a Lie subalgebra of the square matrices indexed by one coordinate per element of the pinned base support and one per root, spanned by the explicit matrices Geck writes down from the root data. The base support is identified with the Bourbaki nodes below. No existence theorem is invoked: every element of the carrier traces back to the pinned root tables.

The two hypotheses Geck's construction needs beyond a root system, reducedness and irreducibility, are supplied by TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/Rational.lean, so what remains here is the numbering. Geck indexes his generators by the support of a base, which is a subtype of the root index type, whereas the conventions a consumer states — which node is long, which pair of nodes a diagram automorphism exchanges — are stated against Fin t.rank in the Bourbaki numbering. TauCeti.DynkinType.lieBasis is therefore Geck's basis renumbered along TauCeti.DynkinType.simpleSupportEquiv, and its Cartan matrix is then literally TauCeti.DynkinType.cartanMatrix, not a reindexed copy of it that would have to be compared with the pinned one.

Nothing is claimed here about the Lie algebra beyond the relations carried by a LieAlgebra.Basis. In particular it is not asserted to be semisimple: Mathlib derives that from Geck's construction over an algebraically closed field, and ℚ is not one. The Cartan subalgebra is a Cartan subalgebra, which is what the basis does give, and the one fact a Chevalley--Demazure construction consumes next that the basis does not already carry is recorded: the generators e and f are nilpotent as matrices. Their generation of the whole Lie algebra is exposed as TauCeti.DynkinType.lieSpan_lieBasis_e_union_f_eq_top.

Main definitions

• TauCeti.DynkinType.GeckIndex: the index set of the matrices, one coordinate per element of the pinned base support and one per root.
• TauCeti.DynkinType.geckDim: the number of Geck coordinates.
• TauCeti.DynkinType.lieAlgebra: the split Lie algebra of a valid Dynkin type.
• TauCeti.DynkinType.cartanSubalgebra: its distinguished Cartan subalgebra.
• TauCeti.DynkinType.lieBasis: its Chevalley generators, numbered by Bourbaki node.
• TauCeti.DynkinType.geckLieEquiv: the identification of the named carrier with Geck's, as an equivalence of Lie algebras.
• TauCeti.DynkinType.chevalleyInvolution: its signed Chevalley involution.

Main results

• TauCeti.DynkinType.lieBasis_A_eq: the Cartan matrix of the basis is the pinned Cartan matrix of the Dynkin type.
• TauCeti.DynkinType.geckDim_eq_rank_add_numRoots: the Geck dimension is the rank plus the number of roots.
• TauCeti.DynkinType.coe_lieBasis_h, coe_lieBasis_e, and coe_lieBasis_f: each generator is the explicit matrix Geck attaches to the corresponding simple root.
• TauCeti.DynkinType.lie_lieBasis_h_e and TauCeti.DynkinType.lie_lieBasis_h_f: the two relations that mention the Cartan matrix, read against the pinned numbering.
• TauCeti.DynkinType.lieSpan_lieBasis_e_union_f_eq_top: the raising and lowering generators span the pinned Lie algebra.
• TauCeti.DynkinType.isNilpotent_coe_lieBasis_e and TauCeti.DynkinType.isNilpotent_coe_lieBasis_f: the raising and lowering generators are nilpotent matrices.
• TauCeti.DynkinType.finrank_cartanSubalgebra: the Cartan subalgebra has dimension t.rank.
• TauCeti.DynkinType.geckLieEquiv_chevalleyInvolution: the involution is Geck's, read through that identification.
• TauCeti.DynkinType.chevalleyInvolution_lieBasis_h, TauCeti.DynkinType.chevalleyInvolution_lieBasis_e and TauCeti.DynkinType.chevalleyInvolution_lieBasis_f: the involution on the numbered generators.
• TauCeti.DynkinType.chevalleyInvolution_cartan: the involution acts by negation on the entire distinguished Cartan subalgebra.
• TauCeti.DynkinType.map_rootSpace_chevalleyInvolution: it exchanges the root spaces indexed by opposite Cartan functionals.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates I--IX, for the numbering.
• R. W. Carter, Simple Groups of Lie Type, §4.2, for the Chevalley basis of a split semisimple Lie algebra.

Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md asks for the split reductive group scheme over ℤ to be constructed "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra", from the root data DynkinType.simplyConnectedRootDatum of Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. This file supplies the Lie algebra and the numbered Chevalley generators that the Kostant ℤ-form of TauCeti/Algebra/Lie/ UniversalEnveloping/Kostant/ is formed from, whose consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

@[reducible, inline]

abbrev TauCeti.DynkinType.GeckIndex (t : DynkinType) (ht : t.Valid) : Type

The index set of the matrices realizing the pinned Lie algebra: one coordinate for each element of the pinned base support and one for each root of the pinned root system. The former is identified with the Bourbaki nodes by TauCeti.DynkinType.simpleSupportEquiv.

Equations

• t.GeckIndex ht = (↥(t.rationalBase ht).support ⊕ Fin t.numRoots)

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckDim (t : DynkinType) (ht : t.Valid) : ℕ

The number of Geck coordinates.

Equations

• t.geckDim ht = Fintype.card (t.GeckIndex ht)

theorem TauCeti.DynkinType.geckDim_eq_rank_add_numRoots (t : DynkinType) (ht : t.Valid) : t.geckDim ht = t.rank + t.numRoots

The number of Geck coordinates is the rank plus the number of roots.

noncomputable def TauCeti.DynkinType.lieAlgebra (t : DynkinType) (ht : t.Valid) : LieSubalgebra ℚ (Matrix (t.GeckIndex ht) (t.GeckIndex ht) ℚ)

The split Lie algebra of a valid Dynkin type. This is Geck's construction applied to the pinned rational root system: the Lie subalgebra of GeckIndex-indexed matrices generated by the explicit matrices RootPairing.GeckConstruction.h, e and f attached to the simple roots.

Equations

• t.lieAlgebra ht = RootPairing.GeckConstruction.lieAlgebra (t.rationalBase ht)

@[simp]

theorem TauCeti.DynkinType.lieAlgebra_def (t : DynkinType) (ht : t.Valid) : t.lieAlgebra ht = RootPairing.GeckConstruction.lieAlgebra (t.rationalBase ht)

The pinned Lie algebra is Geck's construction on the pinned rational base.

noncomputable def TauCeti.DynkinType.cartanSubalgebra (t : DynkinType) (ht : t.Valid) : LieSubalgebra ℚ ↥(t.lieAlgebra ht)

The distinguished Cartan subalgebra of TauCeti.DynkinType.lieAlgebra, spanned by the diagonal matrices attached to the simple coroots.

Equations

• t.cartanSubalgebra ht = RootPairing.GeckConstruction.cartanSubalgebra' (t.rationalBase ht)

@[simp]

theorem TauCeti.DynkinType.cartanSubalgebra_def (t : DynkinType) (ht : t.Valid) : t.cartanSubalgebra ht = LieSubalgebra.comap (t.lieAlgebra ht).incl (RootPairing.GeckConstruction.cartanSubalgebra (t.rationalBase ht))

The distinguished Cartan subalgebra is the one supplied by Geck's construction.

noncomputable def TauCeti.DynkinType.lieBasis (t : DynkinType) (ht : t.Valid) : LieAlgebra.Basis (Fin t.rank) (t.cartanSubalgebra ht)

The Chevalley generators of the pinned Lie algebra, numbered by Bourbaki node. This is Geck's basis, whose nodes are the support of the pinned base, renumbered along TauCeti.DynkinType.simpleSupportEquiv.

Equations

• t.lieBasis ht = (RootPairing.GeckConstruction.basis (t.rationalBase ht)).reindex (t.simpleSupportEquiv ht).symm

The generators as explicit matrices

@[simp]

theorem TauCeti.DynkinType.coe_lieBasis_h (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : ↑((t.lieBasis ht).h i) = RootPairing.GeckConstruction.h ((t.simpleSupportEquiv ht) i)

The Bourbaki-numbered Cartan generator is Geck's explicit diagonal matrix for the corresponding simple root.

@[simp]

theorem TauCeti.DynkinType.coe_lieBasis_e (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : ↑((t.lieBasis ht).e i) = RootPairing.GeckConstruction.e ((t.simpleSupportEquiv ht) i)

The Bourbaki-numbered raising generator is Geck's explicit matrix for the corresponding simple root.

@[simp]

theorem TauCeti.DynkinType.coe_lieBasis_f (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : ↑((t.lieBasis ht).f i) = RootPairing.GeckConstruction.f ((t.simpleSupportEquiv ht) i)

The Bourbaki-numbered lowering generator is Geck's explicit matrix for the corresponding simple root.

theorem TauCeti.DynkinType.lieSpan_lieBasis_e_union_f_eq_top (t : DynkinType) (ht : t.Valid) : LieSubalgebra.lieSpan ℚ (↥(t.lieAlgebra ht)) (Set.range (t.lieBasis ht).e ∪ Set.range (t.lieBasis ht).f) = ⊤

The Bourbaki-numbered raising and lowering generators span the pinned Lie algebra.

The pinned Cartan matrix and the relations

@[simp]

theorem TauCeti.DynkinType.lieBasis_A_eq (t : DynkinType) (ht : t.Valid) : (t.lieBasis ht).A = t.cartanMatrix

The Cartan matrix of the pinned Chevalley generators is the Cartan matrix of the Dynkin type, in the Bourbaki numbering.

@[simp]

theorem TauCeti.DynkinType.lie_lieBasis_h_e (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) : ⁅(t.lieBasis ht).h j, (t.lieBasis ht).e i⁆ = t.cartanMatrix i j • (t.lieBasis ht).e i

The action of a Cartan generator on a raising generator, against the pinned Cartan matrix.

@[simp]

theorem TauCeti.DynkinType.lie_lieBasis_h_f (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) : ⁅(t.lieBasis ht).h j, (t.lieBasis ht).f i⁆ = -t.cartanMatrix i j • (t.lieBasis ht).f i

The action of a Cartan generator on a lowering generator, against the pinned Cartan matrix.

Nilpotency

theorem TauCeti.DynkinType.isNilpotent_coe_lieBasis_e (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : IsNilpotent ↑((t.lieBasis ht).e i)

The explicit raising matrices are nilpotent.

theorem TauCeti.DynkinType.isNilpotent_coe_lieBasis_f (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : IsNilpotent ↑((t.lieBasis ht).f i)

The lowering generators are nilpotent matrices.

The Cartan subalgebra

instance TauCeti.DynkinType.instIsLieAbelianCartanSubalgebra (t : DynkinType) (ht : t.Valid) : IsLieAbelian ↥(t.cartanSubalgebra ht)

instance TauCeti.DynkinType.instIsCartanSubalgebraCartanSubalgebra (t : DynkinType) (ht : t.Valid) : (t.cartanSubalgebra ht).IsCartanSubalgebra

noncomputable def TauCeti.DynkinType.cartanBasis (t : DynkinType) (ht : t.Valid) : Module.Basis (Fin t.rank) ℚ ↥(t.cartanSubalgebra ht)

The Cartan generators are a basis of the Cartan subalgebra.

Equations

• t.cartanBasis ht = (t.lieBasis ht).cartanBasis

@[simp]

theorem TauCeti.DynkinType.coe_cartanBasis (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : ↑((t.cartanBasis ht) i) = (t.lieBasis ht).h i

The i-th vector of that basis is the i-th Cartan generator.

theorem TauCeti.DynkinType.finrank_cartanSubalgebra (t : DynkinType) (ht : t.Valid) : Module.finrank ℚ ↥(t.cartanSubalgebra ht) = t.rank

The Cartan subalgebra has dimension the rank of the Dynkin diagram.

The Chevalley involution

noncomputable def TauCeti.DynkinType.geckLieEquiv (t : DynkinType) (ht : t.Valid) : ↥(t.lieAlgebra ht) ≃ₗ⁅ℚ⁆ ↥(RootPairing.GeckConstruction.lieAlgebra (t.rationalBase ht))

The pinned Lie algebra and Geck's construction on the pinned rational base are the same subalgebra of matrices, TauCeti.DynkinType.lieAlgebra_def; this is that identification as an equivalence of Lie algebras. It carries Geck's automorphisms over to the named carrier without unfolding it.

Equations

• t.geckLieEquiv ht = LieEquiv.ofEq (t.lieAlgebra ht) (RootPairing.GeckConstruction.lieAlgebra (t.rationalBase ht)) ⋯

noncomputable def TauCeti.DynkinType.chevalleyInvolution (t : DynkinType) (ht : t.Valid) : ↥(t.lieAlgebra ht) ≃ₗ⁅ℚ⁆ ↥(t.lieAlgebra ht)

The Chevalley involution of the pinned split Lie algebra: the automorphism hᵢ ↦ -hᵢ, eᵢ ↦ -fᵢ, fᵢ ↦ -eᵢ of TauCeti.DynkinType.lieAlgebra. It is TauCeti.geckChevalleyInvolution of the pinned rational base, read against the Bourbaki numbering.

Equations

• t.chevalleyInvolution ht = ((t.geckLieEquiv ht).trans (TauCeti.geckChevalleyInvolution (t.rationalBase ht))).trans (t.geckLieEquiv ht).symm

@[simp]

theorem TauCeti.DynkinType.geckLieEquiv_chevalleyInvolution (t : DynkinType) (ht : t.Valid) (x : ↥(t.lieAlgebra ht)) : (t.geckLieEquiv ht) ((t.chevalleyInvolution ht) x) = (geckChevalleyInvolution (t.rationalBase ht)) ((t.geckLieEquiv ht) x)

The pinned Chevalley involution is Geck's involution, read through the identification of the two carriers.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_lieBasis_h (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.chevalleyInvolution ht) ((t.lieBasis ht).h i) = -(t.lieBasis ht).h i

The Chevalley involution negates each Cartan generator, hᵢ ↦ -hᵢ.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_lieBasis_e (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.chevalleyInvolution ht) ((t.lieBasis ht).e i) = -(t.lieBasis ht).f i

The Chevalley involution sends each raising generator to minus the lowering generator with the same Bourbaki number, eᵢ ↦ -fᵢ.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_lieBasis_f (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.chevalleyInvolution ht) ((t.lieBasis ht).f i) = -(t.lieBasis ht).e i

The Chevalley involution sends each lowering generator to minus the raising generator with the same Bourbaki number, fᵢ ↦ -eᵢ.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_symm (t : DynkinType) (ht : t.Valid) : (t.chevalleyInvolution ht).symm = t.chevalleyInvolution ht

The Chevalley involution of the pinned split Lie algebra is its own inverse.

Action on the Cartan subalgebra and weights

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_cartan (t : DynkinType) (ht : t.Valid) (x : ↥(t.cartanSubalgebra ht)) : (t.chevalleyInvolution ht) ↑x = -↑x

The pinned Chevalley involution acts by negation on the entire distinguished Cartan subalgebra. The numbered Cartan generators are a module basis, so their defining formula determines the restriction of the involution.

@[simp]

theorem TauCeti.DynkinType.map_chevalleyInvolution_cartanSubalgebra (t : DynkinType) (ht : t.Valid) : LieSubalgebra.map (t.chevalleyInvolution ht).toLieHom (LieSubalgebra.comap (t.lieAlgebra ht).incl (RootPairing.GeckConstruction.cartanSubalgebra (t.rationalBase ht))) = t.cartanSubalgebra ht

The pinned Chevalley involution normalizes the distinguished Cartan subalgebra. This is the hypothesis used to restrict it to the Cartan and to form its induced permutation of weights.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_ofSubalgebras_apply (t : DynkinType) (ht : t.Valid) (x : ↥(t.cartanSubalgebra ht)) : (LieEquiv.ofSubalgebras (t.cartanSubalgebra ht) (t.cartanSubalgebra ht) (t.chevalleyInvolution ht) ⋯) x = -x

Restricting the pinned Chevalley involution to the distinguished Cartan subalgebra gives pointwise negation.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_ofSubalgebras_symm_apply (t : DynkinType) (ht : t.Valid) (x : ↥(t.cartanSubalgebra ht)) : (LieEquiv.ofSubalgebras (t.cartanSubalgebra ht) (t.cartanSubalgebra ht) (t.chevalleyInvolution ht) ⋯).symm x = -x

The inverse of the restriction of the pinned Chevalley involution to the distinguished Cartan subalgebra is also pointwise negation.

@[simp]

theorem TauCeti.DynkinType.comp_chevalleyInvolution_ofSubalgebras_symm (t : DynkinType) (ht : t.Valid) (χ : Module.Dual ℚ ↥(t.cartanSubalgebra ht)) : ⇑χ ∘ ⇑(LieEquiv.ofSubalgebras (t.cartanSubalgebra ht) (t.cartanSubalgebra ht) (t.chevalleyInvolution ht) ⋯).symm = -⇑χ

Precomposing a Cartan functional with the inverse restriction of the pinned Chevalley involution negates that functional.

@[simp]

theorem TauCeti.DynkinType.map_rootSpace_chevalleyInvolution (t : DynkinType) (ht : t.Valid) (χ : Module.Dual ℚ ↥(t.cartanSubalgebra ht)) : Submodule.map ↑(t.chevalleyInvolution ht).toLinearEquiv ↑(LieAlgebra.rootSpace (t.cartanSubalgebra ht) ⇑χ) = ↑(LieAlgebra.rootSpace (t.cartanSubalgebra ht) (-⇑χ))

The pinned Chevalley involution exchanges opposite root spaces. For every Cartan functional χ, it carries the χ-root space onto the root space indexed by -χ.