Frobenius on tensor products #
The tensor product of Frobenius endomorphisms agrees with Frobenius on the tensor product over a finite field. This identity makes Frobenius commute with bialgebra comultiplication, allowing the algebra endomorphism to be promoted to a bialgebra endomorphism.
References #
- Mathlib's
FiniteField.frobeniusAlgHom, the finite-field Frobenius algebra endomorphism.
@[simp]
theorem
TauCeti.tensorProductMap_frobeniusAlgHom_pow_apply
(K : Type u)
(S : Type v)
(T : Type w)
[Field K]
[Fintype K]
[CommSemiring S]
[CommSemiring T]
[Algebra K S]
[Algebra K T]
(n : ℕ)
(z : TensorProduct K S T)
:
let this := (algebraMap K S).commSemiringToCommRing;
let this_1 := (algebraMap K T).commSemiringToCommRing;
(Algebra.TensorProduct.map (FiniteField.frobeniusAlgHom K S ^ n) (FiniteField.frobeniusAlgHom K T ^ n)) z = z ^ Fintype.card K ^ n
The tensor product of the nth Frobenius iterates is the (#K) ^ n-power map of the tensor
product over the finite field K.