Frobenius on diagonalizable groups #
Let A be a commutative ring of exponential characteristic p. For any finitely generated
commutative group G, applying the n-fold Frobenius of A to an A-valued point of the
diagonalizable group D(G) agrees, under the coordinate-algebra comparison, with the existing
Frobenius endomorphism on convolution points.
Main result #
TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_mapValue_iterateFrobenius: the scheme-point and convolution-point descriptions of iterated Frobenius agree.
References #
- J. S. Milne, Algebraic Groups (2017), Sections 12 and 13.
theorem
TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_mapValue_iterateFrobenius
{A : Type}
[CommRing A]
(p n : ℕ)
[ExpChar A p]
(G : FGCommGrpCat)
(q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (groupScheme ℤ G).X)
:
(groupSchemePointsMulEquiv G)
(CategoryTheory.CategoryStruct.comp
(AlgebraicGeometry.Scheme.Hom.asOver
(AlgebraicGeometry.Spec.map (CommRingCat.ofHom (iterateFrobenius A p n).toIntAlgHom.toRingHom))
(AlgebraicGeometry.Spec ↧ℤ))
q) = (Bialgebra.iterateFrobeniusPoints p n) ((groupSchemePointsMulEquiv G) q)
Under the coordinate-algebra comparison for a diagonalizable group, applying the iterated Frobenius of the value ring is the existing Frobenius endomorphism on convolution points.