Total ramification at a prime-to-characteristic Artin–Schreier pole

Suppose F' = F(y) and y ^ p - y = u in characteristic p. If u has a pole at P whose order is not divisible by p, every place P' above P is totally ramified: [F' : F] = e(P' ∣ P) = p and ord_{P'} y = ord_P u. The existing total-ramification API then gives relative degree one and uniqueness of the place above P.

The results are stated in the characteristic-independent form y ^ n - y = u, n > 1, and gcd(n, ord_P u) = 1. Taking orders gives n · ord_{P'} y = e(P' ∣ P) · ord_P u, so n divides e. The polynomial relation bounds the degree by n, and the fundamental inequality bounds e by that degree. Thus the extension degree is proved, rather than assumed. No existence of a reduced representative is claimed: in the Artin–Schreier application, the prime-to-p pole is an explicit input.

Replacing y by y - w with w ∈ F replaces u by the equivalent representative u - (w ^ p - w) (TauCeti.sub_algebraMap_pow_sub_self_eq). Hence the same conclusions hold when only some translate u - (w ^ p - w) has a prime-to-p pole, i.e. for a supplied reduced Artin–Schreier representative.

The base-field obstruction is Valuation.ne_pow_sub_self_of_ord_neg_of_not_dvd: such a pole also ensures u ≠ w ^ p - w for every w ∈ F.

The Bezout identity between the characteristic and a reduced pole order gives an explicit uniformizer generator z = y ^ β * t ^ α. This is the generator whose Galois displacements enter the derivative calculation for the Artin--Schreier different.

References

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

theorem TauCeti.Place.natCast_mul_ord_eq_ramificationIdx_mul_ord_of_pow_sub_self_eq (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'} {y : F'} {n : ℕ} {u : F} (hn : 1 < n) (hy : y ^ n - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) : ↑n * P'.ord y = ↑(ramificationIdx F P') * (restrict k F P').ord u

Orders in y ^ n - y = u at a pole of u: the power term dominates, giving n · ord_{P'} y = e(P' ∣ P) · ord_P u.

theorem TauCeti.Place.finrank_eq_of_pow_sub_self_eq_of_gcd_ord_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'} {y : F'} {n : ℕ} {u : F} (hn : 1 < n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) (hcop : (↑n).gcd ((restrict k F P').ord u) = 1) : Module.finrank F F' = n

A generator satisfying y ^ n - y = u has degree n if u has a pole of order coprime to n. In particular this proves degree p for an Artin–Schreier equation with a prime-to-p pole.

theorem TauCeti.Place.ramificationIdx_eq_of_pow_sub_self_eq_of_gcd_ord_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'} {y : F'} {n : ℕ} {u : F} (hn : 1 < n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) (hcop : (↑n).gcd ((restrict k F P').ord u) = 1) : ramificationIdx F P' = n

A pole of order coprime to n is totally ramified in a generated extension y ^ n - y = u: the ramification index equals n.

theorem TauCeti.Place.isTotallyRamified_of_pow_sub_self_eq_of_gcd_ord_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'} {y : F'} {n : ℕ} {u : F} (hn : 1 < n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) (hcop : (↑n).gcd ((restrict k F P').ord u) = 1) : IsTotallyRamified F P'

A pole of order coprime to n is totally ramified in F(y) / F when y ^ n - y = u. The existing total-ramification API gives relative degree one and a singleton fibre over the restricted place.

theorem TauCeti.Place.ord_eq_of_pow_sub_self_eq_of_gcd_ord_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'} {y : F'} {n : ℕ} {u : F} (hn : 1 < n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) (hcop : (↑n).gcd ((restrict k F P').ord u) = 1) : P'.ord y = (restrict k F P').ord u

The generator has the same order as u below a totally ramified pole of y ^ n - y = u, provided the pole order is coprime to n.

theorem TauCeti.Place.exists_eq_zpow_mul_adjoin_eq_top_ord_eq_one_of_pow_sub_self_eq_of_gcd_ord_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'} {y : F'} {n : ℕ} {u : F} (hn : 1 < n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n - y = (algebraMap F F') u) (hu : (restrict k F P').ord u < 0) (hcop : (↑n).gcd ((restrict k F P').ord u) = 1) : ∃ (z : F') (t : F) (α : ℤ) (β : ℤ), (restrict k F P').ord t = 1 ∧ ↑n * α + (restrict k F P').ord u * β = 1 ∧ z = y ^ β * (algebraMap F F') t ^ α ∧ F⟮z⟯ = ⊤ ∧ P'.ord z = 1

At a reduced Artin--Schreier pole, a Bezout combination of the pole generator and a uniformizer from the field below is a uniformizer that still generates the extension. The displayed construction is the one used to evaluate Galois displacements in the different formula.

theorem TauCeti.Place.isTotallyRamified_of_exists_reduced_artinSchreier_pole (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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) (hpole : ∃ (w : F), (restrict k F P').ord (u - (w ^ p - w)) < 0 ∧ ¬↑p ∣ (restrict k F P').ord (u - (w ^ p - w))) : IsTotallyRamified F P'

A reduced Artin–Schreier pole is totally ramified: if some representative u - (w ^ p - w) of the class of u has a pole of order prime to p below P', then P' is totally ramified over that place. No perfection hypothesis on the residue field is needed.

theorem TauCeti.Place.finrank_eq_of_exists_reduced_artinSchreier_pole (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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) (hpole : ∃ (w : F), (restrict k F P').ord (u - (w ^ p - w)) < 0 ∧ ¬↑p ∣ (restrict k F P').ord (u - (w ^ p - w))) : Module.finrank F F' = p

A reduced Artin–Schreier pole forces the extension to have degree p: if some representative u - (w ^ p - w) of the class of u has a pole of order prime to p below P', then [F' : F] = p.

theorem TauCeti.Place.ramificationIdx_eq_of_exists_reduced_artinSchreier_pole (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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) (hpole : ∃ (w : F), (restrict k F P').ord (u - (w ^ p - w)) < 0 ∧ ¬↑p ∣ (restrict k F P').ord (u - (w ^ p - w))) : ramificationIdx F P' = p

At a reduced Artin–Schreier pole the ramification index is p.