The integral toral closure of the short-root type-G2 representation

This file feeds the explicit seven-dimensional representation of type G₂, its admissible coordinate lattice, and its weights, the six short roots and zero, into the Kostant toral-closure construction. The result is an affine group scheme over ℤ, explicitly cut out inside GL₇ by the largest Hopf ideal killed by all represented simple-root and weight-torus coordinate maps. Because the short roots generate the root lattice of G₂, which is its weight lattice, the weights of this module span the full character lattice, and the weight torus is a closed rank-two split torus in the integral toral closure.

The construction exposes the positive and negative numbered simple root subgroups, the closed weight torus, matrix-valued points over every commutative ring, and the scheme-level pinning equation. The two short-root generators are cube-zero and their subgroup matrices are quadratic, x(t) = 1 + t X + t² Y; the two long-root subgroup matrices are linear. Every ingredient is explicit data from TauCeti.Algebra.Lie.G2.ShortRoot.AdmissibleLattice; no group scheme is selected from an existence theorem.

Nothing here asserts reductivity, identifies the root datum of the integral toral closure, or constructs root subgroups for nonsimple roots. In particular this construction 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. It is also distinct from the designated characteristic-three carrier generated over the prime field; no identification with a base change of this integral toral closure is claimed.

Main definitions

• TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme: the short-root integral toral closure in GL₇.
• TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroup: its four numbered simple root subgroups.
• TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus: its rank-two split weight torus.
• TauCeti.G2ShortRoot.IntegralToralClosure.points: its matrix-valued points over a commutative ring.

Main results

• TauCeti.G2ShortRoot.IntegralToralClosure.isClosedImmersion_rootSubgroup: each numbered root subgroup is a closed copy of the additive group.
• TauCeti.G2ShortRoot.IntegralToralClosure.isClosedImmersion_weightTorus: the weights make the split torus a closed subgroup of the integral toral closure.
• TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints: the numbered simple-root matrices 1 + t X + t² Y in the weight basis, written out one index at a time in TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints_inl_zero and its three siblings.
• TauCeti.G2ShortRoot.IntegralToralClosure.coe_weightTorusPoints_eq_diagonal: a point of the split weight torus is the diagonal matrix of the weight characters at that point.
• TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus_conj_rootSubgroup: the scheme-level pinning equation.
• TauCeti.G2ShortRoot.IntegralToralClosure.weightTorusPoints_conj_rootSubgroupPoints: the same equation on matrix-valued points.

References

The Kostant toral-closure construction is motivated by the Chevalley--Demazure construction on the seven-dimensional module; see J. E. Humphreys, Linear Algebraic Groups, §26, and R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1. The representation and weight conventions follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX, and J. C. Jantzen, Representations of Algebraic Groups, II.2. The formal carrier interface follows TauCeti.Algebra.Lie.F4.ShortRoot.Carrier and TauCeti.Algebra.Lie.E7.Minuscule.Carrier.

theorem TauCeti.G2ShortRoot.rep_kostantForm_mem_lattice (u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CartanMatrix.G₂)) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂)) (v : Fin 7 → ℚ) (hv : v ∈ lattice.toAddSubgroup) : (rep u) v ∈ lattice.toAddSubgroup

The coordinate lattice is stable under the generic Kostant form generated by the Serre generators. This is the form required by the toral-closure construction.

Root characters and the unit root steps

theorem TauCeti.G2ShortRoot.lie_cartanGenerator_rootGenerator (k : Fin 2 ⊕ Fin 2) (j : Fin 2) : ⁅serreH ℚ CartanMatrix.G₂ j, serreRootGenerator CartanMatrix.G₂ k⁆ = ↑(DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2 k j) • serreRootGenerator CartanMatrix.G₂ k

The Cartan generators act on the numbered simple root generators through their root characters: the character of the i-th raising generator is the i-th row of the Bourbaki Cartan matrix of type G₂, and that of the i-th lowering generator is its negative.

The integral toral closure

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.definingIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 7)

The Hopf ideal cutting out the integral toral closure inside GL₇.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.definingIdeal_def : definingIdeal = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight

The defining ideal is the one supplied by the generic Kostant toral-closure construction.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.le_definingIdeal_iff (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 7)) : J ≤ definingIdeal ↔ (∀ (k : Fin 2 ⊕ Fin 2), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis))).toRingHom) ∧ J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap weight))).toRingHom

A Hopf ideal is contained in the defining ideal exactly when every represented simple-root subgroup and the weight torus kill it.

@[reducible, inline]

noncomputable abbrev TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The integral toral closure: the smallest closed subgroup scheme of GL₇ containing the represented simple root subgroups and the weight torus of the seven-dimensional module.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 7) definingIdeal

The quotient-spectrum presentation of the integral toral closure.

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.carrierι : groupScheme ⟶ GeneralLinear.groupScheme ℤ 7

The canonical inclusion of the integral toral closure into GL₇.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.carrierι_def : carrierι = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight

The ambient inclusion is the generic Kostant toral-closure inclusion.

instance TauCeti.G2ShortRoot.IntegralToralClosure.isClosedImmersion_carrierι : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left carrierι.hom.hom)

The integral toral closure is a closed subgroup scheme of GL₇.

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroup (k : Fin 2 ⊕ Fin 2) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme

A positive or negative numbered simple root subgroup of the integral toral closure.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroup_def (k : Fin 2 ⊕ Fin 2) : rootSubgroup k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight k

The numbered root subgroup is the one supplied by the generic Kostant toral-closure construction.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroup_comp_carrierι (k : Fin 2 ⊕ Fin 2) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) carrierι = UniversalEnvelopingAlgebra.kostantRootSubgroup (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis

Including a numbered root subgroup into GL₇ recovers its represented Kostant root subgroup.

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus : SplitTorus.groupScheme ℤ (Fin 2) ⟶ groupScheme

The rank-two split weight torus in the integral toral closure.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus_def : weightTorus = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight

The weight torus is the one supplied by the generic Kostant toral-closure construction.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus_comp_carrierι : CategoryTheory.CategoryStruct.comp weightTorus carrierι = GeneralLinear.weightTorus weight

Including the split weight torus into GL₇ recovers the diagonal torus of the weights.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 2 ⊕ Fin 2), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) (htorus : CategoryTheory.CategoryStruct.comp weightTorus f = CategoryTheory.CategoryStruct.comp weightTorus g) : f = g

Two morphisms out of the integral toral closure agree when they agree on every numbered simple root subgroup and on the split weight torus.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : f = g ↔ (∀ (k : Fin 2 ⊕ Fin 2), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) ∧ CategoryTheory.CategoryStruct.comp weightTorus f = CategoryTheory.CategoryStruct.comp weightTorus g

Matrix-valued points

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.points (A : Type v) [CommRing A] : Subgroup (GL (Fin 7) A)

The matrix-valued points of the integral toral closure.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.points_def (A : Type v) [CommRing A] : points A = GeneralLinear.hopfIdealPointsSubgroup 7 definingIdeal A

The points of the integral toral closure are cut out by its defining Hopf ideal.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.mem_points_iff (A : Type v) [CommRing A] (g : GL (Fin 7) A) : g ∈ points A ↔ ∀ x ∈ definingIdeal, ((GeneralLinear.pointsMulEquiv 7).symm g).ofConv x = 0

A matrix is a point of the integral toral closure exactly when its associated convolution point kills the defining Hopf ideal.

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroupPoints (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] : Multiplicative A →* ↥(points A)

The parametrized numbered simple root subgroup inside the integral toral closure points.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints_eq_kostantRootSubgroupMatrix (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints k A) u) = (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis) (AdditiveGroup.gaPointsMulEquiv.symm u)

A numbered simple-root point is the corresponding divided-power exponential matrix.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints k A) u) = 1 + Multiplicative.toAdd u • (rootMatrix k).map Int.cast + Multiplicative.toAdd u ^ 2 • (rootDividedSquareMatrix k).map Int.cast

A numbered simple-root point is 1 + t X + t² Y in the weight basis, for X the integral matrix of the generator and Y that of its divided square; Y vanishes at the two long-root indices.

noncomputable def TauCeti.G2ShortRoot.IntegralToralClosure.weightTorusPoints (A : Type v) [CommRing A] : (Fin 2 → Aˣ) →* ↥(points A)

The split weight torus inside the integral toral-closure points.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_weightTorusPoints (A : Type v) [CommRing A] (s : Fin 2 → Aˣ) : ↑((weightTorusPoints A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix lattice.toAddSubgroup latticeBasis weight) s

A split-torus point is the diagonal matrix whose entries are the weight characters.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints_inl_zero (A : Type v) [CommRing A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inl 0) A) (Multiplicative.ofAdd t)) = !![1, t, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, 0, 1, 2 * t, t ^ 2, 0, 0; 0, 0, 0, 1, t, 0, 0; 0, 0, 0, 0, 1, 0, 0; 0, 0, 0, 0, 0, 1, t; 0, 0, 0, 0, 0, 0, 1]

The short positive simple-root point x_{α₁}(t), written out.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints_inl_one (A : Type v) [CommRing A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inl 1) A) (Multiplicative.ofAdd t)) = !![1, 0, 0, 0, 0, 0, 0; 0, 1, t, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 1, t, 0; 0, 0, 0, 0, 0, 1, 0; 0, 0, 0, 0, 0, 0, 1]

The long positive simple-root point x_{α₂}(t), written out.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints_inr_zero (A : Type v) [CommRing A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inr 0) A) (Multiplicative.ofAdd t)) = !![1, 0, 0, 0, 0, 0, 0; t, 1, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0; 0, 0, t, 1, 0, 0, 0; 0, 0, t ^ 2, 2 * t, 1, 0, 0; 0, 0, 0, 0, 0, 1, 0; 0, 0, 0, 0, 0, t, 1]

The short negative simple-root point x_{-α₁}(t), written out.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_rootSubgroupPoints_inr_one (A : Type v) [CommRing A] (t : A) : ↑↑((rootSubgroupPoints (Sum.inr 1) A) (Multiplicative.ofAdd t)) = !![1, 0, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0; 0, t, 1, 0, 0, 0, 0; 0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 1, 0, 0; 0, 0, 0, 0, t, 1, 0; 0, 0, 0, 0, 0, 0, 1]

The long negative simple-root point x_{-α₂}(t), written out.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.coe_weightTorusPoints_eq_diagonal (A : Type v) [CommRing A] (s : Fin 2 → Aˣ) : ↑↑((weightTorusPoints A) s) = Matrix.diagonal fun (a : Fin 7) => ↑(torusCharacter s (weight a))

The matrix of a point of the integral toral closure's split weight torus is the diagonal matrix of the weight characters at that point.

Closed subgroups and the pinning equation

theorem TauCeti.G2ShortRoot.IntegralToralClosure.representedRootSubgroupCoordinateMap_surjective (k : Fin 2 ⊕ Fin 2) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis))

The represented integral root-subgroup coordinate map into the additive group is surjective.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroupCoordinateMap_surjective (k : Fin 2 ⊕ Fin 2) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight k))

The root-subgroup coordinate map remains surjective after adjoining the weight torus.

instance TauCeti.G2ShortRoot.IntegralToralClosure.isClosedImmersion_rootSubgroup (k : Fin 2 ⊕ Fin 2) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup k).hom.hom)

Every numbered simple root subgroup is a closed copy of the additive group.

instance TauCeti.G2ShortRoot.IntegralToralClosure.isClosedImmersion_weightTorus : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left weightTorus.hom.hom)

The weights make the rank-two split weight torus a closed immersion into the integral toral closure.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus_conj_rootSubgroup (k : Fin 2 ⊕ Fin 2) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 2)).X) (u : A) : CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (rootSubgroup k).hom.hom * (CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2 k)) * u))) (rootSubgroup k).hom.hom

The scheme-level pinning equation: conjugation by the weight torus acts on each numbered simple root subgroup through the corresponding type-G₂ root character.

@[simp]

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorusPoints_conj_rootSubgroupPoints (k : Fin 2 ⊕ Fin 2) (A : Type v) [CommRing A] (s : Fin 2 → Aˣ) (u : Multiplicative A) : (weightTorusPoints A) s * (rootSubgroupPoints k A) u * ((weightTorusPoints A) s)⁻¹ = (rootSubgroupPoints k A) (Multiplicative.ofAdd (↑(torusCharacter s (DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2 k)) * Multiplicative.toAdd u))

The pinning equation on matrix-valued points: conjugation by a point s of the weight torus rescales the parameter of each numbered simple root subgroup by the corresponding type-G₂ root character evaluated at s.