Orders of y ^ n - y at a pole

For a discrete valuation and n > 1, a pole of y is a pole of y ^ n - y of order multiplied by n. Conversely, y ^ n - y cannot have a pole unless y does. Thus an element with negative order not divisible by n is not of the form y ^ n - y.

A prime-to-n pole is maximal among representatives u - (w ^ n - w). In prime characteristic, this also gives uniqueness of the reduced Artin–Schreier pole order.

The pole and maximality results need no characteristic hypothesis. In characteristic p, with n = p, they give the local nontriviality criterion for an Artin–Schreier equation: a pole of order prime to p rules out a root in the base field. TauCeti.ne_pow_sub_self_of_exists_reduced_artinSchreier_pole applies this criterion when a translated representative has such a pole.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.7.8.

theorem Valuation.ord_pow_sub_self_of_ord_neg {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {n : ℕ} (hn : 1 < n) {y : F} (hy : v.ord y < 0) : v.ord (y ^ n - y) = ↑n * v.ord y

At a pole, the power term dominates y ^ n - y when n > 1.

@[simp]

theorem Valuation.ord_pow_sub_self_neg_iff {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {n : ℕ} (hn : 1 < n) (y : F) : v.ord (y ^ n - y) < 0 ↔ v.ord y < 0

For n > 1, y ^ n - y has a pole exactly when y has a pole.

theorem Valuation.ne_pow_sub_self_of_ord_neg_of_not_dvd {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {n : ℕ} (hn : 1 < n) {u : F} (hu : v.ord u < 0) (hdiv : ¬↑n ∣ v.ord u) (y : F) : u ≠ y ^ n - y

A pole whose order is not divisible by n cannot be a value of y ↦ y ^ n - y. For prime n in characteristic n, this proves nontriviality of the Artin–Schreier class.

theorem TauCeti.ne_pow_sub_self_of_exists_reduced_artinSchreier_pole {F : Type u_1} [Field F] {v : Valuation F (WithZero (Multiplicative ℤ))} (p : ℕ) (hp : 1 < p) [ExpChar F p] {u : F} (hpole : ∃ (w₀ : F), v.ord (u - (w₀ ^ p - w₀)) < 0 ∧ ¬↑p ∣ v.ord (u - (w₀ ^ p - w₀))) (w : F) : w ^ p - w ≠ u

A supplied reduced Artin–Schreier pole makes the class of u nontrivial. Only exponential characteristic p > 1 is needed; no perfection or function-field hypothesis is needed.

theorem TauCeti.ord_sub_pow_sub_self_le_of_ord_neg_of_not_dvd {F : Type u_1} [Field F] {v : Valuation F (WithZero (Multiplicative ℤ))} {n : ℕ} (hn : 1 < n) {u : F} (hu : v.ord u < 0) (hdiv : ¬↑n ∣ v.ord u) (w : F) : v.ord (u - (w ^ n - w)) ≤ v.ord u

A negative order not divisible by n > 1 is maximal among all representatives u - (w ^ n - w). No perfection or characteristic hypothesis is needed for this obstruction to improving a pole.

theorem TauCeti.ord_reduced_artinSchreier_representative_eq {F : Type u_1} [Field F] {v : Valuation F (WithZero (Multiplicative ℤ))} (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {u w z : F} (hw : v.ord (u - (w ^ p - w)) < 0) (hwdiv : ¬↑p ∣ v.ord (u - (w ^ p - w))) (hz : v.ord (u - (z ^ p - z)) < 0) (hzdiv : ¬↑p ∣ v.ord (u - (z ^ p - z))) : v.ord (u - (w ^ p - w)) = v.ord (u - (z ^ p - z))

Two representatives of an Artin–Schreier class with prime-to-p poles have the same order. Thus the reduced pole order is independent of the substitution used to obtain it. This uniqueness statement does not need a perfect residue field.