Presented points of the pinned Geck carrier

TauCeti.DynkinType.geckPointsPresentation presents the matrix points of the pinned Geck carrier by its integral defining Hopf ideal. The shared GeneralLinear.IntegralPointsPresentation API supplies maps of value rings, their functoriality, and the representing equivalence with quotient-algebra points. The scheme-points equivalence identifies these matrix points with morphisms into the Geck carrier and carries each numbered root-subgroup morphism to the existing point-level homomorphism. This file also proves that maps of value rings preserve the pinned root subgroups and weight torus.

The Geck weights span the root lattice rather than, in general, the full character lattice. This presentation does not identify the carrier with the simply connected group or its points with the elementary subgroup generated by its root subgroups.

The matrix-points presentation is universe-polymorphic. The Geck carrier is a scheme over Spec ℤ in universe zero, so its scheme-valued points over Spec A use value rings A : Type.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.geckPointsPresentation (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : GeneralLinear.IntegralPointsPresentation (t.geckDim ht) (t.geckDefiningIdeal ht) A

The matrix points of the pinned Geck carrier, presented by its integral defining Hopf ideal.

Equations

• t.geckPointsPresentation ht A = ⟨t.geckPoints ht A, ⋯⟩

noncomputable def TauCeti.DynkinType.geckCoordinatePointMulEquiv (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(t.geckPoints ht A)

Quotient-coordinate points of the Geck carrier, identified with its matrix points.

Equations

• t.geckCoordinatePointMulEquiv ht A = (t.geckPointsPresentation ht ↑↧A).mulEquiv

theorem TauCeti.DynkinType.geckCoordinatePointMulEquiv_mapPoints (t : DynkinType) (ht : t.Valid) {A B : Type v} [CommRing A] [CommRing B] (f : A →ₐ[ℤ] B) (q : ↑(HopfAlgebra.points ↧A)) : (t.geckCoordinatePointMulEquiv ht B) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints (CommAlgCat.ofHom f))) q) = ((t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht B) f.toRingHom) ((t.geckCoordinatePointMulEquiv ht A) q)

The coordinate-point equivalence is natural in the value algebra.

noncomputable def TauCeti.DynkinType.geckCoordinatePoint (t : DynkinType) (ht : t.Valid) (g : ↥(t.geckPoints ht ℤ)) : ↑(HopfAlgebra.points ↧ℤ)

An integral point of the Geck carrier, read intrinsically as a point of its coordinate Hopf algebra.

Equations

• t.geckCoordinatePoint ht g = (t.geckCoordinatePointMulEquiv ht ℤ).symm g

@[simp]

theorem TauCeti.DynkinType.geckCoordinatePointMulEquiv_geckCoordinatePoint (t : DynkinType) (ht : t.Valid) (g : ↥(t.geckPoints ht ℤ)) : (t.geckCoordinatePointMulEquiv ht ℤ) (t.geckCoordinatePoint ht g) = g

Passing an intrinsic coordinate point back through the presentation recovers the original integral Geck point.

@[simp]

theorem TauCeti.DynkinType.geckCoordinatePointMulEquiv_extendPoint_geckCoordinatePoint (t : DynkinType) (ht : t.Valid) (g : ↥(t.geckPoints ht ℤ)) (A : Type v) [CommRing A] : (t.geckCoordinatePointMulEquiv ht A) ((HopfAlgebra.extendPoint ↑(t.geckCoordinateHopfAlgebra ht) ↧A) (t.geckCoordinatePoint ht g)) = ((t.geckPointsPresentation ht ℤ).map (t.geckPointsPresentation ht A) (Int.castRingHom A)) g

Extending the coordinate point of an integral Geck point to a commutative ring agrees with the presented-points map on that point.

Scheme-valued points of the carrier

noncomputable def TauCeti.DynkinType.geckGroupSchemePointMulEquiv (t : DynkinType) (ht : t.Valid) (A : Type) [CommRing A] : ↑(HopfAlgebra.points ↧A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (t.geckGroupScheme ht).X)

Quotient-Hopf-algebra points of the Geck carrier, transported to scheme-valued points.

Equations

• t.geckGroupSchemePointMulEquiv ht A = TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation (t.geckCoordinateHopfAlgebra ht) A ⋯

@[simp]

theorem TauCeti.DynkinType.geckGroupSchemePointMulEquiv_apply_left (t : DynkinType) (ht : t.Valid) (A : Type) [CommRing A] (q : ↑(HopfAlgebra.points ↧A)) : CategoryTheory.Over.Hom.left ((t.geckGroupSchemePointMulEquiv ht A) q) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑q.ofConv)) (CategoryTheory.eqToHom ⋯)

The underlying spectrum map of a quotient point of the Geck carrier.

noncomputable def TauCeti.DynkinType.geckSchemePointsMulEquiv (t : DynkinType) (ht : t.Valid) (A : Type) [CommRing A] : ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (t.geckGroupScheme ht).X) ≃* ↥(t.geckPoints ht A)

Scheme-valued points of the Geck carrier, identified with its matrix points.

Equations

• t.geckSchemePointsMulEquiv ht A = (t.geckGroupSchemePointMulEquiv ht A).symm.trans (t.geckCoordinatePointMulEquiv ht A)

@[simp]

theorem TauCeti.DynkinType.geckSchemePointsMulEquiv_groupSchemePointMulEquiv (t : DynkinType) (ht : t.Valid) (A : Type) [CommRing A] (q : ↑(HopfAlgebra.points ↧A)) : (t.geckSchemePointsMulEquiv ht A) ((t.geckGroupSchemePointMulEquiv ht A) q) = (t.geckCoordinatePointMulEquiv ht A) q

Evaluating the scheme-points equivalence on a presented quotient point recovers its matrix point.

@[simp]

theorem TauCeti.DynkinType.geckSchemePointsMulEquiv_mapValue (t : DynkinType) (ht : t.Valid) {A B : Type} [CommRing A] [CommRing B] (f : A →+* B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (t.geckGroupScheme ht).X) : (t.geckSchemePointsMulEquiv ht B) (CategoryTheory.CategoryStruct.comp (have x := ⋯; AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f)) (AlgebraicGeometry.Spec ↧ℤ)) p) = ((t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht B) f) ((t.geckSchemePointsMulEquiv ht A) p)

The scheme-valued point identification is covariantly natural in the value ring. A ring homomorphism A → B becomes precomposition by the reversed spectrum map and acts through the presented-points map on the corresponding Geck point.

@[simp]

theorem TauCeti.DynkinType.geckSchemePointsMulEquiv_comp_geckRootSubgroup (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : (t.geckSchemePointsMulEquiv ht A) (CategoryTheory.CategoryStruct.comp p (t.geckRootSubgroup ht i).hom.hom) = (t.geckRootSubgroupPoints ht i A) ((AdditiveGroup.schemePointsMulEquiv A) p)

The map on scheme-valued points induced by a numbered Geck root-subgroup morphism is the existing matrix-valued root-subgroup homomorphism.

@[simp]

theorem TauCeti.DynkinType.map_geckRootSubgroupPoints (t : DynkinType) (ht : t.Valid) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (i : Fin t.rank ⊕ Fin t.rank) (u : Multiplicative A) : ((t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht B) f) ((t.geckRootSubgroupPoints ht i A) u) = (t.geckRootSubgroupPoints ht i B) (Multiplicative.ofAdd (f (Multiplicative.toAdd u)))

The induced map carries a numbered root-subgroup point along the homomorphism of value rings.

@[simp]

theorem TauCeti.DynkinType.map_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (s : Fin t.rank → Aˣ) : ((t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht B) f) ((t.geckWeightTorusPoints ht A) s) = (t.geckWeightTorusPoints ht B) fun (j : Fin t.rank) => (Units.map ↑f) (s j)

The induced map carries a point of the pinned Geck weight torus along the homomorphism of value rings, parameter by parameter.