The points of the type-F4 short-root carrier, functorially

TauCeti.F4ShortRoot.groupScheme is the explicit short-root type-F₄ carrier over ℤ, built from the 26-dimensional short-root representation, and TauCeti.F4ShortRoot.points A realizes its A-valued points as a subgroup of GL₂₆(A). This file supplies the homomorphism induced by an arbitrary homomorphism of value rings and assembles these point groups into a functor on commutative ℤ-algebras.

The induced map is entrywise and preserves the two pinned families:

f (x_k(u)) = x_k(f(u)),        f (t(s)) = t(f ∘ s).

The quotient of the ambient general-linear coordinate Hopf algebra by the short-root carrier's defining ideal represents this functor. Nothing here asserts reductivity, maximality of the weight torus, or an identification of the carrier's root datum.

Main declarations

• TauCeti.F4ShortRoot.pointsPresentation: the generic integral presentation of the named points.
• TauCeti.F4ShortRoot.pointsMap: the map on carrier points induced by a ring homomorphism.
• TauCeti.F4ShortRoot.pointsFunctor: the group-valued functor of points.
• TauCeti.F4ShortRoot.pointsMulEquiv: the pointwise representing isomorphism.
• TauCeti.F4ShortRoot.pointsFunctorNatIso: the natural representing isomorphism.

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--2.

noncomputable def TauCeti.F4ShortRoot.pointsPresentation (A : Type v) [CommRing A] : GeneralLinear.IntegralPointsPresentation 26 definingIdeal A

The named short-root carrier points, packaged as an integral Hopf-ideal presentation.

Equations

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

noncomputable def TauCeti.F4ShortRoot.pointsMap {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) : ↥(points A) →* ↥(points B)

The map on the points of the short-root type-F₄ carrier induced by a homomorphism of value rings. It is the entrywise map on GL₂₆, restricted to the subgroup cut out by the carrier's defining ideal.

Equations

• TauCeti.F4ShortRoot.pointsMap f = (TauCeti.F4ShortRoot.pointsPresentation A).map (TauCeti.F4ShortRoot.pointsPresentation B) f

@[simp]

theorem TauCeti.F4ShortRoot.coe_pointsMap {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (g : ↥(points A)) : ↑((pointsMap f) g) = (Matrix.GeneralLinearGroup.map f) ↑g

The induced map on short-root type-F₄ carrier points is the entrywise map.

theorem TauCeti.F4ShortRoot.coe_pointsMap_apply {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (g : ↥(points A)) (i j : Fin 26) : ↑↑((pointsMap f) g) i j = f (↑↑g i j)

Entrywise, the induced map applies the homomorphism of value rings to each matrix entry.

@[simp]

theorem TauCeti.F4ShortRoot.pointsMap_id {A : Type v} [CommRing A] : pointsMap (RingHom.id A) = MonoidHom.id ↥(points A)

The identity homomorphism induces the identity on short-root type-F₄ carrier points.

@[simp]

theorem TauCeti.F4ShortRoot.pointsMap_comp {A : Type v} {B : Type v'} [CommRing A] [CommRing B] {C : Type u_1} [CommRing C] (f : A →+* B) (g : B →+* C) : pointsMap (g.comp f) = (pointsMap g).comp (pointsMap f)

The induced maps on short-root type-F₄ carrier points compose.

theorem TauCeti.F4ShortRoot.pointsMap_injective {A : Type v} {B : Type v'} [CommRing A] [CommRing B] {f : A →+* B} (hf : Function.Injective ⇑f) : Function.Injective ⇑(pointsMap f)

An injective homomorphism of value rings induces an injective map on the points of the short-root type-F₄ carrier.

@[simp]

theorem TauCeti.F4ShortRoot.pointsMap_rootSubgroupPoints {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) : (pointsMap 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.F4ShortRoot.pointsMap_weightTorusPoints {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (s : Fin 4 → Aˣ) : (pointsMap f) ((weightTorusPoints A) s) = (weightTorusPoints B) fun (i : Fin 4) => (Units.map ↑f) (s i)

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

The functor of points

noncomputable def TauCeti.F4ShortRoot.pointsFunctor : CategoryTheory.Functor (CommAlgCat ℤ) GrpCat

The group-valued functor of points of the short-root type-F₄ carrier.

Equations

• TauCeti.F4ShortRoot.pointsFunctor = TauCeti.GeneralLinear.IntegralPointsPresentation.functor TauCeti.F4ShortRoot.pointsPresentation

@[simp]

theorem TauCeti.F4ShortRoot.pointsFunctor_obj (A : CommAlgCat ℤ) : pointsFunctor.obj A = ↧↥(points ↑A)

The object part of the short-root carrier's points functor is its named point group.

@[simp]

theorem TauCeti.F4ShortRoot.pointsFunctor_map {A B : CommAlgCat ℤ} (f : A ⟶ B) : pointsFunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (pointsMap ↑(CommAlgCat.Hom.hom f))) (CategoryTheory.eqToHom ⋯))

The morphism part of the short-root carrier's points functor is the induced entrywise map.

noncomputable def TauCeti.F4ShortRoot.pointsMulEquiv (A : CommAlgCat ℤ) : ↑(HopfAlgebra.points A) ≃* ↥(points ↑A)

The points of the quotient coordinate Hopf algebra are the named short-root carrier points.

Equations

• TauCeti.F4ShortRoot.pointsMulEquiv A = (TauCeti.F4ShortRoot.pointsPresentation ↑A).mulEquiv

@[simp]

theorem TauCeti.F4ShortRoot.coe_pointsMulEquiv_apply (A : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points A)) : ↑((pointsMulEquiv A) q) = (GeneralLinear.pointsMulEquiv 26) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra ℤ 26) definingIdeal A)) q)

A quotient point, read through pointsMulEquiv, is its ambient point viewed as an invertible matrix.

@[simp]

theorem TauCeti.F4ShortRoot.quotientPointsHom_pointsMulEquiv_symm (A : CommAlgCat ℤ) (g : ↥(points ↑A)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra ℤ 26) definingIdeal A)) ((pointsMulEquiv A).symm g) = (GeneralLinear.pointsMulEquiv 26).symm ↑g

Including the ambient Hopf-algebra point underlying the inverse of pointsMulEquiv recovers the point corresponding to the underlying matrix.

@[simp]

theorem TauCeti.F4ShortRoot.pointsMulEquiv_mapPoints {A B : CommAlgCat ℤ} (f : A ⟶ B) (q : ↑(HopfAlgebra.points A)) : (pointsMulEquiv B) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) q) = (pointsMap ↑(CommAlgCat.Hom.hom f)) ((pointsMulEquiv A) q)

The pointwise identification with quotient Hopf-algebra points is natural in the value algebra.

noncomputable def TauCeti.F4ShortRoot.pointsFunctorNatIso : HopfAlgebra.pointsFunctor ≅ pointsFunctor

The quotient coordinate Hopf algebra represents the points functor of the type-F₄ short-root carrier.

Equations

• TauCeti.F4ShortRoot.pointsFunctorNatIso = TauCeti.GeneralLinear.IntegralPointsPresentation.natIso TauCeti.F4ShortRoot.pointsPresentation

@[simp]

theorem TauCeti.F4ShortRoot.pointsFunctorNatIso_hom_app_apply (A : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom (pointsFunctorNatIso.hom.app A)) q) = (pointsMulEquiv A) q

The forward component of the representing natural isomorphism is the pointwise identification.

@[simp]

theorem TauCeti.F4ShortRoot.pointsFunctorNatIso_inv_app_apply (A : CommAlgCat ℤ) (g : ↥(points ↑A)) : (CategoryTheory.ConcreteCategory.hom (pointsFunctorNatIso.inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g) = (pointsMulEquiv A).symm g

The inverse component of the representing natural isomorphism is the inverse pointwise identification.