Galois displacements at a reduced Artin--Schreier pole

Let F' = F(y) with y ^ p - y = u in characteristic p, and suppose u has a pole of order m prime to p. There is a uniformizer z at every place above that pole which generates F' / F and satisfies

ord (σ z - z) = m + 1 for every nonidentity F-automorphism σ.

This is the local calculation used to evaluate the derivative of the uniformizer's minimal polynomial, and hence the different exponent of an Artin--Schreier extension. The uniformizer is the Bezout product supplied by TauCeti.Place.exists_eq_zpow_mul_adjoin_eq_top_ord_eq_one_of_pow_sub_self_eq_of_gcd_ord_eq_one; its integer exponent on y is nonzero in the prime field. Nonidentity automorphisms translate y by a nonzero prime-field constant, so the valuation of the displacement follows from Valuation.map_add_zpow_sub_zpow. Both positive and negative Bezout exponents are allowed.

References

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

theorem TauCeti.Place.exists_uniformizer_ord_aut_sub_of_artinSchreier_pole (k : Type u_1) {k' : Type u_2} (F : Type u_3) {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] {P' : Place k' F'} (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {y : F'} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) (hcop : (↑p).gcd ((restrict k F P').ord u) = 1) : ∃ (z : F'), F⟮z⟯ = ⊤ ∧ P'.ord z = 1 ∧ ∀ (σ : Gal(F'/F)), σ ≠ 1 → P'.ord (σ z - z) = 1 - (restrict k F P').ord u

At a prime-to-characteristic Artin--Schreier pole, there is a generating uniformizer whose displacement by every nonidentity automorphism has order one greater than the pole order. No hypothesis on perfection of the residue field is needed.