The standard representation of the short-root F₄ prime-field carrier

The scalar extension of the short-root carrier over 𝔽₂ has a faithful representation on column vectors of length twenty-six. Restriction to its weight torus has twenty-four distinct nonzero weights and a two-dimensional zero-weight space. Every invariant submodule is stable under the corresponding weight projections, including over finite fields: characters, rather than rational torus points, separate the weights.

The zero-weight projection retains both coordinates together. There is no assertion that either zero-weight coordinate line is invariant, nor that the standard representation is simple. These projections and the numbered root actions provide the invariant-subspace calculations needed to study simplicity and the unipotent radical.

Here the coordinate algebra is the scalar extension of the prime-field carrier itself; it is also the subgroup generated after scalar extension, by TauCeti.F4ShortRoot.PrimeField.baseChangeDefiningIdeal_eq_generatedDefiningIdeal. The carrier is not identified with the pinned simply connected group scheme of type F₄; transfer to that group requires such an identification.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII.

The corestriction construction follows TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generated.StandardComodule; the coefficient and matrix-point interface follows TauCeti.Algebra.Lie.E6.DoubledMinuscule.StandardComodule.

noncomputable def TauCeti.F4ShortRoot.PrimeField.coordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : GeneralLinear.coordinateHopfAlgebra k 26 ⟶ coordinateHopfAlgebra k

The coordinate morphism of the carrier's inclusion in GL₂₆ after scalar extension.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.F4ShortRoot.PrimeField.coordinateMap_def (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : coordinateMap k = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) definingIdeal))

The carrier coordinate morphism is the scalar extension of its quotient morphism, transported along the general-linear coordinate identification.

theorem TauCeti.F4ShortRoot.PrimeField.coordinateMap_surjective (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (coordinateMap k))

The standard coordinate morphism is surjective, so the represented inclusion is closed.

noncomputable def TauCeti.F4ShortRoot.PrimeField.generatorCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : coordinateHopfAlgebra k ⟶ CommHopfAlgCat.baseChange (generatorCodomain j)

A reduced generator factored through the carrier, then extended to k.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.coordinateMap_comp_generatorCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : CategoryTheory.CategoryStruct.comp (coordinateMap k) (generatorCoordinateMap k j) = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).inv (CommHopfAlgCat.baseChangeMap (generator j))

Factoring a generator through the carrier does not alter its ambient coordinate map.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.coordinateMap_comp_generatorCoordinateMap_assoc (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) {Z : CommHopfAlgCat k} (h : CommHopfAlgCat.baseChange (generatorCodomain j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coordinateMap k) (CategoryTheory.CategoryStruct.comp (generatorCoordinateMap k j) h) = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (generator j)) h)

Factoring a generator through the carrier does not alter its ambient coordinate map.

noncomputable def TauCeti.F4ShortRoot.PrimeField.weightTorusCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : coordinateHopfAlgebra k ⟶ (DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (Fin 4))).obj

Restriction of functions on the carrier to its scalar-extended weight torus.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.coordinateMap_comp_weightTorusCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : CategoryTheory.CategoryStruct.comp (coordinateMap k) (weightTorusCoordinateMap k) = GeneralLinear.weightTorusBaseChangeCoordinateMap (ZMod 2) k DynkinType.f4ShortRootWeight

The carrier weight torus recovers the prescribed twenty-six weights in the ambient group.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.coordinateMap_comp_weightTorusCoordinateMap_assoc (k : Type u) [CommRing k] [Algebra (ZMod 2) k] {Z : CommHopfAlgCat k} (h : ↧(MonoidAlgebra k ↑(SplitTorus.characterGroup (Fin 4))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coordinateMap k) (CategoryTheory.CategoryStruct.comp (weightTorusCoordinateMap k) h) = CategoryTheory.CategoryStruct.comp (GeneralLinear.weightTorusBaseChangeCoordinateMap (ZMod 2) k DynkinType.f4ShortRootWeight) h

The carrier weight torus recovers the prescribed twenty-six weights in the ambient group.

@[instance_reducible]

noncomputable def TauCeti.F4ShortRoot.PrimeField.standardComodule (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : Comodule k (↑(coordinateHopfAlgebra k)) (Fin 26 → k)

The standard right comodule of the scalar-extended short-root carrier on k²⁶.

Equations

• TauCeti.F4ShortRoot.PrimeField.standardComodule k = TauCeti.GeneralLinear.corestrictStandardComodule k 26 (CommHopfAlgCat.Hom.hom (TauCeti.F4ShortRoot.PrimeField.coordinateMap k))

theorem TauCeti.F4ShortRoot.PrimeField.isFaithful_standardComodule (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : Comodule.IsFaithful

The standard representation is faithful in the scheme-theoretic sense.

theorem TauCeti.F4ShortRoot.PrimeField.coefficientMatrix_basisFun (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (a b : Fin 26) : Comodule.coefficientMatrix (Pi.basisFun k (Fin 26)) a b = (CommHopfAlgCat.Hom.hom (coordinateMap k)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv k 26) ((GeneralLinear.coordinateRingMap k 26) (MvPolynomial.X (a, b))))

The coefficient matrix consists of the ambient matrix coordinates restricted to the carrier.

noncomputable def TauCeti.F4ShortRoot.PrimeField.specializedPointsMulEquiv (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : ↑(HopfAlgebra.points ↧k) ≃* ↥(points k)

Base-valued points of the scalar-extended coordinate algebra are the existing matrix-valued points of the prime-field carrier.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.pointToGeneralLinear_specializedPointsMulEquiv (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (q : ↑(HopfAlgebra.points ↧k)) : GeneralLinear.pointToGeneralLinear 26 (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (coordinateMap k)))) = ↑((specializedPointsMulEquiv k) q)

The point equivalence evaluates the same matrix coordinates as the carrier's standard representation.

theorem TauCeti.F4ShortRoot.PrimeField.points_mulVec_mem (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (N : Subcomodule k (↑(coordinateHopfAlgebra k)) (Fin 26 → k)) (g : ↥(points k)) {v : Fin 26 → k} (hv : v ∈ N) : (↑↑g).mulVec v ∈ N

Every subcomodule of the standard representation is stable under the carrier's concrete matrix-valued points, in particular under its positive and negative simple root subgroups.

theorem TauCeti.F4ShortRoot.PrimeField.torusCorestrict_eq_ofWeights (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : Comodule.Corestrict (CommHopfAlgCat.Hom.hom (weightTorusCoordinateMap k)).toCoalgHom = Comodule.ofWeights (Pi.basisFun k (Fin 26)) fun (a : Fin 26) => SplitTorus.weightCharacter (DynkinType.f4ShortRootWeight a)

On the weight torus the standard comodule is diagonal with the short-root weight table. The two occurrences of zero remain two independent basis vectors of the same weight.

theorem TauCeti.F4ShortRoot.PrimeField.weightComponent_mem (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (N : Subcomodule k (↑(coordinateHopfAlgebra k)) (Fin 26 → k)) {v : Fin 26 → k} (hv : v ∈ N) (w : Fin 4 → ℤ) : (fun (a : Fin 26) => if DynkinType.f4ShortRootWeight a = w then v a else 0) ∈ N

A subcomodule is stable under the projection to any torus weight, with all its multiplicities retained.

theorem TauCeti.F4ShortRoot.PrimeField.single_smul_mem (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (N : Subcomodule k (↑(coordinateHopfAlgebra k)) (Fin 26 → k)) {v : Fin 26 → k} (hv : v ∈ N) (a : Fin 26) (ha : DynkinType.f4ShortRootWeight a ≠ 0) : v a • Pi.single a 1 ∈ N

Every nonzero-weight coordinate can be extracted from an invariant submodule vector.

theorem TauCeti.F4ShortRoot.PrimeField.zeroWeightComponent_mem (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (N : Subcomodule k (↑(coordinateHopfAlgebra k)) (Fin 26 → k)) {v : Fin 26 → k} (hv : v ∈ N) : v 12 • Pi.single 12 1 + v 13 • Pi.single 13 1 ∈ N

The zero-weight part of an invariant vector retains both zero-weight coordinates together.