The Kostant toral-closure group scheme of the pinned Geck lattice

TauCeti.DynkinType.lieAlgebra is the split Lie algebra of a valid Dynkin type, realized by Geck's construction as explicit matrices acting on the coordinate space GeckIndex → ℚ, and TauCeti.DynkinType.geckCoordinateLattice is the ℤ-lattice of integral coordinate vectors in that space, preserved by the whole simple-generator Kostant form. This file feeds that pinned data into the Kostant toral-closure construction and so produces, for every valid Dynkin type, an explicit affine group scheme over ℤ: the smallest closed subgroup scheme of GLₙ containing the divided-power exponential root subgroups of the numbered Chevalley generators together with the weight torus of the Geck coordinate weights.

The lattice, weights, and nilpotent root vectors are read off the Bourbaki-numbered pinned data, so the carrier traces back to explicit matrices. The ambient coordinate ordering is the arbitrary Fintype.equivFin reindexing of GeckIndex, and hence is pinned only up to that permutation. The size of the ambient general linear group is TauCeti.DynkinType.geckDim_eq_rank_add_numRoots, namely rank + numRoots. In the classical construction Geck's module is the adjoint module and its weights are the roots, so this carrier is expected to be the adjoint form; those identifications are not formalized here. The simply connected carrier required by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md needs instead an admissible lattice whose weights generate the full weight lattice. That lattice, the Borel, root subgroups for nonsimple roots, the Chevalley commutator relations, and the root-datum properties that turn a carrier into a pinned split reductive group scheme are the Layer 9 work that remains; the functoriality of geckPoints in the value ring is supplied by TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.PointsFunctor.

This construction supplies part of the interface that Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md asks for: the closed immersion into GLₙ, the root subgroup morphisms x_{±α_i} : 𝔾ₐ → G of the numbered simple raising and lowering generators and the weight-torus morphism T → G that factor through it, the group of A-valued points for every commutative ring A, and the pinning equation s x_i(u) s⁻¹ = x_i(α_i(s) u) expressing the torus action on a root subgroup through the Bourbaki row of the Cartan matrix. No reductivity, maximality of the torus, finiteness, or root-datum statement is asserted.

Main definitions

• TauCeti.DynkinType.geckDefiningIdeal and TauCeti.DynkinType.geckGroupScheme: the defining Hopf ideal and the resulting affine group scheme over ℤ.
• TauCeti.DynkinType.geckCoordinateHopfAlgebra: the coordinate Hopf algebra representing the carrier.
• TauCeti.DynkinType.geckGroupSchemeι: its closed immersion into GLₙ.
• TauCeti.DynkinType.geckRootSubgroup and TauCeti.DynkinType.geckWeightTorus: the root subgroup and weight-torus morphisms into the carrier.
• TauCeti.DynkinType.geckPoints: the A-valued points of the carrier, as matrices.
• TauCeti.DynkinType.geckRootSubgroupPoints and TauCeti.DynkinType.geckWeightTorusPoints: the numbered root subgroups and represented weight torus inside the point group.

Main results

• TauCeti.DynkinType.geckRootSubgroup_comp_ι and TauCeti.DynkinType.geckWeightTorus_comp_ι: both families recover their represented morphisms into GLₙ.
• TauCeti.DynkinType.geckWeightTorus_conj_geckRootSubgroup: the scheme-level pinning equation.
• TauCeti.DynkinType.isClosedImmersion_geckWeightTorus and TauCeti.DynkinType.geckTorusPoints_injective: weights generating the character lattice embed the weight torus in the carrier, on schemes and on points.
• TauCeti.DynkinType.geckGroupScheme_hom_ext: morphisms from the carrier into affine group schemes represented by commutative Hopf algebras are determined by their composites with the root subgroups and weight torus.
• TauCeti.DynkinType.geckTorusPoints_conj_geckRootSubgroupParam: the pinning equation, with the root of a raising generator the corresponding pinned Cartan-matrix row and that of a lowering generator its negative.
• TauCeti.DynkinType.geckWeightTorusPoints_conj_geckRootSubgroupPoints: the same pinning equation inside the points of the carrier.
• TauCeti.DynkinType.map_geckElementarySubgroup_conj_geckTorusPoints: the torus normalizes the elementary group.
• TauCeti.DynkinType.map_geckTorusSubsystemSubgroup_le_geckPoints: the pointwise group generated by the torus and a chosen set of numbered root subgroups lies in the points of the carrier.
• TauCeti.DynkinType.geckPoints_def: the points are the matrices cut out by the defining ideal.
• TauCeti.DynkinType.geckPoints_mk_geckTorusMatrix: the weight-torus matrix and the diagonal matrix of the weight characters are the same point.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

This advances "The Chevalley--Demazure construction", "Root subgroup maps" and "Points over an algebraically closed field" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, whose consumer is the pinned ambient group of milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

The group scheme

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckDefiningIdeal (t : DynkinType) (ht : t.Valid) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht))

The defining Hopf ideal of the Geck carrier of a valid Dynkin type: the largest Hopf ideal of the coordinate algebra of GLₙ killed by every numbered Kostant root subgroup and by the weight torus of the Geck lattice.

This is an abbreviation because the presented quotient-coordinate API is indexed by the ideal itself; definitional transparency lets that API specialize to the pinned Kostant ideal without transporting every point and coordinate morphism across an equality of ideals.

Equations

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

theorem TauCeti.DynkinType.geckDefiningIdeal_def (t : DynkinType) (ht : t.Valid) : t.geckDefiningIdeal ht = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht)

The defining ideal of the Geck carrier is the Kostant toral defining ideal of the pinned Geck data.

noncomputable def TauCeti.DynkinType.geckGroupScheme (t : DynkinType) (ht : t.Valid) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The Kostant toral-closure group scheme of the pinned Geck lattice: the smallest closed subgroup scheme of GLₙ over ℤ, with n = rank + numRoots, containing every divided-power exponential root subgroup of a numbered Chevalley generator and the weight torus of the Geck coordinates.

Every ingredient is explicit pinned data, so no carrier is chosen from an existence theorem. Reductivity, and the identification of its root datum, are not claimed.

Equations

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

theorem TauCeti.DynkinType.geckGroupScheme_def (t : DynkinType) (ht : t.Valid) : t.geckGroupScheme ht = UniversalEnvelopingAlgebra.kostantToralGroupScheme (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht)

The Geck carrier is the Kostant toral-closure group scheme of the pinned Geck data.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckCoordinateHopfAlgebra (t : DynkinType) (ht : t.Valid) : CommHopfAlgCat ℤ

The coordinate Hopf algebra of the Geck carrier.

This is a type abbreviation so the quotient-coordinate point API recognizes the representing quotient without transports across an equality of bundled Hopf algebras.

Equations

• t.geckCoordinateHopfAlgebra ht = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht)) (t.geckDefiningIdeal ht)

theorem TauCeti.DynkinType.geckCoordinateHopfAlgebra_def (t : DynkinType) (ht : t.Valid) : t.geckCoordinateHopfAlgebra ht = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (t.geckDim ht)) (t.geckDefiningIdeal ht)

The coordinate Hopf algebra is the quotient by the Geck defining ideal.

theorem TauCeti.DynkinType.geckGroupScheme_eq_hopfSpec (t : DynkinType) (ht : t.Valid) : t.geckGroupScheme ht = (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op (t.geckCoordinateHopfAlgebra ht))

The Geck carrier is the Hopf spectrum of its coordinate Hopf algebra.

theorem TauCeti.DynkinType.geckGroupScheme_X_left (t : DynkinType) (ht : t.Valid) : (t.geckGroupScheme ht).X.left = AlgebraicGeometry.Spec ↧↑(t.geckCoordinateHopfAlgebra ht)

The underlying scheme of the Geck carrier is the spectrum of its coordinate ring.

noncomputable def TauCeti.DynkinType.geckGroupSchemeι (t : DynkinType) (ht : t.Valid) : t.geckGroupScheme ht ⟶ GeneralLinear.groupScheme ℤ (t.geckDim ht)

The Geck carrier is a closed subgroup scheme of GLₙ.

Equations

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

theorem TauCeti.DynkinType.geckGroupSchemeι_def (t : DynkinType) (ht : t.Valid) : t.geckGroupSchemeι ht = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht))

The carrier inclusion is the Kostant toral-closure inclusion for the pinned Geck data.

instance TauCeti.DynkinType.isClosedImmersion_geckGroupSchemeι (t : DynkinType) (ht : t.Valid) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (t.geckGroupSchemeι ht).hom.hom)

The inclusion of the Geck carrier into GLₙ is a closed immersion.

noncomputable def TauCeti.DynkinType.geckRootSubgroup (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) : AdditiveGroup.groupScheme ℤ ⟶ t.geckGroupScheme ht

The i-th root subgroup of the Geck carrier, the divided-power exponential of the numbered raising or lowering generator, factored through the carrier.

Equations

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

theorem TauCeti.DynkinType.geckRootSubgroup_def (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) : t.geckRootSubgroup ht i = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht) i) (CategoryTheory.eqToHom ⋯)

A pinned root-subgroup morphism is the corresponding Kostant toral-closure morphism.

@[simp]

theorem TauCeti.DynkinType.geckRootSubgroup_comp_ι (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) : CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) (t.geckGroupSchemeι ht) = UniversalEnvelopingAlgebra.kostantRootSubgroup (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ i ⋯ (t.geckCoordinateBasisFin ht)

Including a root subgroup of the Geck carrier into GLₙ recovers the represented Kostant root subgroup of the corresponding numbered generator.

noncomputable def TauCeti.DynkinType.geckWeightTorus (t : DynkinType) (ht : t.Valid) : SplitTorus.groupScheme ℤ (Fin t.rank) ⟶ t.geckGroupScheme ht

The represented weight torus of the Geck lattice, factored through the carrier. This is a weight-torus morphism into the carrier; it is not asserted to be a monomorphism.

Equations

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

theorem TauCeti.DynkinType.geckWeightTorus_def (t : DynkinType) (ht : t.Valid) : t.geckWeightTorus ht = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantWeightTorusToToral (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht)) (CategoryTheory.eqToHom ⋯)

The pinned weight-torus morphism is the Kostant toral-closure weight-torus morphism.

@[simp]

theorem TauCeti.DynkinType.geckWeightTorus_comp_ι (t : DynkinType) (ht : t.Valid) : CategoryTheory.CategoryStruct.comp (t.geckWeightTorus ht) (t.geckGroupSchemeι ht) = GeneralLinear.weightTorus (t.geckWeightFin ht)

Including the weight-torus morphism into GLₙ recovers the diagonal weight torus of the Geck lattice.

theorem TauCeti.DynkinType.isClosedImmersion_geckWeightTorus (t : DynkinType) (ht : t.Valid) (hwt : Submodule.span ℤ (Set.range (t.geckWeightFin ht)) = ⊤) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (t.geckWeightTorus ht).hom.hom)

Weights generating the character lattice embed the weight torus as a closed subgroup scheme of the Geck carrier. The hypothesis fails in general, since the Geck weights generate only the root lattice; the types where it holds are settled in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.FullWeight.

@[simp]

theorem TauCeti.DynkinType.geckWeightTorus_conj_geckRootSubgroup (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin t.rank)).X) (u : A) : CategoryTheory.CategoryStruct.comp s (t.geckWeightTorus ht).hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (t.geckRootSubgroup ht i).hom.hom * (CategoryTheory.CategoryStruct.comp s (t.geckWeightTorus ht).hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (t.rootGeneratorWeight ht i)) * u))) (t.geckRootSubgroup ht i).hom.hom

The intrinsic pinning equation for the Geck carrier. On points over a commutative ring, conjugation by a weight-torus point rescales the parameter of a numbered root subgroup by the corresponding root character.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext (t : DynkinType) (ht : t.Valid) {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) ψ) (htorus : CategoryTheory.CategoryStruct.comp (t.geckWeightTorus ht) φ = CategoryTheory.CategoryStruct.comp (t.geckWeightTorus ht) ψ) : φ = ψ

Rigidity of the Geck carrier. Two homomorphisms from the carrier into an affine group scheme represented by a commutative Hopf algebra are equal if they agree on every numbered root subgroup and on the represented weight torus.

theorem TauCeti.DynkinType.geckGroupScheme_hom_ext_iff {t : DynkinType} {ht : t.Valid} {Y : CommHopfAlgCat ℤ} {φ ψ : t.geckGroupScheme ht ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : φ = ψ ↔ (∀ (i : Fin t.rank ⊕ Fin t.rank), CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) φ = CategoryTheory.CategoryStruct.comp (t.geckRootSubgroup ht i) ψ) ∧ CategoryTheory.CategoryStruct.comp (t.geckWeightTorus ht) φ = CategoryTheory.CategoryStruct.comp (t.geckWeightTorus ht) ψ

Pinned pointwise subgroups

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckTorusPoints (t : DynkinType) (ht : t.Valid) (A : CommAlgCat ℤ) : (Fin t.rank → (↑A)ˣ) →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(t.geckCoordinateLattice ht).toAddSubgroup)

The represented Geck weight torus on points of a value algebra.

Equations

• t.geckTorusPoints ht A = TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints (t.geckCoordinateLattice ht).toAddSubgroup (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht) ↑A

theorem TauCeti.DynkinType.geckTorusPoints_injective (t : DynkinType) (ht : t.Valid) (A : CommAlgCat ℤ) (hwt : Submodule.span ℤ (Set.range (t.geckWeightFin ht)) = ⊤) : Function.Injective ⇑(t.geckTorusPoints ht A)

Weights generating the character lattice make the Geck weight torus injective on points, over every value algebra. This is the point-level counterpart of TauCeti.DynkinType.isClosedImmersion_geckWeightTorus, proved from the same hypothesis rather than transported across it: the identification of Fin t.rank → Aˣ with the scheme-theoretic A-points of the split torus, and the compatibility of geckTorusPoints with geckWeightTorus, are not established here.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckRootSubgroupParam (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : CommAlgCat ℤ) : Multiplicative ↑A →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(t.geckCoordinateLattice ht).toAddSubgroup)

The parametrized root subgroup for a numbered Geck root generator.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckElementarySubgroup (t : DynkinType) (ht : t.Valid) (A : CommAlgCat ℤ) : Subgroup (LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(t.geckCoordinateLattice ht).toAddSubgroup))

The elementary subgroup generated by all numbered Geck root subgroups.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckTorusSubsystemSubgroup (t : DynkinType) (ht : t.Valid) (S : Set (Fin t.rank ⊕ Fin t.rank)) (A : CommAlgCat ℤ) : Subgroup (LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥(t.geckCoordinateLattice ht).toAddSubgroup))

The subgroup generated by the represented Geck weight torus and a chosen set of numbered root subgroups.

Equations

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

The pinning equation

theorem TauCeti.DynkinType.geckTorusPoints_conj_geckRootSubgroupParam (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : CommAlgCat ℤ) (s : Fin t.rank → (↑A)ˣ) (u : Multiplicative ↑A) : (t.geckTorusPoints ht A) s * (t.geckRootSubgroupParam ht i A) u * ((t.geckTorusPoints ht A) s)⁻¹ = (t.geckRootSubgroupParam ht i A) (Multiplicative.ofAdd (↑(torusCharacter s (t.rootGeneratorWeight ht i)) * Multiplicative.toAdd u))

The pinning equation for the Geck carrier of a valid Dynkin type. A torus point s conjugates the root-subgroup element of parameter u into the one of parameter α_i(s) u, where α_i is the i-th Bourbaki row of the Cartan matrix on a raising generator and its negative on a lowering one.

This is the equation against which the numbered conventions of downstream Steinberg maps are stated.

theorem TauCeti.DynkinType.map_geckElementarySubgroup_conj_geckTorusPoints (t : DynkinType) (ht : t.Valid) (A : CommAlgCat ℤ) (s : Fin t.rank → (↑A)ˣ) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj ((t.geckTorusPoints ht A) s))) (t.geckElementarySubgroup ht A) = t.geckElementarySubgroup ht A

The represented weight torus normalizes the elementary group. Conjugation by a torus point rescales the parameter of each numbered root subgroup by the value of its root, so it preserves the group the root subgroups generate.

The points of the carrier

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckRootSubgroupMatrix (t : DynkinType) (ht : t.Valid) {A : Type v} [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A) →* GL (Fin (t.geckDim ht)) A

A numbered Geck root subgroup written in the finite coordinate basis.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckTorusMatrix (t : DynkinType) (ht : t.Valid) {A : Type v} [CommRing A] : (Fin t.rank → Aˣ) →* GL (Fin (t.geckDim ht)) A

The represented Geck weight torus written in the finite coordinate basis.

Equations

• t.geckTorusMatrix ht = TauCeti.UniversalEnvelopingAlgebra.kostantTorusMatrix (t.geckCoordinateLattice ht).toAddSubgroup (t.geckCoordinateBasisFin ht) (t.geckWeightFin ht)

noncomputable def TauCeti.DynkinType.geckPoints (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : Subgroup (GL (Fin (t.geckDim ht)) A)

The A-valued points of the Geck carrier of a valid Dynkin type, as a subgroup of GLₙ(A) through the Hopf-ideal quotient presentation and the Geck coordinate basis.

Equations

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

theorem TauCeti.DynkinType.geckPoints_def (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : t.geckPoints ht A = GeneralLinear.hopfIdealPointsSubgroup (t.geckDim ht) (t.geckDefiningIdeal ht) A

The points of the Geck carrier are cut out by its defining Hopf ideal. This is the form in which the q-power Frobenius of TauCeti/Algebra/AlgebraicGroup/Frobenius/GeneralLinear.lean acts on them.

@[simp]

theorem TauCeti.DynkinType.mem_geckPoints_iff (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (g : GL (Fin (t.geckDim ht)) A) : g ∈ t.geckPoints ht A ↔ ∀ x ∈ t.geckDefiningIdeal ht, ((GeneralLinear.pointsMulEquiv (t.geckDim ht)).symm g).ofConv x = 0

A matrix is a point of the Geck carrier exactly when the associated convolution point kills its defining Hopf ideal.

theorem TauCeti.DynkinType.geckRootSubgroupMatrix_mem_geckPoints (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (i : Fin t.rank ⊕ Fin t.rank) (q : ↑(HopfAlgebra.points ↧A)) : (t.geckRootSubgroupMatrix ht i) q ∈ t.geckPoints ht A

Every matrix in a numbered Geck root subgroup is a point of the carrier.

theorem TauCeti.DynkinType.geckTorusMatrix_mem_geckPoints (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) : (t.geckTorusMatrix ht) s ∈ t.geckPoints ht A

Every represented Geck weight-torus matrix is a point of the carrier.

noncomputable def TauCeti.DynkinType.geckRootSubgroupPoints (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : Type v) [CommRing A] : Multiplicative A →* ↥(t.geckPoints ht A)

The parametrized numbered root subgroup inside the Geck carrier points. The parameter is read through the canonical multiplicative copy of the additive group of A.

Equations

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

@[simp]

theorem TauCeti.DynkinType.coe_geckRootSubgroupPoints (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((t.geckRootSubgroupPoints ht i A) u) = (t.geckRootSubgroupMatrix ht i) (AdditiveGroup.gaPointsMulEquiv.symm u)

A parametrized Geck root-subgroup point has the represented root-subgroup matrix as its underlying general-linear element.

noncomputable def TauCeti.DynkinType.geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : (Fin t.rank → Aˣ) →* ↥(t.geckPoints ht A)

The represented weight torus inside the Geck carrier points.

Equations

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

@[simp]

theorem TauCeti.DynkinType.coe_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) : ↑((t.geckWeightTorusPoints ht A) s) = (t.geckTorusMatrix ht) s

A represented Geck weight-torus point has the weight-torus matrix as its underlying general-linear element.

@[simp]

theorem TauCeti.DynkinType.geckWeightTorusPoints_conj_geckRootSubgroupPoints (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) (u : Multiplicative A) : (t.geckWeightTorusPoints ht A) s * (t.geckRootSubgroupPoints ht i A) u * ((t.geckWeightTorusPoints ht A) s)⁻¹ = (t.geckRootSubgroupPoints ht i A) (Multiplicative.ofAdd (↑(torusCharacter s (t.rootGeneratorWeight ht i)) * Multiplicative.toAdd u))

The pinning equation inside the points of the Geck carrier. Conjugation by a represented weight-torus point rescales a numbered root-subgroup parameter by the corresponding root character.

theorem TauCeti.DynkinType.geckPoints_mk_geckTorusMatrix (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) : ⟨(t.geckTorusMatrix ht) s, ⋯⟩ = ⟨diagGL fun (i : Fin (t.geckDim ht)) => torusCharacter s (t.geckWeightFin ht i), ⋯⟩

The two representations of a weight-torus point of the carrier agree: writing the point through TauCeti.DynkinType.geckTorusMatrix and writing it as the diagonal matrix of the weight characters give the same element of TauCeti.DynkinType.geckPoints. Both occur in the pinning equations, which state the parameter of a torus point in the second form and its value in the first.

theorem TauCeti.DynkinType.map_geckTorusSubsystemSubgroup_le_geckPoints (t : DynkinType) (ht : t.Valid) (S : Set (Fin t.rank ⊕ Fin t.rank)) (A : Type v) [CommRing A] : Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A (t.geckCoordinateBasisFin ht))).toMulEquiv) (t.geckTorusSubsystemSubgroup ht S ↧A) ≤ t.geckPoints ht A

A pointwise torus-subsystem group lies in the points of the carrier. The subgroup of Aut_A(A ⊗ M) generated by the torus and a chosen set of numbered root subgroups, written in the Geck coordinate basis, is contained in the A-valued points of the group scheme.