Frobenius on the short-root type-G2 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 3-algebra, including the zero ring, so the coefficient formula and all functor laws need no separate characteristic hypothesis. It also records the cubic Frobenius of the carrier itself, as an endomorphism of its coordinate Hopf algebra and of the group scheme, and identifies the induced action on scheme-valued points with the point map at m = 1.

Over an algebraic closure of 𝔽₃, and for 0 < m, the points fixed by the 3 ^ m-power Frobenius are those with entries in the field of 3 ^ m elements, which is how a group of type G₂ over a finite field is cut out of the carrier. The twisted groups of the same diagram need one further ingredient, the length-exchanging special isogeny of characteristic three, whose square is the 3-power Frobenius defined here.

Main declarations

• PrimeField.frobenius is the point map induced by an iterate of the finite-field Frobenius.
• PrimeField.coe_frobenius_apply is its entrywise 3 ^ 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.
• PrimeField.frobeniusCoordinateMap and PrimeField.frobeniusHom are the cubic Frobenius of the carrier's coordinate Hopf algebra and of the carrier group scheme, with PrimeField.map_carrierGenericMatrix_frobeniusCoordinateMap its action on the universal point and PrimeField.schemePointsMulEquiv_comp_frobeniusHom identifying the induced action on scheme-valued points with PrimeField.frobenius 1.

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.

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

The 3 ^ 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 3 ^ m-power Frobenius of the carrier's points; at m = 0 it is the identity.

Equations

• TauCeti.G2ShortRoot.PrimeField.frobenius m A = TauCeti.G2ShortRoot.PrimeField.pointsMap (FiniteField.frobeniusAlgHom (ZMod 3) A ^ m)

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

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

@[simp]

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

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

@[simp]

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

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

theorem TauCeti.G2ShortRoot.PrimeField.frobenius_add (m k : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 3) 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.G2ShortRoot.PrimeField.frobenius_pow (k m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 3) A] : (have this := frobenius k A; this) ^ m = frobenius (k * m) A

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

theorem TauCeti.G2ShortRoot.PrimeField.map_subtype_fixedSubgroup_frobenius_eq (m : ℕ) (A : Type v) [CommRing A] [Algebra (ZMod 3) A] : Subgroup.map (points A).subtype (fixedSubgroup (frobenius m A)) = Subgroup.map (Matrix.GeneralLinearGroup.map ↑(FiniteField.frobeniusFixedSubalgebra (ZMod 3) A m).val) (points ↥(FiniteField.frobeniusFixedSubalgebra (ZMod 3) 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 3 ^ m elements, but no finiteness of either side is asserted here.

Frobenius on the coordinate Hopf algebra and on the carrier

noncomputable def TauCeti.G2ShortRoot.PrimeField.frobeniusCoordinateMap : carrierAlgebra ⟶ carrierAlgebra

The cubic Frobenius endomorphism of the carrier coordinate Hopf algebra, the 3-power map of the coordinate Hopf algebra over 𝔽₃.

Equations

• TauCeti.G2ShortRoot.PrimeField.frobeniusCoordinateMap = CommHopfAlgCat.ofHom (TauCeti.frobeniusBialgHom (ZMod 3) ↑TauCeti.G2ShortRoot.PrimeField.carrierAlgebra)

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.frobeniusCoordinateMap_apply (x : ↑carrierAlgebra) : (CommHopfAlgCat.Hom.hom frobeniusCoordinateMap) x = x ^ 3

The Frobenius coordinate map cubes every element of the carrier coordinate Hopf algebra.

theorem TauCeti.G2ShortRoot.PrimeField.map_carrierGenericMatrix_frobeniusCoordinateMap : carrierGenericMatrix.map ⇑↑(CommHopfAlgCat.Hom.hom frobeniusCoordinateMap) = carrierGenericMatrix.map fun (x : ↑carrierAlgebra) => x ^ 3

The Frobenius coordinate map cubes the universal point of the carrier entrywise.

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

The cubic Frobenius as an endomorphism of the short-root type-G₂ carrier over 𝔽₃.

Equations

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

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

The carrier Frobenius is the scheme morphism induced by frobeniusCoordinateMap.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_frobeniusHom (B : Type) [CommRing B] [Algebra (ZMod 3) B] (p : (AlgebraicGeometry.Spec ↧B).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ groupScheme.X) : (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp p frobeniusHom.hom.hom) = (frobenius 1 B) ((schemePointsMulEquiv B) p)

The action induced by frobeniusHom on scheme-valued carrier points is the cubic Frobenius frobenius 1 of matrix-valued points.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_rootSubgroup_comp_frobeniusHom (k : Fin 2 ⊕ Fin 2) (B : Type) [CommRing B] [Algebra (ZMod 3) B] (p : (AlgebraicGeometry.Spec ↧B).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ (AdditiveGroup.groupScheme (ZMod 3)).X) : (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (rootSubgroup k).hom.hom frobeniusHom.hom.hom)) = (rootSubgroupPoints k B) (Multiplicative.ofAdd (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv B) p) ^ 3))

On scheme-valued points, composing a numbered root subgroup with the carrier Frobenius cubes its parameter.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.schemePointsMulEquiv_comp_weightTorus_comp_frobeniusHom (B : Type) [CommRing B] [Algebra (ZMod 3) B] (p : (AlgebraicGeometry.Spec ↧B).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ (SplitTorus.groupScheme (ZMod 3) (Fin 2)).X) : (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp weightTorus.hom.hom frobeniusHom.hom.hom)) = (weightTorusPoints B) (SplitTorus.schemePointsMulEquiv p ^ 3)

On scheme-valued points, composing the weight torus with the carrier Frobenius cubes every torus coordinate.