Frobenius on split tori

Let A be a commutative ring of exponential characteristic p. On the A-valued points of an integral split torus, post-composition with the n-fold Frobenius of A agrees with the group-scheme power endomorphism of exponent p ^ n. Thus the coordinate-free Frobenius on convolution points, the functorial action on scheme-valued points, and coordinatewise powering all describe the same endomorphism.

This comparison is the bridge needed to read the square of a special isogeny on a split maximal torus as Frobenius rather than merely as an abstract power map.

Main results

• TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_mapValue_iterateFrobenius: under the coordinate-algebra comparison, functoriality along Frobenius is the existing convolution-point Frobenius.
• TauCeti.SplitTorus.mapValue_iterateFrobenius_eq_comp_powEnd: on scheme-valued points, the n-fold Frobenius is composition with the power endomorphism of exponent p ^ n.
• TauCeti.SplitTorus.mapValue_iterateFrobenius_eq_self_iff: a point is fixed by the iterated Frobenius exactly when each torus coordinate is fixed by the corresponding power map.

References

• J. S. Milne, Algebraic Groups (2017), Sections 12 and 13.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), Section 11.

theorem TauCeti.SplitTorus.mapValue_iterateFrobenius_eq_comp_powEnd {A sigma : Type} [CommRing A] [Finite sigma] (p n : ℕ) [ExpChar A p] (q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (groupScheme ℤ sigma).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (iterateFrobenius A p n).toIntAlgHom.toRingHom)) (AlgebraicGeometry.Spec ↧ℤ)) q = CategoryTheory.CategoryStruct.comp q (powEnd ℤ sigma ↑(p ^ n)).hom.hom

The iterated Frobenius on the points of an integral split torus is its power endomorphism. Precomposing an A-valued point by the n-fold Frobenius of A agrees with postcomposing it by the split-torus power map of exponent p ^ n.

theorem TauCeti.SplitTorus.mapValue_frobenius_eq_comp_powEnd {A sigma : Type} [CommRing A] [Finite sigma] (p : ℕ) [ExpChar A p] (q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (groupScheme ℤ sigma).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (frobenius A p).toIntAlgHom.toRingHom)) (AlgebraicGeometry.Spec ↧ℤ)) q = CategoryTheory.CategoryStruct.comp q (powEnd ℤ sigma ↑p).hom.hom

The ordinary Frobenius on the points of an integral split torus is its power endomorphism of exponent p.

theorem TauCeti.SplitTorus.mapValue_iterateFrobenius_eq_self_iff {A sigma : Type} [CommRing A] [Finite sigma] (p n : ℕ) [ExpChar A p] (q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (groupScheme ℤ sigma).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (iterateFrobenius A p n).toIntAlgHom.toRingHom)) (AlgebraicGeometry.Spec ↧ℤ)) q = q ↔ ∀ (i : sigma), schemePointsMulEquiv q i ^ ↑(p ^ n) = schemePointsMulEquiv q i

An A-valued point of an integral split torus is fixed by the n-fold Frobenius exactly when each of its coordinates is fixed by the power map of exponent p ^ n.