Presented points of the doubled minuscule E₆ carrier

TauCeti.E6DoubledMinuscule.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.
• R. W. Carter, Simple Groups of Lie Type, §12.2, for the doubled minuscule realization.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.

@[reducible, inline]

noncomputable abbrev TauCeti.E6DoubledMinuscule.pointsPresentation (A : Type v) [CommRing A] : GeneralLinear.IntegralPointsPresentation 54 definingIdeal A

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

Equations

• TauCeti.E6DoubledMinuscule.pointsPresentation A = ⟨TauCeti.E6DoubledMinuscule.points A, ⋯⟩

@[simp]

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

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