Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.SchemeGeneration

Scheme-theoretic root generation of full-weight Geck carriers #

The Geck carrier is defined as the closed subgroup scheme generated jointly by the numbered positive and negative simple-root subgroups and the represented weight torus. This file upgrades universal pointwise generation of the represented torus to equality of the toral and root-generated defining ideals and carriers.

The general results apply to every valid type whose Cartan rows are primitive. The specializations record E₈, F₄, and G₂, the three exceptional types whose Geck coordinate weights span the full character lattice and hence whose Geck tori are the full-weight tori used by the Chevalley--Demazure construction.

Main results #

TauCeti.DynkinType.geckDefiningIdeal_eq_kostantGeneratedDefiningIdeal: primitive Cartan rows make the torus redundant in the Geck defining ideal.
TauCeti.DynkinType.geckGroupScheme_eq_kostantGeneratedGroupScheme: the corresponding carrier equality.
TauCeti.DynkinType.geckGroupScheme_hom_ext_of_rootSubgroup: under the same hypothesis, a morphism out of the Geck carrier is determined by its restrictions to the numbered root subgroups.
The suffixes _E8, _F4, and _G2 record both equalities, the canonical comparison isomorphism, and this rigidity for the three full-weight Geck carriers.

References #

R. Steinberg, Lectures on Chevalley Groups, Section 3.
R. W. Carter, Simple Groups of Lie Type, Sections 6.4 and 7.1.

theorem TauCeti.DynkinType.geckDefiningIdeal_eq_kostantGeneratedDefiningIdeal_of_universal_torus_mem_elementary (t : DynkinType) (ht : t.Valid) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin t.rank))).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (t.geckTorusPoints ht A) (SplitTorus.pointsMulEquiv q) ∈ t.geckElementarySubgroup ht A) :

t.geckDefiningIdeal ht = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht)

Generation of the universal Geck torus makes the Geck defining ideal root-generated. It is enough to contain its universal point over the coordinate ring of the split torus itself.

theorem TauCeti.DynkinType.geckDefiningIdeal_eq_kostantGeneratedDefiningIdeal (t : DynkinType) (ht : t.Valid) (hrow : ∀ (i : Fin t.rank), ∃ (c : Fin t.rank → ℤ), ∑ j : Fin t.rank, t.cartanMatrix i j * c j = 1) :

t.geckDefiningIdeal ht = UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht)

Primitive Cartan rows make the Geck torus scheme-theoretically redundant. The defining Hopf ideal obtained from the numbered root subgroups and the weight torus is already the defining ideal generated by the numbered root subgroups alone.

theorem TauCeti.DynkinType.geckGroupScheme_eq_kostantGeneratedGroupScheme_of_universal_torus_mem_elementary (t : DynkinType) (ht : t.Valid) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin t.rank))).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (t.geckTorusPoints ht A) (SplitTorus.pointsMulEquiv q) ∈ t.geckElementarySubgroup ht A) :

t.geckGroupScheme ht = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht)

Generation of the universal Geck torus identifies the Geck and root-generated carriers. The carrier equality is induced by the equality of their defining Hopf ideals.

theorem TauCeti.DynkinType.geckGroupScheme_eq_kostantGeneratedGroupScheme (t : DynkinType) (ht : t.Valid) (hrow : ∀ (i : Fin t.rank), ∃ (c : Fin t.rank → ℤ), ∑ j : Fin t.rank, t.cartanMatrix i j * c j = 1) :

t.geckGroupScheme ht = UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht)

Primitive Cartan rows identify the Geck carrier with the root-generated Kostant carrier. Thus the represented weight torus adds no scheme-theoretic generator.

theorem TauCeti.DynkinType.isIso_kostantGeneratedToToral_geck_of_universal_torus_mem_elementary (t : DynkinType) (ht : t.Valid) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin t.rank))).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (t.geckTorusPoints ht A) (SplitTorus.pointsMulEquiv q) ∈ t.geckElementarySubgroup ht A) :

CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht))

Generation of the universal Geck torus makes the canonical comparison from the root-generated Kostant carrier to the Geck toral carrier an isomorphism.

theorem TauCeti.DynkinType.isIso_kostantGeneratedToToral_geck (t : DynkinType) (ht : t.Valid) (hrow : ∀ (i : Fin t.rank), ∃ (c : Fin t.rank → ℤ), ∑ j : Fin t.rank, t.cartanMatrix i j * c j = 1) :

CategoryTheory.IsIso (UniversalEnvelopingAlgebra.kostantGeneratedToToral (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht))

Primitive Cartan rows make the canonical comparison from the root-generated Kostant carrier to the Geck toral carrier an isomorphism.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext_of_rootSubgroup_of_universal_torus_mem_elementary (t : DynkinType) (ht : t.Valid) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin t.rank))).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (t.geckTorusPoints ht A) (SplitTorus.pointsMulEquiv q) ∈ t.geckElementarySubgroup ht A) {Y : CommHopfAlgCat ℤ} (φ ψ : t.geckGroupScheme ht ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin t.rank ⊕ Fin t.rank), CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) φ = CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) ψ) :

φ = ψ

Generation of the universal Geck torus makes the Geck carrier rigid in its root subgroups. Two morphisms out of the carrier agree as soon as they agree on its numbered positive and negative simple-root subgroups; the weight-torus hypothesis of TauCeti.DynkinType.geckGroupScheme_hom_ext is then redundant.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext_of_rootSubgroup (t : DynkinType) (ht : t.Valid) (hrow : ∀ (i : Fin t.rank), ∃ (c : Fin t.rank → ℤ), ∑ j : Fin t.rank, t.cartanMatrix i j * c j = 1) {Y : CommHopfAlgCat ℤ} (φ ψ : t.geckGroupScheme ht ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin t.rank ⊕ Fin t.rank), CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) φ = CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) ψ) :

φ = ψ

Primitive Cartan rows make the Geck carrier rigid in its root subgroups. Two morphisms out of the carrier agree as soon as they agree on its numbered positive and negative simple-root subgroups.

Full-weight exceptional Geck carriers #

The type-E₈ Geck defining ideal is generated scheme-theoretically by its sixteen numbered positive and negative simple-root subgroups; adjoining the weight torus does not change it.

The type-E₈ full-weight Geck carrier is the closed group scheme generated by its sixteen numbered positive and negative simple-root subgroups alone.

For type E₈, the canonical comparison from the root-generated Kostant carrier to the Geck toral carrier is an isomorphism.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext_of_rootSubgroup_E8 {Y : CommHopfAlgCat ℤ} (φ ψ : E8.geckGroupScheme valid_E8 ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin E8.rank ⊕ Fin E8.rank), CategoryTheory.CategoryStruct.comp (E8.geckRootSubgroup valid_E8 i) φ = CategoryTheory.CategoryStruct.comp (E8.geckRootSubgroup valid_E8 i) ψ) :

φ = ψ

Two morphisms out of the type-E₈ full-weight Geck carrier agree as soon as they agree on its sixteen numbered positive and negative simple-root subgroups.

The type-F₄ Geck defining ideal is generated scheme-theoretically by its eight numbered positive and negative simple-root subgroups; adjoining the weight torus does not change it.

The type-F₄ full-weight Geck carrier is the closed group scheme generated by its eight numbered positive and negative simple-root subgroups alone.

For type F₄, the canonical comparison from the root-generated Kostant carrier to the Geck toral carrier is an isomorphism.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext_of_rootSubgroup_F4 {Y : CommHopfAlgCat ℤ} (φ ψ : F4.geckGroupScheme valid_F4 ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin F4.rank ⊕ Fin F4.rank), CategoryTheory.CategoryStruct.comp (F4.geckRootSubgroup valid_F4 i) φ = CategoryTheory.CategoryStruct.comp (F4.geckRootSubgroup valid_F4 i) ψ) :

φ = ψ

Two morphisms out of the type-F₄ full-weight Geck carrier agree as soon as they agree on its eight numbered positive and negative simple-root subgroups.

The type-G₂ Geck defining ideal is generated scheme-theoretically by its four numbered positive and negative simple-root subgroups; adjoining the weight torus does not change it.

The type-G₂ full-weight Geck carrier is the closed group scheme generated by its four numbered positive and negative simple-root subgroups alone.

For type G₂, the canonical comparison from the root-generated Kostant carrier to the Geck toral carrier is an isomorphism.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext_of_rootSubgroup_G2 {Y : CommHopfAlgCat ℤ} (φ ψ : G2.geckGroupScheme valid_G2 ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : Fin G2.rank ⊕ Fin G2.rank), CategoryTheory.CategoryStruct.comp (G2.geckRootSubgroup valid_G2 i) φ = CategoryTheory.CategoryStruct.comp (G2.geckRootSubgroup valid_G2 i) ψ) :

φ = ψ

Two morphisms out of the type-G₂ full-weight Geck carrier agree as soon as they agree on its four numbered positive and negative simple-root subgroups.