The admissible lattice in the seven-dimensional representation of type G2

This file extends the integral seven-dimensional representation of the type-G₂ Serre presentation to the rational Serre algebra and proves that its coordinate ℤ-lattice is preserved by the Serre Kostant form. The raising and lowering matrices have integral entries and cube to zero; the two long-root generators square to zero, while each short-root generator squares to twice a single unit matrix, so its divided square is again an integral matrix. The Cartan matrices act diagonally through the weights TauCeti.G2ShortRoot.weight.

Thus the coordinate lattice is an admissible lattice for the explicit Serre-generator Kostant form. Its weights span the full type-G₂ character lattice by TauCeti.G2ShortRoot.span_range_weight_eq_top. These are the lattice inputs of the Kostant toral-closure construction for the short-root type-G₂ representation. That integral toral closure is not identified with the pinned simply connected group scheme of type G₂, and constructions on it transfer to that scheme only along such an identification.

Main declarations

• TauCeti.G2ShortRoot.rationalSerreRepresentation: the rational seven-dimensional representation.
• TauCeti.G2ShortRoot.rep: its extension to the universal enveloping algebra, acting through the rational matrix of its argument by TauCeti.G2ShortRoot.rep_ι_eq_toLinAlgEquiv'.
• TauCeti.G2ShortRoot.isSl2Triple_rep_serreRootGenerator: the represented Cartan, raising and lowering generators at each node form an sl₂ triple.
• TauCeti.G2ShortRoot.rootMatrix and TauCeti.G2ShortRoot.rootDividedSquareMatrix: the integral matrix of each numbered simple-root generator and of its divided square.
• TauCeti.G2ShortRoot.isNilpotent_rep_serreRootGenerator: the simple-root generators act nilpotently, with pow_three_rep_serreRootGenerator_eq_zero giving the cube.
• TauCeti.G2ShortRoot.lattice: the coordinate ℤ-lattice in the rational module.
• TauCeti.G2ShortRoot.rep_serreKostantForm_apply_mem_lattice: the Serre Kostant form preserves the lattice.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§22.3 and 26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• The formal organization follows TauCeti.Algebra.Lie.F4.ShortRoot.AdmissibleLattice and TauCeti.Algebra.Lie.E7.Minuscule.AdmissibleLattice.

Extension from the integral representation

noncomputable def TauCeti.G2ShortRoot.raisingMatrixRat (i : Fin 2) : Matrix (Fin 7) (Fin 7) ℚ

The rational raising matrix obtained from the integral representation.

Equations

• TauCeti.G2ShortRoot.raisingMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.G2ShortRoot.raisingMatrix i)

noncomputable def TauCeti.G2ShortRoot.loweringMatrixRat (i : Fin 2) : Matrix (Fin 7) (Fin 7) ℚ

The rational lowering matrix obtained from the integral representation.

Equations

• TauCeti.G2ShortRoot.loweringMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.G2ShortRoot.loweringMatrix i)

noncomputable def TauCeti.G2ShortRoot.cartanMatrixRat (i : Fin 2) : Matrix (Fin 7) (Fin 7) ℚ

The rational Cartan matrix obtained from the integral representation.

Equations

• TauCeti.G2ShortRoot.cartanMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.G2ShortRoot.cartanMatrix i)

@[simp]

theorem TauCeti.G2ShortRoot.raisingMatrixRat_apply (i : Fin 2) (a b : Fin 7) : raisingMatrixRat i a b = ↑(raisingMatrix i a b)

The entries of the rational raising matrix are the integral raising coefficients.

@[simp]

theorem TauCeti.G2ShortRoot.loweringMatrixRat_apply (i : Fin 2) (a b : Fin 7) : loweringMatrixRat i a b = ↑(loweringMatrix i a b)

The entries of the rational lowering matrix are the integral lowering coefficients.

@[simp]

theorem TauCeti.G2ShortRoot.cartanMatrixRat_apply (i : Fin 2) (a b : Fin 7) : cartanMatrixRat i a b = if a = b then ↑(weight a i) else 0

The rational Cartan matrix is diagonal with the weights on its diagonal.

theorem TauCeti.G2ShortRoot.isSerreSystemRat : IsSerreSystem ℚ CartanMatrix.G₂ cartanMatrixRat raisingMatrixRat loweringMatrixRat

The rational matrices satisfy the type-G₂ Serre relations.

theorem TauCeti.G2ShortRoot.isSl2TripleRat (i : Fin 2) : IsSl2Triple (cartanMatrixRat i) (raisingMatrixRat i) (loweringMatrixRat i)

At each simple node, the three rational matrices form an sl₂ triple.

noncomputable def TauCeti.G2ShortRoot.rationalSerreRepresentation : Matrix.ToLieAlgebra ℚ CartanMatrix.G₂ →ₗ⁅ℚ⁆ Matrix (Fin 7) (Fin 7) ℚ

The rational seven-dimensional representation of the type-G₂ Serre presentation.

Equations

• TauCeti.G2ShortRoot.rationalSerreRepresentation = TauCeti.serreLift TauCeti.G2ShortRoot.isSerreSystemRat

@[simp]

theorem TauCeti.G2ShortRoot.rationalSerreRepresentation_serreH (i : Fin 2) : rationalSerreRepresentation (serreH ℚ CartanMatrix.G₂ i) = cartanMatrixRat i

The rational Serre representation sends H_i to the rational Cartan matrix.

@[simp]

theorem TauCeti.G2ShortRoot.rationalSerreRepresentation_serreE (i : Fin 2) : rationalSerreRepresentation (serreE ℚ CartanMatrix.G₂ i) = raisingMatrixRat i

The rational Serre representation sends E_i to the rational raising matrix.

@[simp]

theorem TauCeti.G2ShortRoot.rationalSerreRepresentation_serreF (i : Fin 2) : rationalSerreRepresentation (serreF ℚ CartanMatrix.G₂ i) = loweringMatrixRat i

The rational Serre representation sends F_i to the rational lowering matrix.

The numbered root generators

def TauCeti.G2ShortRoot.rootMatrix : Fin 2 ⊕ Fin 2 → Matrix (Fin 7) (Fin 7) ℤ

The integral matrix of a numbered simple-root generator: a raising matrix at a positive index, a lowering matrix at a negative one.

Equations

• TauCeti.G2ShortRoot.rootMatrix (Sum.inl i) = TauCeti.G2ShortRoot.raisingMatrix i
• TauCeti.G2ShortRoot.rootMatrix (Sum.inr i) = TauCeti.G2ShortRoot.loweringMatrix i

def TauCeti.G2ShortRoot.rootDividedSquareMatrix : Fin 2 ⊕ Fin 2 → Matrix (Fin 7) (Fin 7) ℤ

The integral matrix of the divided square of a numbered simple-root generator: a single unit matrix for the two short-root generators, zero for the two long-root ones.

Equations

• TauCeti.G2ShortRoot.rootDividedSquareMatrix (Sum.inl i) = ![Matrix.single 2 4 1, 0] i
• TauCeti.G2ShortRoot.rootDividedSquareMatrix (Sum.inr i) = ![Matrix.single 4 2 1, 0] i

@[simp]

theorem TauCeti.G2ShortRoot.rootMatrix_inl (i : Fin 2) : rootMatrix (Sum.inl i) = raisingMatrix i

The integral matrix of a positive numbered root generator is the raising matrix.

@[simp]

theorem TauCeti.G2ShortRoot.rootMatrix_inr (i : Fin 2) : rootMatrix (Sum.inr i) = loweringMatrix i

The integral matrix of a negative numbered root generator is the lowering matrix.

@[simp]

theorem TauCeti.G2ShortRoot.rootDividedSquareMatrix_inl (i : Fin 2) : rootDividedSquareMatrix (Sum.inl i) = ![Matrix.single 2 4 1, 0] i

The divided square of a positive numbered root generator: a single unit matrix at the short-root index, zero at the long-root one.

@[simp]

theorem TauCeti.G2ShortRoot.rootDividedSquareMatrix_inr (i : Fin 2) : rootDividedSquareMatrix (Sum.inr i) = ![Matrix.single 4 2 1, 0] i

The divided square of a negative numbered root generator: a single unit matrix at the short-root index, zero at the long-root one.

theorem TauCeti.G2ShortRoot.rootMatrix_mul_self (k : Fin 2 ⊕ Fin 2) : rootMatrix k * rootMatrix k = 2 • rootDividedSquareMatrix k

Every numbered root generator squares to twice its divided square.

theorem TauCeti.G2ShortRoot.rootMatrix_pow_three (k : Fin 2 ⊕ Fin 2) : rootMatrix k ^ 3 = 0

Every numbered root generator cubes to zero.

theorem TauCeti.G2ShortRoot.rationalSerreRepresentation_serreRootGenerator (k : Fin 2 ⊕ Fin 2) : rationalSerreRepresentation (serreRootGenerator CartanMatrix.G₂ k) = (rootMatrix k).map ⇑(Int.castRingHom ℚ)

The rational Serre representation sends a numbered root generator to the cast of its integral matrix.

The enveloping-algebra representation

noncomputable def TauCeti.G2ShortRoot.rep : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CartanMatrix.G₂) →ₐ[ℚ] Module.End ℚ (Fin 7 → ℚ)

The rational representation extended to the universal enveloping algebra.

Equations

• TauCeti.G2ShortRoot.rep = (UniversalEnvelopingAlgebra.lift ℚ) ((↑Matrix.toLinAlgEquiv').toLieHom.comp TauCeti.G2ShortRoot.rationalSerreRepresentation)

theorem TauCeti.G2ShortRoot.rep_ι_apply (x : Matrix.ToLieAlgebra ℚ CartanMatrix.G₂) (v : Fin 7 → ℚ) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (rationalSerreRepresentation x).mulVec v

The enveloping-algebra inclusion acts by multiplying with the represented matrix.

theorem TauCeti.G2ShortRoot.rep_serreRootGenerator_apply (k : Fin 2 ⊕ Fin 2) (v : Fin 7 → ℚ) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k))) v = ((rootMatrix k).map ⇑(Int.castRingHom ℚ)).mulVec v

A numbered root generator acts by its integral matrix.

theorem TauCeti.G2ShortRoot.rep_ι_eq_toLinAlgEquiv' (x : Matrix.ToLieAlgebra ℚ CartanMatrix.G₂) : rep ((UniversalEnvelopingAlgebra.ι ℚ) x) = Matrix.toLinAlgEquiv' (rationalSerreRepresentation x)

A represented Lie-algebra element is the linear map of its rational matrix. Reading the operator this way transports identities between matrices to identities between operators.

theorem TauCeti.G2ShortRoot.rep_serreRootGenerator_eq_toLinAlgEquiv' (k : Fin 2 ⊕ Fin 2) : rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k)) = Matrix.toLinAlgEquiv' ((rootMatrix k).map ⇑(Int.castRingHom ℚ))

The represented simple-root generator is the linear map of its rational matrix, which transports the value of its square and the vanishing of its cube to the operator.

theorem TauCeti.G2ShortRoot.isSl2Triple_rep_serreRootGenerator (i : Fin 2) : IsSl2Triple (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ CartanMatrix.G₂ i))) (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ (Sum.inl i)))) (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ (Sum.inr i))))

The represented Cartan, positive and negative simple generators at a common type-G₂ node form an sl₂ triple.

theorem TauCeti.G2ShortRoot.dividedPower_two_rep_serreRootGenerator_apply (k : Fin 2 ⊕ Fin 2) (v : Fin 7 → ℚ) : (Associative.dividedPower 2 (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k)))) v = ((rootDividedSquareMatrix k).map ⇑(Int.castRingHom ℚ)).mulVec v

The divided square of a numbered root generator acts by the integral matrix of its divided square.

theorem TauCeti.G2ShortRoot.pow_three_rep_serreRootGenerator_eq_zero (k : Fin 2 ⊕ Fin 2) : rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k)) ^ 3 = 0

Every simple-root generator acts with cube zero.

theorem TauCeti.G2ShortRoot.isNilpotent_rep_serreRootGenerator (k : Fin 2 ⊕ Fin 2) : IsNilpotent (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k)))

Every represented simple-root generator is nilpotent, with nilpotence index at most three.

The admissible coordinate lattice

def TauCeti.G2ShortRoot.lattice : Submodule ℤ (Fin 7 → ℚ)

The coordinate ℤ-lattice in the rational module.

Equations

• TauCeti.G2ShortRoot.lattice = TauCeti.coordinateLattice (Fin 7)

@[simp]

theorem TauCeti.G2ShortRoot.mem_lattice_iff {v : Fin 7 → ℚ} : v ∈ lattice ↔ ∀ (a : Fin 7), ∃ (z : ℤ), ↑z = v a

A vector belongs to the lattice exactly when every coordinate is integral.

noncomputable def TauCeti.G2ShortRoot.latticeBasis : Module.Basis (Fin 7) ℤ ↥lattice

The coordinate basis of the lattice.

Equations

• TauCeti.G2ShortRoot.latticeBasis = TauCeti.coordinateLatticeBasis (Fin 7)

@[simp]

theorem TauCeti.G2ShortRoot.coe_latticeBasis (a : Fin 7) : ↑(latticeBasis a) = Pi.single a 1

Coercing a lattice basis vector to the rational module gives the corresponding coordinate vector.

theorem TauCeti.G2ShortRoot.rep_serreRootGenerator_apply_mem_lattice (k : Fin 2 ⊕ Fin 2) {v : Fin 7 → ℚ} (hv : v ∈ lattice) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k))) v ∈ lattice

Every simple-root generator preserves the coordinate lattice.

theorem TauCeti.G2ShortRoot.dividedPower_two_rep_serreRootGenerator_apply_mem_lattice (k : Fin 2 ⊕ Fin 2) {v : Fin 7 → ℚ} (hv : v ∈ lattice) : (Associative.dividedPower 2 (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.G₂ k)))) v ∈ lattice

The divided square of every simple-root generator preserves the coordinate lattice.

theorem TauCeti.G2ShortRoot.isCartanWeightVector_single (a : Fin 7) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ CartanMatrix.G₂) rep (weight a) (Pi.single a 1)

Each coordinate basis vector has the corresponding weight for the Cartan generators.

theorem TauCeti.G2ShortRoot.isCartanWeightVector_latticeBasis (a : Fin 7) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ CartanMatrix.G₂) rep (weight a) ↑(latticeBasis a)

Every lattice-basis vector is a Cartan weight vector with its weight.

theorem TauCeti.G2ShortRoot.rep_serreKostantForm_apply_mem_lattice {u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CartanMatrix.G₂)} (hu : u ∈ serreKostantForm CartanMatrix.G₂) {v : Fin 7 → ℚ} (hv : v ∈ lattice) : (rep u) v ∈ lattice

The coordinate lattice is admissible for the type-G₂ Serre Kostant form.