Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.SerrePresentation

The Serre presentation of the pinned split Lie algebra of a Dynkin type #

TauCeti.DynkinType.lieAlgebra is the concrete matrix Lie algebra that Geck's construction attaches to the pinned root datum of a valid Dynkin type, and TauCeti.DynkinType.lieBasis is its Chevalley generators numbered by Bourbaki node. Matrix.ToLieAlgebra ℚ t.cartanMatrixᵀ is the abstract Lie algebra presented by Serre's relations for the same numbered Cartan matrix. This file names the homomorphism between them, TauCeti.DynkinType.serreLift, and proves it surjective.

The two carriers are the two ways a Chevalley--Demazure construction can name its Lie algebra: the presentation carries the generators and relations that the Kostant ℤ-form is written against, while Geck's matrices carry the root system and the nilpotency of the raising generators. The named comparison map here specialises the universal map induced by a Lie algebra basis to the pinned Dynkin type, without invoking Classical.choose.

The matrix is transposed on the way. TauCeti.IsSerreSystem follows Serre's convention ⁅Hᵢ, Eⱼ⁆ = CMᵢⱼ Eⱼ, whereas LieAlgebra.Basis.lie_h_e reads ⁅hⱼ, eᵢ⁆ = Aᵢⱼ eᵢ, so the Cartan matrix presenting TauCeti.DynkinType.lieAlgebra is t.cartanMatrixᵀ. Since t.cartanMatrixᵀ i j is t.cartanMatrix j i definitionally, no reindexing of Fin t.rank is involved and the Bourbaki numbering is the same on both sides.

Two things the presentation does not know on its own are read off the comparison map. The pinned Serre generators are nonzero, and the Cartan generators are even linearly independent, because their images are; nothing in Serre's relations says so, and for a matrix that is not a Cartan matrix the presented algebra can collapse. And the Chevalley involution of the presentation, TauCeti.serreChevalleyInvolution, is carried to the concrete signed involution TauCeti.geckChevalleyInvolution of Geck's algebra.

No claim is made that TauCeti.DynkinType.serreLift is injective. That is Serre's theorem, and it is not needed by a construction that starts from the concrete algebra and only wants to write its generators and relations down.

Main definitions #

Main results #

References #

Roadmap #

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", and insists on constructions rather than existence theorems. TauCeti.serreKostantForm of TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/Serre.lean is that Kostant form, written against Matrix.ToLieAlgebra ℚ CM; this file pins CM to the numbered Cartan matrix of a Dynkin type and identifies the presented algebra's image with the concrete carrier TauCeti.DynkinType.lieAlgebra. Milestone L0 of TauCetiRoadmap/CFSGStatement/README.md is the downstream consumer, reaching a Dynkin type through TauCeti.ValidLieTypeIndex.dynkinType and TauCeti.ValidLieTypeIndex.dynkinType_valid.

The higher Serre relations come from TauCeti/Algebra/Lie/Presentation/Serre/Basis.lean, which proves them for any LieAlgebra.Basis on a Noetherian Lie algebra. The root-string form in TauCeti/Algebra/Lie/Presentation/Serre/Killing.lean does not apply here: the pinned algebra is built over ℚ, and Mathlib establishes a trivial radical for Geck's construction only over an algebraically closed field.

The presented algebra and the comparison map #

source
@[reducible, inline]
abbrev TauCeti.DynkinType.SerreLieAlgebra (t : DynkinType) :
Type

The Lie algebra presented by Serre's relations for a Dynkin type, for the pinned Cartan matrix in the Bourbaki numbering.

The matrix is transposed because TauCeti.IsSerreSystem follows Serre's convention ⁅Hᵢ, Eⱼ⁆ = CMᵢⱼ Eⱼ; see the module docstring. Validity of the type is not needed to write the presentation down, only to compare it with TauCeti.DynkinType.lieAlgebra.

Equations
Instances For
    source
    theorem TauCeti.DynkinType.isSerreSystem_lieBasis (t : DynkinType) (ht : t.Valid) :
    IsSerreSystem ℚ t.cartanMatrix.transpose (t.lieBasis ht).h (t.lieBasis ht).e (t.lieBasis ht).f

    The pinned Chevalley generators satisfy Serre's relations for the transposed pinned Cartan matrix.

    source
    noncomputable def TauCeti.DynkinType.serreLift (t : DynkinType) (ht : t.Valid) :
    t.SerreLieAlgebra →ₗ⁅ℚ⁆ ↥(t.lieAlgebra ht)

    The comparison map from the Serre presentation of a Dynkin type to its pinned split Lie algebra, sending each Serre generator to the Chevalley generator with the same Bourbaki number.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DynkinType.serreLift_serreH (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      (t.serreLift ht) (serreH ℚ t.cartanMatrix.transpose i) = (t.lieBasis ht).h i
      source
      @[simp]
      theorem TauCeti.DynkinType.serreLift_serreE (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      (t.serreLift ht) (serreE ℚ t.cartanMatrix.transpose i) = (t.lieBasis ht).e i
      source
      @[simp]
      theorem TauCeti.DynkinType.serreLift_serreF (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      (t.serreLift ht) (serreF ℚ t.cartanMatrix.transpose i) = (t.lieBasis ht).f i
      source
      theorem TauCeti.DynkinType.eq_serreLift (t : DynkinType) (ht : t.Valid) {g : t.SerreLieAlgebra →ₗ⁅ℚ⁆ ↥(t.lieAlgebra ht)} (hH : ∀ (i : Fin t.rank), g (serreH ℚ t.cartanMatrix.transpose i) = (t.lieBasis ht).h i) (hE : ∀ (i : Fin t.rank), g (serreE ℚ t.cartanMatrix.transpose i) = (t.lieBasis ht).e i) (hF : ∀ (i : Fin t.rank), g (serreF ℚ t.cartanMatrix.transpose i) = (t.lieBasis ht).f i) :
      g = t.serreLift ht

      The comparison map is the unique homomorphism sending the Serre generators to the pinned Chevalley generators.

      source
      theorem TauCeti.DynkinType.serreLift_surjective (t : DynkinType) (ht : t.Valid) :
      Function.Surjective ⇑(t.serreLift ht)

      The pinned split Lie algebra is a quotient of its Serre presentation. The raising and lowering generators generate it, which is what makes the comparison map surjective.

      The generators do not collapse #

      Serre's relations alone do not forbid a generator from being zero in the presented algebra: for a matrix that is not a Cartan matrix the presentation can degenerate. Here the concrete realization rules it out, since a generator with a nonzero image is nonzero.

      source
      theorem TauCeti.DynkinType.serreE_ne_zero (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      serreE ℚ t.cartanMatrix.transpose i ≠ 0

      The pinned Serre raising generators are nonzero.

      source
      theorem TauCeti.DynkinType.serreF_ne_zero (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      serreF ℚ t.cartanMatrix.transpose i ≠ 0

      The pinned Serre lowering generators are nonzero.

      source
      theorem TauCeti.DynkinType.linearIndependent_serreH (t : DynkinType) (ht : t.Valid) :
      LinearIndependent ℚ (serreH ℚ t.cartanMatrix.transpose)

      The pinned Serre Cartan generators are linearly independent, since the Cartan generators of a LieAlgebra.Basis are.

      source
      theorem TauCeti.DynkinType.serreH_ne_zero (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) :
      serreH ℚ t.cartanMatrix.transpose i ≠ 0

      The pinned Serre Cartan generators are nonzero.

      source
      theorem TauCeti.DynkinType.nontrivial_serreLieAlgebra (t : DynkinType) (ht : t.Valid) :
      Nontrivial t.SerreLieAlgebra

      The Serre presentation of a valid Dynkin type is nontrivial.

      source
      @[simp]
      theorem TauCeti.DynkinType.serreLift_serreChevalleyInvolution (t : DynkinType) (ht : t.Valid) (x : t.SerreLieAlgebra) :
      (t.serreLift ht) ((serreChevalleyInvolution ℚ t.cartanMatrix.transpose) x) = (t.chevalleyInvolution ht) ((t.serreLift ht) x)

      The comparison map intertwines the two Chevalley involutions: the signed exchange of the Serre generators is carried to the signed exchange of the pinned Chevalley generators.