Orders of Frobenius powers under a discrete valuation

Let F be a field of exponential characteristic p, and let v : Valuation F ℤᵐ⁰. Every element in the image of the n-fold Frobenius has order under v divisible by p ^ n: if z = y ^ (p ^ n), then

ord_v(z) = p ^ n * ord_v(y).

Consequently, an element whose order under a discrete valuation is not divisible by p ^ n cannot lie in the image of the n-fold Frobenius. Applied to the valuation of a function-field place, this is the valuation-theoretic input to the separating-element criterion in positive characteristic.

Main results

• Valuation.ord_iterateFrobenius: the order of an iterated Frobenius image.
• Valuation.natCast_pow_dvd_ord_of_mem_fieldRange_iterateFrobenius: membership in the p ^ n-power subfield forces divisibility of the order by p ^ n.
• Valuation.not_mem_fieldRange_iterateFrobenius_of_not_natCast_pow_dvd_ord: the contrapositive, eliminating membership in the p ^ n-power subfield.

References

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 3.10.2.

@[simp]

theorem Valuation.ord_iterateFrobenius {F : Type u} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (p : ℕ) [ExpChar F p] (n : ℕ) (z : F) : v.ord ((iterateFrobenius F p n) z) = ↑p ^ n * v.ord z

The order under a discrete valuation of an n-fold Frobenius image is multiplied by p ^ n.

theorem Valuation.natCast_pow_dvd_ord_of_mem_fieldRange_iterateFrobenius {F : Type u} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (p : ℕ) [ExpChar F p] (n : ℕ) {z : F} (hz : z ∈ (iterateFrobenius F p n).fieldRange) : ↑p ^ n ∣ v.ord z

Membership in the image of the n-fold Frobenius forces the order under every discrete valuation to be divisible by p ^ n.

theorem Valuation.not_mem_fieldRange_iterateFrobenius_of_not_natCast_pow_dvd_ord {F : Type u} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (p : ℕ) [ExpChar F p] (n : ℕ) {z : F} (hz : ¬↑p ^ n ∣ v.ord z) : z ∉ (iterateFrobenius F p n).fieldRange

An element whose order under a discrete valuation is not divisible by p ^ n does not lie in the image of the n-fold Frobenius.