Frobenius on the short-root type-F4 prime-field carrier

This file defines the Frobenius endomorphisms of the carrier's matrix-valued points. The finite-field Frobenius algebra homomorphism exists for every ZMod 2-algebra, including the zero ring, so the coefficient formula and all functor laws need no separate characteristic hypothesis. The coordinate and group-scheme Frobenius maps are also exposed as frobeniusCoordinateMap and frobeniusHom.

Main declarations

• PrimeField.frobenius is the point map induced by an iterate of the finite-field Frobenius.
• PrimeField.coe_frobenius_apply is its entrywise 2 ^ m-power formula.
• PrimeField.frobenius_zero, PrimeField.frobenius_add, and PrimeField.frobenius_pow are the iteration laws inherited from point functoriality.
• PrimeField.frobenius_rootSubgroupPoints and PrimeField.frobenius_weightTorusPoints describe the action on the pinned generators.
• PrimeField.frobenius_eq_self_iff and PrimeField.map_subtype_fixedSubgroup_frobenius_eq say which points it fixes, and identify the fixed subgroup with the carrier's points over the Frobenius-fixed subalgebra. No finiteness of either side is asserted.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 11.3.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• The corresponding integral short-root construction in TauCeti.Algebra.Lie.F4.ShortRoot.Frobenius.

noncomputable def TauCeti.F4ShortRoot.PrimeField.frobenius (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] : ↥(points A) →* ↥(points A)

The 2 ^ m-power Frobenius endomorphism of the carrier over 𝔽₂, the map on points induced by the iterated Frobenius of the value algebra.

For m positive this is the 2 ^ m-power Frobenius of the carrier's points; at m = 0 it is the identity.

Equations

• TauCeti.F4ShortRoot.PrimeField.frobenius m A = TauCeti.F4ShortRoot.PrimeField.pointsMap (FiniteField.frobeniusAlgHom (ZMod 2) A ^ m)

theorem TauCeti.F4ShortRoot.PrimeField.coe_frobenius (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (g : ↥(points A)) : ↑((frobenius m A) g) = (Matrix.GeneralLinearGroup.map ↑(FiniteField.frobeniusAlgHom (ZMod 2) A ^ m)) ↑g

The Frobenius endomorphism of the carrier over 𝔽₂ maps matrices entrywise by the finite-field Frobenius algebra homomorphism.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.coe_frobenius_apply (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (g : ↥(points A)) (i j : Fin 26) : ↑↑((frobenius m A) g) i j = ↑↑g i j ^ 2 ^ m

Entrywise, the Frobenius endomorphism of the carrier over 𝔽₂ raises each matrix coefficient to its 2 ^ m-th power.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.frobenius_zero (A : Type v) [CommRing A] [Algebra (ZMod 2) A] : frobenius 0 A = MonoidHom.id ↥(points A)

The zeroth Frobenius iterate is the identity on the carrier's point group.

theorem TauCeti.F4ShortRoot.PrimeField.frobenius_add (m k : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] : frobenius (m + k) A = (frobenius m A).comp (frobenius k A)

Frobenius iterates add under composition on the carrier's point group.

theorem TauCeti.F4ShortRoot.PrimeField.frobenius_pow (k m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] : (have this := frobenius k A; this) ^ m = frobenius (k * m) A

Frobenius exponents multiply under taking powers: the m-th power of the 2 ^ k-power Frobenius of the carrier, in the endomorphism monoid of its points, is its 2 ^ (k * m)-power Frobenius.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.frobenius_rootSubgroupPoints (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) : (frobenius m A) ((rootSubgroupPoints k A) u) = (rootSubgroupPoints k A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ 2 ^ m))

Frobenius raises the parameter of every numbered simple root subgroup to its 2 ^ m-th power.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.frobenius_weightTorusPoints (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 → Aˣ) : (frobenius m A) ((weightTorusPoints A) s) = (weightTorusPoints A) (s ^ 2 ^ m)

Frobenius raises every coordinate of the pinned split weight torus to its 2 ^ m-th power.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.frobenius_eq_self_iff (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] (g : ↥(points A)) : (frobenius m A) g = g ↔ ∀ (i j : Fin 26), ↑↑g i j ∈ FiniteField.frobeniusFixedSubalgebra (ZMod 2) A m

A point of the carrier over 𝔽₂ is fixed by the 2 ^ m-power Frobenius exactly when all of its matrix entries lie in the Frobenius-fixed subalgebra.

theorem TauCeti.F4ShortRoot.PrimeField.map_subtype_fixedSubgroup_frobenius_eq (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 2) A] : Subgroup.map (points A).subtype (fixedSubgroup (frobenius m A)) = Subgroup.map (Matrix.GeneralLinearGroup.map ↑(FiniteField.frobeniusFixedSubalgebra (ZMod 2) A m).val) (points ↥(FiniteField.frobeniusFixedSubalgebra (ZMod 2) A m))

The Frobenius-fixed points of the carrier over 𝔽₂ are its points over the Frobenius-fixed subalgebra. For A an algebraic closure of 𝔽₂ and 0 < m that subalgebra is the field of 2 ^ m elements, but no finiteness of either side is asserted here.

Frobenius of the carrier group scheme

noncomputable def TauCeti.F4ShortRoot.PrimeField.frobeniusCoordinateMap : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator) ⟶ CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator)

The squaring Frobenius of the carrier coordinate Hopf algebra.

Equations

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

theorem TauCeti.F4ShortRoot.PrimeField.frobeniusCoordinateMap_def : frobeniusCoordinateMap = CommHopfAlgCat.ofHom (frobeniusBialgHom (ZMod 2) ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator)))

The coordinate Frobenius is the canonical Frobenius bialgebra homomorphism.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.frobeniusCoordinateMap_apply (x : ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal generator))) : (CommHopfAlgCat.Hom.hom frobeniusCoordinateMap) x = x ^ 2

The Frobenius coordinate morphism squares each function on the carrier.

theorem TauCeti.F4ShortRoot.PrimeField.coordinatePointsEquiv_map_frobeniusCoordinateMap (A : Type u_1) [CommRing A] [Algebra (ZMod 2) A] (q : ↑(HopfAlgebra.points ↧A)) : (coordinatePointsEquiv A) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom frobeniusCoordinateMap)) q) = (frobenius 1 A) ((coordinatePointsEquiv A) q)

Evaluating the coordinate Frobenius is the named Frobenius on matrix-valued points.

noncomputable def TauCeti.F4ShortRoot.PrimeField.frobeniusHom : groupScheme ⟶ groupScheme

The characteristic-two Frobenius of the explicit F4 carrier group scheme.

Equations

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

theorem TauCeti.F4ShortRoot.PrimeField.frobeniusHom_eq_map_frobeniusCoordinateMap : frobeniusHom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧(ZMod 2)).map frobeniusCoordinateMap.op) (CategoryTheory.eqToHom ⋯))

The carrier Frobenius is represented by its coordinate Frobenius morphism.