Presented points of the full-weight type-C carrier

TauCeti.SpStd.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, Sections 1.15 and 1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

@[reducible, inline]

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

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

Equations

• TauCeti.SpStd.pointsPresentation n A = ⟨TauCeti.SpStd.points n A, ⋯⟩

@[simp]

theorem TauCeti.SpStd.map_rootSubgroupPoints (n : ℕ) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (i : Fin (n + 1) ⊕ Fin (n + 1)) (u : Multiplicative A) : ((pointsPresentation n A).map (pointsPresentation n B) f) ((rootSubgroupPoints n i A) u) = (rootSubgroupPoints n i 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.SpStd.map_weightTorusPoints (n : ℕ) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (s : Fin (n + 1) → Aˣ) : ((pointsPresentation n A).map (pointsPresentation n B) f) ((weightTorusPoints n A) s) = (weightTorusPoints n B) fun (i : Fin (n + 1)) => (Units.map ↑f) (s i)

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