Presented points of the full-weight type-A carrier

TauCeti.SlStd.pointsPresentation presents the carrier's matrix points by its defining integral Hopf ideal. The shared GeneralLinear.IntegralPointsPresentation API supplies maps of value rings, their functoriality, and the representing equivalence with quotient-algebra points. This file proves that those maps preserve the pinned root subgroups and weight torus.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

@[reducible, inline]

noncomputable abbrev TauCeti.SlStd.pointsPresentation (r : ℕ) (A : Type v) [CommRing A] : GeneralLinear.IntegralPointsPresentation (r + 1) (definingIdeal r) A

The carrier's matrix points, presented by its defining integral Hopf ideal.

Equations

• TauCeti.SlStd.pointsPresentation r A = ⟨TauCeti.SlStd.points r A, ⋯⟩

@[simp]

theorem TauCeti.SlStd.map_rootSubgroupPoints (r : ℕ) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (k : Fin r ⊕ Fin r) (u : Multiplicative A) : ((pointsPresentation r A).map (pointsPresentation r B) f) ((rootSubgroupPoints r k A) u) = (rootSubgroupPoints r k B) (Multiplicative.ofAdd (f (Multiplicative.toAdd u)))

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

@[simp]

theorem TauCeti.SlStd.map_weightTorusPoints (r : ℕ) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (s : Fin r → Aˣ) : ((pointsPresentation r A).map (pointsPresentation r B) f) ((weightTorusPoints r A) s) = (weightTorusPoints r B) fun (i : Fin r) => (Units.map ↑f) (s i)

The induced map carries a point of the pinned split weight torus coordinatewise along the homomorphism of value rings.