The coordinate lattice in the pinned Geck module

The pinned split Lie algebra TauCeti.DynkinType.lieAlgebra acts faithfully on the explicit Geck module TauCeti.DynkinType.GeckIndex → ℚ. This file equips that module with its coordinate ℤ-lattice, spanned by the standard coordinate vectors. It is finite free, has the expected coordinate basis, and spans the rational module.

The numbered Cartan, raising, and lowering generators preserve this lattice, and so do all of their generalized binomial coefficients and divided powers: the Cartan binomials because the coordinate vectors have the integral weights TauCeti.DynkinType.geckWeight, the root divided powers because every entry of TauCeti.Associative.dividedPower n of a raising or lowering matrix is an integer.

Consequently the entire simple-generator Kostant form preserves the lattice, and the integral orbit TauCeti.DynkinType.geckOrbit of the standard coordinate vectors coincides with it. In particular the orbit is finitely generated over ℤ, so it is a full lattice in the sense of Humphreys §27; no integral Poincaré--Birkhoff--Witt theorem is needed, since containment in the coordinate lattice reduces finite generation to Noetherianity of ℤ.

Main declarations

• TauCeti.DynkinType.geckCoordinateLattice: the coordinate ℤ-lattice in the Geck module.
• TauCeti.DynkinType.geckCoordinateBasis: its standard coordinate basis.
• TauCeti.DynkinType.geckCoordinateBasisFin: the same basis indexed by a finite ordinal, as required by the general-linear group-scheme construction.
• TauCeti.DynkinType.geckWeightFin: the coordinate weights in that finite-ordinal indexing.
• TauCeti.DynkinType.isCartanWeightVector_geckCoordinateBasisFin: every finite-ordinal basis vector is a Cartan weight vector.
• TauCeti.DynkinType.geckRepresentation_lieBasis_e_mem_geckCoordinateLattice and its lowering analogue: stability under the numbered root generators.
• TauCeti.DynkinType.geckRepresentation_ringChoose_lieBasis_h_mem_geckCoordinateLattice: stability under every Cartan binomial operator.
• TauCeti.DynkinType.geckRepresentation_dividedPower_rootGenerator_mem_geckCoordinateLattice: stability under every divided power of a numbered root generator.
• TauCeti.DynkinType.geckRepresentation_kostantForm_mem_geckCoordinateLattice: stability under the whole simple-generator Kostant form.
• TauCeti.DynkinType.geckOrbit_eq_geckCoordinateLattice: the integral orbit of the standard coordinate vectors is exactly the coordinate lattice.
• TauCeti.DynkinType.instIsLatticeGeckOrbit: the integral orbit is therefore a full lattice, finitely generated over ℤ.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

This advances the Chevalley--Demazure construction of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is the explicit pinned ambient group in milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

The coordinate lattice and its basis

def TauCeti.DynkinType.geckCoordinateLattice (t : DynkinType) (ht : t.Valid) : Submodule ℤ (t.GeckIndex ht → ℚ)

The coordinate ℤ-lattice in the pinned Geck module, spanned by the standard coordinate vectors.

Equations

• t.geckCoordinateLattice ht = TauCeti.coordinateLattice (t.GeckIndex ht)

@[simp]

theorem TauCeti.DynkinType.mem_geckCoordinateLattice_iff (t : DynkinType) (ht : t.Valid) {v : t.GeckIndex ht → ℚ} : v ∈ t.geckCoordinateLattice ht ↔ ∀ (i : t.GeckIndex ht), ∃ (z : ℤ), ↑z = v i

A vector belongs to the Geck coordinate lattice exactly when all its coordinates are integer-valued.

noncomputable def TauCeti.DynkinType.geckCoordinateBasis (t : DynkinType) (ht : t.Valid) : Module.Basis (t.GeckIndex ht) ℤ ↥(t.geckCoordinateLattice ht)

The standard coordinate basis of the Geck coordinate lattice.

Equations

• t.geckCoordinateBasis ht = TauCeti.coordinateLatticeBasis (t.GeckIndex ht)

@[simp]

theorem TauCeti.DynkinType.coe_geckCoordinateBasis (t : DynkinType) (ht : t.Valid) (i : t.GeckIndex ht) : ↑((t.geckCoordinateBasis ht) i) = Pi.single i 1

The underlying vector of a Geck coordinate basis element is the corresponding standard coordinate vector.

noncomputable def TauCeti.DynkinType.geckCoordinateBasisFin (t : DynkinType) (ht : t.Valid) : Module.Basis (Fin (t.geckDim ht)) ℤ ↥(t.geckCoordinateLattice ht).toAddSubgroup

The coordinate basis reindexed by a finite ordinal. This is the basis shape consumed by the Kostant generated-group-scheme construction.

The carrier subtype and ℤ-module structure of a submodule are definitionally equal to those of its underlying additive subgroup, so the reindexed submodule basis has the displayed target type.

Equations

• t.geckCoordinateBasisFin ht = (t.geckCoordinateBasis ht).reindex (Fintype.equivFin (t.GeckIndex ht))

@[simp]

theorem TauCeti.DynkinType.coe_geckCoordinateBasisFin (t : DynkinType) (ht : t.Valid) (i : Fin (t.geckDim ht)) : ↑((t.geckCoordinateBasisFin ht) i) = Pi.single ((Fintype.equivFin (t.GeckIndex ht)).symm i) 1

A finite-ordinal coordinate basis element is the standard vector at the corresponding Geck coordinate.

@[simp]

theorem TauCeti.DynkinType.intCast_geckCoordinateBasisFin_repr (t : DynkinType) (ht : t.Valid) (v : ↥(t.geckCoordinateLattice ht).toAddSubgroup) (i : Fin (t.geckDim ht)) : ↑(((t.geckCoordinateBasisFin ht).repr v) i) = ↑v ((Fintype.equivFin (t.GeckIndex ht)).symm i)

Reading a lattice vector in the finite-ordinal Geck basis recovers its corresponding standard coordinate after extending the integral coefficient to ℚ.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckWeightFin (t : DynkinType) (ht : t.Valid) : Fin (t.geckDim ht) → Fin t.rank → ℤ

The integral weight of a finite-ordinal Geck coordinate basis vector. The Cartan argument uses the Bourbaki numbering, while the coordinate argument uses the Fintype.equivFin ordering of GeckIndex.

Equations

• t.geckWeightFin ht i = t.geckWeight ht ((Fintype.equivFin (t.GeckIndex ht)).symm i)

theorem TauCeti.DynkinType.isCartanWeightVector_geckCoordinateBasisFin (t : DynkinType) (ht : t.Valid) (i : Fin (t.geckDim ht)) : UniversalEnvelopingAlgebra.IsCartanWeightVector (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckWeightFin ht i) ↑((t.geckCoordinateBasisFin ht) i)

Every finite-ordinal coordinate basis vector is a Cartan weight vector.

theorem TauCeti.DynkinType.geckCoordinateLattice_le_geckOrbit (t : DynkinType) (ht : t.Valid) : t.geckCoordinateLattice ht ≤ t.geckOrbit ht

The coordinate lattice is contained in the integral orbit of the pinned Kostant form, since the latter contains every standard coordinate vector.

instance TauCeti.DynkinType.instIsLatticeGeckCoordinateLattice (t : DynkinType) (ht : t.Valid) : Submodule.IsLattice ℚ (t.geckCoordinateLattice ht)

The coordinate lattice is finitely generated over ℤ and spans the ambient rational Geck module.

Stability under integral matrices

The numbered Chevalley generators

theorem TauCeti.DynkinType.geckRepresentation_lieBasis_e_mem_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) {v : t.GeckIndex ht → ℚ} (hv : v ∈ t.geckCoordinateLattice ht) : ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).e i))) v ∈ t.geckCoordinateLattice ht

A numbered raising generator preserves the Geck coordinate lattice.

theorem TauCeti.DynkinType.geckRepresentation_lieBasis_f_mem_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) {v : t.GeckIndex ht → ℚ} (hv : v ∈ t.geckCoordinateLattice ht) : ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).f i))) v ∈ t.geckCoordinateLattice ht

A numbered lowering generator preserves the Geck coordinate lattice.

theorem TauCeti.DynkinType.geckRepresentation_rootGenerator_mem_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) {v : t.GeckIndex ht → ℚ} (hv : v ∈ t.geckCoordinateLattice ht) : ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator i))) v ∈ t.geckCoordinateLattice ht

A numbered root generator, raising or lowering, preserves the Geck coordinate lattice.

Cartan binomial operators

theorem TauCeti.DynkinType.geckRepresentation_ringChoose_lieBasis_h_mem_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (n : ℕ) {v : t.GeckIndex ht → ℚ} (hv : v ∈ t.geckCoordinateLattice ht) : ((t.geckRepresentation ht) (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).h i)) n)) v ∈ t.geckCoordinateLattice ht

Every generalized binomial coefficient in a numbered Cartan generator preserves the Geck coordinate lattice.

Divided powers of the numbered root generators

theorem TauCeti.DynkinType.geckRepresentation_dividedPower_ι_apply (t : DynkinType) (ht : t.Valid) (x : ↥(t.lieAlgebra ht)) (n : ℕ) (v : t.GeckIndex ht → ℚ) : ((t.geckRepresentation ht) (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x))) v = (Associative.dividedPower n ↑x).mulVec v

The Geck representation sends the enveloping-algebra divided power of ι x to the matrix divided power of x, acting on v.

theorem TauCeti.DynkinType.geckRepresentation_dividedPower_rootGenerator_mem_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (n : ℕ) {v : t.GeckIndex ht → ℚ} (hv : v ∈ t.geckCoordinateLattice ht) : ((t.geckRepresentation ht) (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator i)))) v ∈ t.geckCoordinateLattice ht

Every divided power of a numbered root generator preserves the Geck coordinate lattice. This is the root-operator half of the statement that the whole Kostant form preserves the lattice; the Cartan half is TauCeti.DynkinType.geckRepresentation_ringChoose_lieBasis_h_mem_geckCoordinateLattice.

The Kostant form preserves the coordinate lattice

theorem TauCeti.DynkinType.geckRepresentation_kostantForm_mem_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) (u : UniversalEnvelopingAlgebra ℚ ↥(t.lieAlgebra ht)) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (t.lieBasis ht).rootGenerator (t.lieBasis ht).h) (v : t.GeckIndex ht → ℚ) (hv : v ∈ (t.geckCoordinateLattice ht).toAddSubgroup) : ((t.geckRepresentation ht) u) v ∈ (t.geckCoordinateLattice ht).toAddSubgroup

The Kostant form presented by the pinned generators preserves the Geck coordinate lattice. Every integral-form translate of a lattice vector stays in the lattice. Together with TauCeti.DynkinType.geckCoordinateLattice_le_geckOrbit this identifies the integral orbit of the standard coordinate vectors with the lattice itself.

theorem TauCeti.DynkinType.geckOrbit_le_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) : t.geckOrbit ht ≤ t.geckCoordinateLattice ht

The integral orbit of the standard coordinate vectors is contained in the coordinate lattice, because the Kostant form preserves the lattice and each coordinate vector lies in it.

@[simp]

theorem TauCeti.DynkinType.geckOrbit_eq_geckCoordinateLattice (t : DynkinType) (ht : t.Valid) : t.geckOrbit ht = t.geckCoordinateLattice ht

The integral orbit of the standard coordinate vectors is the coordinate lattice. The containment TauCeti.DynkinType.geckCoordinateLattice_le_geckOrbit holds because the identity of the enveloping algebra lies in the Kostant form; the reverse containment is the stability of the lattice under the form.

instance TauCeti.DynkinType.instIsLatticeGeckOrbit (t : DynkinType) (ht : t.Valid) : Submodule.IsLattice ℚ (t.geckOrbit ht)

The integral orbit of the standard coordinate vectors is a full lattice: finitely generated over ℤ and spanning the rational Geck module. This is the admissibility statement, in the sense of Humphreys §27, that the Chevalley--Demazure construction consumes; its finite generation needs no integral Poincaré--Birkhoff--Witt theorem, only containment in the finitely generated coordinate lattice.