Ramification from a reduced Artin--Schreier representative

Let F' = F(y) with y ^ p - y = u in characteristic p. Replacing y by y - w replaces u by the equivalent representative u - (w ^ p - w). This file proves the ramification dichotomy for a representative reduced at a place P:

• if the representative is regular at P, every place above P has different exponent zero and ramification index one;
• if it has a pole of order m not divisible by p, every place above P is totally ramified and its different exponent is (p - 1) * (m + 1).

The regular case follows from the derivative -1 of X ^ p - X - u. In the pole case, a Bezout construction supplies a generating uniformizer z such that every nonidentity Galois automorphism satisfies ord (σ z - z) = m + 1. Its powers form an integral basis at the totally ramified place, so the derivative formula for the different turns these displacements into the exact exponent.

References

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

theorem TauCeti.Place.differentExponent_eq_zero_of_pow_sub_self_eq_of_mem_integers (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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {y : F'} {a : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap F F') a) (ha : a ∈ (restrict k F P').integers) : differentExponent k F P' = 0

An Artin--Schreier generator whose right-hand side is regular has different exponent zero.

This is the m_P = -1 case of the Artin--Schreier different formula.

theorem TauCeti.Place.ramificationIdx_eq_one_of_pow_sub_self_eq_of_mem_integers (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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] {y : F'} {a : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap F F') a) (ha : a ∈ (restrict k F P').integers) : ramificationIdx F P' = 1

An Artin--Schreier generator whose right-hand side is regular has ramification index one at every place above the given place.

theorem TauCeti.Place.differentExponent_eq_zero_of_exists_sub_pow_sub_self_mem_integers (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'] [FiniteDimensional F F'] [Algebra.IsSeparable 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) (hreg : ∃ (w : F), u - (w ^ p - w) ∈ (restrict k F P').integers) : differentExponent k F P' = 0

If an Artin--Schreier class has a representative regular at the place below P', then the different exponent at P' is zero.

theorem TauCeti.Place.ramificationIdx_eq_one_of_exists_sub_pow_sub_self_mem_integers (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'] [FiniteDimensional F F'] [Algebra.IsSeparable 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) (hreg : ∃ (w : F), u - (w ^ p - w) ∈ (restrict k F P').integers) : ramificationIdx F P' = 1

If an Artin--Schreier class has a representative regular at the place below P', then P' has ramification index one over that place.

theorem TauCeti.Place.differentExponent_eq_of_pow_sub_self_eq_of_ord_eq_neg (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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (p m : ℕ) [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 = -↑m) (hprime : ¬↑p ∣ (restrict k F P').ord u) : differentExponent k F P' = (p - 1) * (m + 1)

At an Artin--Schreier pole of order m prime to p, the different exponent is (p - 1) * (m + 1). No perfection hypothesis on the residue field is needed.

theorem TauCeti.Place.differentExponent_eq_of_sub_pow_sub_self_ord_eq_neg (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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (p m : ℕ) [Fact (Nat.Prime p)] [CharP F p] {y : F'} {u w : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap F F') u) (hu : (restrict k F P').ord (u - (w ^ p - w)) = -↑m) (hprime : ¬↑p ∣ (restrict k F P').ord (u - (w ^ p - w))) : differentExponent k F P' = (p - 1) * (m + 1)

The exact different formula for a supplied reduced representative of an Artin--Schreier class. Translating the generator does not change the extension.

theorem TauCeti.Place.isWild_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'] [FiniteDimensional F F'] [Algebra.IsSeparable 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))) : IsWild k F P'

A reduced Artin--Schreier pole is wildly ramified. Indeed, its ramification index is p, which vanishes in the residue field of the place below.

theorem TauCeti.Place.p_le_differentExponent_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'] [FiniteDimensional F F'] [Algebra.IsSeparable 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))) : p ≤ differentExponent k F P'

At a reduced Artin--Schreier pole the different exponent is at least p. This is the wild lower bound; the exact exponent additionally requires the upper bound d(P' | P) ≤ (p - 1) * (m + 1).

theorem TauCeti.Place.differentExponent_eq_zero_and_ramificationIdx_eq_one_or_p_le_differentExponent (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'] [FiniteDimensional F F'] [Algebra.IsSeparable 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) (hred : ∃ (w : F), u - (w ^ p - w) ∈ (restrict k F P').integers ∨ (restrict k F P').ord (u - (w ^ p - w)) < 0 ∧ ¬↑p ∣ (restrict k F P').ord (u - (w ^ p - w))) : differentExponent k F P' = 0 ∧ ramificationIdx F P' = 1 ∨ p ≤ differentExponent k F P' ∧ ramificationIdx F P' = p

For a supplied reduced Artin--Schreier representative, a place is either unramified with different exponent zero, or is totally ramified and satisfies the wild lower bound for the different exponent. This statement does not require the residue field to be perfect.

theorem TauCeti.Place.differentExponent_eq_zero_and_ramificationIdx_eq_one_or_p_le_differentExponent_of_perfectField (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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] [PerfectField (restrict k F P').ResidueField] {y : F'} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap F F') u) : differentExponent k F P' = 0 ∧ ramificationIdx F P' = 1 ∨ p ≤ differentExponent k F P' ∧ ramificationIdx F P' = p

Over a perfect residue field, an Artin--Schreier place is either unramified with different exponent zero, or is totally ramified and satisfies the wild lower bound. The reduced representative is produced inside F, without passing to a completion.