Reduced Artin–Schreier representatives at a place

In characteristic p, a function u defines the same Artin–Schreier extension as u - (w ^ p - w). At a place with perfect residue field, such a representative can be chosen integral or with pole order prime to p. This is the local input for computing ramification and the different of Artin–Schreier extensions.

exists_ord_sub_pow_sub_self_gt_of_dvd_ord cancels a leading pole term whose order is divisible by the exponent, by lifting a root of its residue. Iteration gives exists_reduced_artinSchreier_representative. The one-step result only needs surjectivity of the power map on the residue field; the iteration uses additivity of Frobenius. Neither result requires completeness, an exact constant field, or a function-field hypothesis.

A prime-to-p pole cannot be improved by any Artin–Schreier substitution, even with an imperfect residue field. TauCeti.ne_pow_sub_self_of_exists_reduced_artinSchreier_pole proves that a class with such a representative is nontrivial. TauCeti.ord_sub_pow_sub_self_le_of_ord_neg_of_not_dvd records this maximality, and TauCeti.ord_reduced_artinSchreier_representative_eq gives uniqueness. The integral alternative includes the zero representative, so no statement uses the junk value ord_P 0 = 0 as a positive order of vanishing.

References

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

theorem TauCeti.Place.exists_ord_sub_pow_sub_self_gt_of_dvd_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {n : ℕ} (hn : 1 < n) (hpow : Function.Surjective fun (a : P.ResidueField) => a ^ n) {u : F} (hu : P.ord u < 0) (hdiv : ↑n ∣ P.ord u) : ∃ (w : F), P.ord u < P.ord (u - (w ^ n - w))

A pole of order divisible by n > 1 can be improved by a substitution u ↦ u - (w ^ n - w) if the n-th power map of the residue field is surjective. This cancellation step does not need a characteristic hypothesis.

theorem TauCeti.Place.exists_reduced_artinSchreier_representative {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] [PerfectField P.ResidueField] (u : F) : ∃ (w : F), u - (w ^ p - w) ∈ P.integers ∨ P.ord (u - (w ^ p - w)) < 0 ∧ ¬↑p ∣ P.ord (u - (w ^ p - w))

Over a perfect residue field in characteristic p, every Artin–Schreier class has an integral representative or a representative with negative order not divisible by p. The substitution lies in F itself; no completion is used.