The Frobenius endomorphism of a commutative bialgebra over a finite field

Let S be a commutative bialgebra over a finite field K. Its algebra map is injective, so the #K-power map is a ring endomorphism of S and of its tensor square. On the tensor square that endomorphism is the tensor square of the one on S, so it respects comultiplication, and the counit lands in K, where the #K-power map is the identity. The #K-power map is therefore a morphism of bialgebras.

Contravariantly this is the Frobenius endomorphism of the affine monoid scheme represented by S. When S is a Hopf algebra, this is an affine group-scheme endomorphism. On points over a K-algebra, it raises every coordinate to its #K-th power.

Main declarations

• TauCeti.frobeniusBialgHom: the #K-power map as a bialgebra endomorphism.

References

• Mathlib's FiniteField.frobeniusAlgHom, the finite-field Frobenius algebra endomorphism.

noncomputable def TauCeti.frobeniusBialgHom (K : Type u_1) [Field K] [Fintype K] (S : Type u) [CommSemiring S] [Bialgebra K S] : S →ₐc[K] S

The #K-power map of a commutative bialgebra over a finite field, as a bialgebra endomorphism.

Equations

• TauCeti.frobeniusBialgHom K S = BialgHom.ofAlgHom (FiniteField.frobeniusAlgHom K S) ⋯ ⋯

@[simp]

theorem TauCeti.frobeniusBialgHom_apply (K : Type u_1) [Field K] [Fintype K] (S : Type u) [CommSemiring S] [Bialgebra K S] (x : S) : (frobeniusBialgHom K S) x = x ^ Fintype.card K

The Frobenius bialgebra endomorphism raises an element to its #K-th power.