Frobenius on convolution points

Let H be a bialgebra over ℤ and let A be a commutative ring of exponential characteristic p. Post-composition with Mathlib's iterateFrobenius A p n sends an A-valued point f : H →ₐ[ℤ] A to the point h ↦ f(h) ^ (p ^ n). Functoriality of convolution makes this a monoid endomorphism of the points represented by H. When H is a Hopf algebra, these convolution points form a group. If H is also commutative, they are the points of the affine group scheme Spec H.

This is the field-endomorphism part of the pinned Chevalley--Demazure interface: once a pinned group's integral coordinate Hopf algebra is constructed, iterateFrobeniusPoints p n supplies the p ^ n-power endomorphism on its points over an algebraic closure. The construction itself needs neither algebraic closedness nor finite type.

Main definitions and results

• TauCeti.Bialgebra.iterateFrobeniusPoints is the induced monoid endomorphism on convolution points.
• TauCeti.Bialgebra.iterateFrobeniusPoints_apply_apply identifies its action with the p ^ n-power map.
• TauCeti.Bialgebra.iterateFrobeniusPoints_zero identifies the zeroth iterate.
• TauCeti.Bialgebra.iterateFrobeniusPoints_add gives the iteration law.
• TauCeti.Bialgebra.mapValue_comp_iterateFrobeniusPoints proves naturality in the value algebra.

Implementation notes

The construction post-composes with Mathlib's iterateFrobenius, whose laws supply every proof here, and reuses Tau Ceti's convolution-valued functor of points. Those laws are equalities of ring homomorphisms, while AlgHom.mapValue consumes ℤ-algebra homomorphisms; the functoriality of RingHom.toIntAlgHom that transports the one into the other lives in TauCeti/Algebra/Algebra/Hom.lean.

noncomputable def TauCeti.Bialgebra.iterateFrobeniusPoints (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : WithConv (H →ₐ[ℤ] A) →* WithConv (H →ₐ[ℤ] A)

The p ^ n-power Frobenius endomorphism on the monoid of A-valued points represented by the integral bialgebra H.

It post-composes a point with the iterated Frobenius of A, regarded as a ℤ-algebra endomorphism. Frobenius is only a ring homomorphism, not an A-algebra homomorphism; regarding it as its canonical ℤ-algebra homomorphism lets AlgHom.mapValue act at base ℤ.

Equations

• TauCeti.Bialgebra.iterateFrobeniusPoints p n = TauCeti.AlgHom.mapValue (iterateFrobenius A p n).toIntAlgHom

theorem TauCeti.Bialgebra.iterateFrobeniusPoints_apply (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (f : WithConv (H →ₐ[ℤ] A)) : (iterateFrobeniusPoints p n) f = WithConv.toConv ((iterateFrobenius A p n).toIntAlgHom.comp f.ofConv)

Frobenius on points is post-composition with the iterated Frobenius of the value algebra.

@[simp]

theorem TauCeti.Bialgebra.iterateFrobeniusPoints_apply_apply (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (f : WithConv (H →ₐ[ℤ] A)) (h : H) : ((iterateFrobeniusPoints p n) f).ofConv h = f.ofConv h ^ p ^ n

Pointwise, the n-fold Frobenius sends an A-valued point f to h ↦ f(h) ^ (p ^ n).

This is the simp-normal form of a value of iterateFrobeniusPoints; iterateFrobeniusPoints_apply is deliberately not a simp lemma, since rewriting with it would leave the left-hand side at the implementation-level iterateFrobenius expression instead.

@[simp]

theorem TauCeti.Bialgebra.iterateFrobeniusPoints_zero (p : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : iterateFrobeniusPoints p 0 = MonoidHom.id (WithConv (H →ₐ[ℤ] A))

The zeroth Frobenius iterate is the identity on points.

theorem TauCeti.Bialgebra.iterateFrobeniusPoints_add (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (m : ℕ) : iterateFrobeniusPoints p (n + m) = (iterateFrobeniusPoints p n).comp (iterateFrobeniusPoints p m)

Frobenius iterates add under composition on the monoid of points.

theorem TauCeti.Bialgebra.mapValue_comp_iterateFrobeniusPoints (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] {B : Type w} [CommRing B] [ExpChar B p] (φ : A →ₐ[ℤ] B) : (AlgHom.mapValue φ).comp (iterateFrobeniusPoints p n) = (iterateFrobeniusPoints p n).comp (AlgHom.mapValue φ)

Naturality of Frobenius on points in the value algebra: Frobenius commutes with every homomorphism φ : A →ₐ[ℤ] B into a value algebra of the same exponential characteristic p, so post-composing a point by φ before or after applying the n-fold Frobenius gives the same point.