Iterated Frobenius on units

Let A be a commutative semiring of exponential characteristic p. The p ^ n-power Frobenius iterateFrobenius A p n is a ring homomorphism, so it acts on the units of A through Units.map, and that action is the p ^ n-th power map. This file records that, pointwise and coordinatewise along a family, because the coordinatewise form is what a split torus of a Chevalley carrier meets when its Frobenius is computed on weight-torus points.

Nothing here is about the fixed locus of the Frobenius; for the subring and subfield it fixes, see TauCeti.Algebra.CharP.Frobenius.Fixed.

Main results

• TauCeti.map_iterateFrobenius_unit_eq_pow: Units.map (iterateFrobenius A p n) u = u ^ p ^ n.
• TauCeti.map_iterateFrobenius_units_eq_pow: the same coordinatewise along a family of units.

@[simp]

theorem TauCeti.map_iterateFrobenius_unit_eq_pow (A : Type u_1) [CommSemiring A] (p n : ℕ) [ExpChar A p] (u : Aˣ) : (Units.map ↑(iterateFrobenius A p n)) u = u ^ p ^ n

The p ^ n-power Frobenius acts on a unit as the p ^ n-th power map.

theorem TauCeti.map_iterateFrobenius_units_eq_pow (A : Type u_1) [CommSemiring A] (p n : ℕ) [ExpChar A p] {ι : Type u_2} (s : ι → Aˣ) : (fun (i : ι) => (Units.map ↑(iterateFrobenius A p n)) (s i)) = s ^ p ^ n

Applying the p ^ n-power Frobenius to each coordinate of a family of units raises the family to its p ^ n-th power. This is the coordinatewise form of TauCeti.map_iterateFrobenius_unit_eq_pow, which is the shape a torus calculation meets it in.