The Artin–Schreier curves y ^ p - y = x ^ m

Let k be a field of characteristic p and m a natural number not divisible by p. This file constructs the function field F = k(x, y) of the curve y ^ p - y = x ^ m and computes its ramification over k(x) completely. It is the standard example of wild ramification, which the tame theory gets wrong:

• F / k(x) is an Artin–Schreier extension of degree p, and k is the exact constant field of F;
• the place at infinity of k(x) is totally ramified in F, with a unique place P_∞ above it, of degree one; every other place of k(x) is unramified;
• P_∞ is wild: its ramification index e = p vanishes in the residue field, and its different exponent is d = (p - 1) (m + 1), so d ≥ e, whereas a tame place has d = e - 1 (Dedekind's different theorem);
• the different of F / k(x) is (p - 1) (m + 1) P_∞, while the tame count e - 1 gives only (p - 1) P_∞; the Hurwitz genus formula with the true different gives 2 g = (p - 1) (m - 1).

For instance y ^ 2 - y = x ^ 3 in characteristic two has genus one and different 4 P_∞, and y ^ p - y = x ^ 2 for odd p has genus (p - 1) / 2 and different 3 (p - 1) P_∞. Fed the tame different instead, the Hurwitz formula would give 2 g - 2 = -2 p + (p - 1), a negative genus.

Main declarations

• TauCeti.ArtinSchreierMonomial.FunctionField k p m: the function field, with coordinates genX and genY; it is a field by TauCeti.ArtinSchreierMonomial.irreducible_equationPolynomial.
• TauCeti.ArtinSchreierMonomial.existsUnique_restrict_eq_infty: the unique place P_∞ over infinity, of degree one.
• TauCeti.ArtinSchreierMonomial.differentExponent_eq_of_restrict_eq_infty and TauCeti.ArtinSchreierMonomial.isWild_of_restrict_eq_infty: d(P_∞) = (p - 1) (m + 1), and P_∞ is wild.
• TauCeti.ArtinSchreierMonomial.ramificationIdx_eq_one_of_restrict_ne_infty: no other place ramifies.
• TauCeti.ArtinSchreierMonomial.different_eq and TauCeti.ArtinSchreierMonomial.tameDifferent_eq: the different and the tame different.
• TauCeti.ArtinSchreierMonomial.two_mul_genus: 2 g = (p - 1) (m - 1).
• TauCeti.ArtinSchreierMonomial.genus_functionField_two_three and TauCeti.ArtinSchreierMonomial.two_mul_genus_functionField_two: the two classical instances.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.5.1 and Proposition 3.7.8.
• TauCeti/FieldTheory/FunctionField/Hyperelliptic/Genus/Two.lean (TauCeti.GenusTwo): the function-field construction via AdjoinRoot is adapted from this worked example.

noncomputable def TauCeti.ArtinSchreierMonomial.equationPolynomial (k : Type u_1) [Field k] (p m : ℕ) : Polynomial (RatFunc k)

The Artin–Schreier equation Y ^ p - Y - x ^ m over k(x).

theorem TauCeti.ArtinSchreierMonomial.equationPolynomial_def (k : Type u_1) [Field k] (p m : ℕ) : equationPolynomial k p m = Polynomial.X ^ p - Polynomial.X - Polynomial.C (RatFunc.X ^ m)

The defining polynomial, for computation without unfolding its body.

@[reducible, inline]

abbrev TauCeti.ArtinSchreierMonomial.FunctionField (k : Type u_1) [Field k] (p m : ℕ) : Type u_1

The function field of the affine curve y ^ p - y = x ^ m, obtained by adjoining a root of the Artin–Schreier equation to k(x). It is a field when p is a prime not dividing m and k has characteristic p.

noncomputable def TauCeti.ArtinSchreierMonomial.genY (k : Type u_1) [Field k] (p m : ℕ) : FunctionField k p m

The y-coordinate: the root of the Artin–Schreier equation.

theorem TauCeti.ArtinSchreierMonomial.genY_def (k : Type u_1) [Field k] (p m : ℕ) : genY k p m = AdjoinRoot.root (equationPolynomial k p m)

The y-coordinate is the root in the defining root algebra.

noncomputable def TauCeti.ArtinSchreierMonomial.genX (k : Type u_1) [Field k] (p m : ℕ) : FunctionField k p m

The x-coordinate: the image of the variable of k(x).

theorem TauCeti.ArtinSchreierMonomial.genX_def (k : Type u_1) [Field k] (p m : ℕ) : genX k p m = (algebraMap (RatFunc k) (FunctionField k p m)) RatFunc.X

The x-coordinate is the image of the variable of k(x).

theorem TauCeti.ArtinSchreierMonomial.genY_pow_sub_genY (k : Type u_1) [Field k] (p m : ℕ) : genY k p m ^ p - genY k p m = (algebraMap (RatFunc k) (FunctionField k p m)) (RatFunc.X ^ m)

The coordinate y satisfies the Artin–Schreier equation over k(x).

theorem TauCeti.ArtinSchreierMonomial.genY_pow_sub_genY_eq (k : Type u_1) [Field k] (p m : ℕ) : genY k p m ^ p - genY k p m = genX k p m ^ m

The equation of the curve: y ^ p - y = x ^ m.

theorem TauCeti.ArtinSchreierMonomial.irreducible_equationPolynomial (k : Type u_1) [Field k] (p : ℕ) {m : ℕ} [Fact (Nat.Prime p)] [CharP k p] (hm : ¬p ∣ m) : Irreducible (equationPolynomial k p m)

The Artin–Schreier equation of y ^ p - y = x ^ m is irreducible over k(x) when p ∤ m.

instance TauCeti.ArtinSchreierMonomial.instFactIrreduciblePolynomialRatFuncEquationPolynomial (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : Fact (Irreducible (equationPolynomial k p m))

Irreducibility supplies the field structure on the root algebra.

theorem TauCeti.ArtinSchreierMonomial.adjoin_genY_eq_top (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : (RatFunc k)⟮genY k p m⟯ = ⊤

The function field is generated by y over k(x).

theorem TauCeti.ArtinSchreierMonomial.finrank_eq (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : Module.finrank (RatFunc k) (FunctionField k p m) = p

The function field has degree p over k(x).

instance TauCeti.ArtinSchreierMonomial.instFiniteDimensionalRatFuncFunctionField (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : FiniteDimensional (RatFunc k) (FunctionField k p m)

The function field is finite over k(x).

instance TauCeti.ArtinSchreierMonomial.instIsGaloisRatFuncFunctionField (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : IsGalois (RatFunc k) (FunctionField k p m)

The function field is a Galois extension of k(x), as every Artin–Schreier extension is.

theorem TauCeti.ArtinSchreierMonomial.isFunctionField (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : IsFunctionField k (FunctionField k p m)

The curve y ^ p - y = x ^ m has an algebraic function field over k.

theorem TauCeti.ArtinSchreierMonomial.isIntegrallyClosedIn (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : IsIntegrallyClosedIn k (FunctionField k p m)

The constants of y ^ p - y = x ^ m are exactly k: the pole at infinity is totally ramified.

The place at infinity

theorem TauCeti.ArtinSchreierMonomial.ramificationIdx_eq_of_restrict_eq_infty {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : Place.ramificationIdx (RatFunc k) P = p

The place at infinity is totally ramified: a place over it has ramification index p.

theorem TauCeti.ArtinSchreierMonomial.isWild_of_restrict_eq_infty {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : Place.IsWild k (RatFunc k) P

The place at infinity is wild: its ramification index p vanishes in its residue field.

theorem TauCeti.ArtinSchreierMonomial.differentExponent_eq_of_restrict_eq_infty {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : Place.differentExponent k (RatFunc k) P = (p - 1) * (m + 1)

The different exponent at infinity is (p - 1) (m + 1), the conductor computation for a reduced pole of order m.

theorem TauCeti.ArtinSchreierMonomial.ramificationIdx_le_differentExponent_of_restrict_eq_infty {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : Place.ramificationIdx (RatFunc k) P ≤ Place.differentExponent k (RatFunc k) P

The tame different theorem fails at infinity: the different exponent d is at least the ramification index e, so e ≠ d + 1, unlike at every tame place.

theorem TauCeti.ArtinSchreierMonomial.existsUnique_restrict_eq_infty (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : ∃ (P : Place k (FunctionField k p m)), Place.restrict k (RatFunc k) P = Place.infty k ∧ P.degree = 1 ∧ ∀ (Q : Place k (FunctionField k p m)), Place.restrict k (RatFunc k) Q = Place.infty k → Q = P

There is exactly one place over infinity, and it has degree one.

The finite places

theorem TauCeti.ArtinSchreierMonomial.ramificationIdx_eq_one_of_restrict_ne_infty {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P ≠ Place.infty k) : Place.ramificationIdx (RatFunc k) P = 1

The finite places are unramified: away from infinity x ^ m is regular.

theorem TauCeti.ArtinSchreierMonomial.differentExponent_eq_zero_of_restrict_ne_infty {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P ≠ Place.infty k) : Place.differentExponent k (RatFunc k) P = 0

The different exponent vanishes at the finite places.

The different and the genus

theorem TauCeti.ArtinSchreierMonomial.different_eq (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : Divisor.different k (FunctionField k p m) ⋯ = ↑((p - 1) * (m + 1)) • AlgebraicGeometry.WeilDivisor.ofPoint P

The different of F / k(x) is (p - 1) (m + 1) P_∞, concentrated at the unique place over infinity.

theorem TauCeti.ArtinSchreierMonomial.tameDifferent_eq (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] {P : Place k (FunctionField k p m)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : Divisor.tameDifferent k (FunctionField k p m) ⋯ = ↑(p - 1) • AlgebraicGeometry.WeilDivisor.ofPoint P

The tame different of F / k(x) is only (p - 1) P_∞: the tame count e - 1 misses the wild part of the different.

theorem TauCeti.ArtinSchreierMonomial.degree_different (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : Divisor.degree (Divisor.different k (FunctionField k p m) ⋯) = (↑p - 1) * (↑m + 1)

The different of F / k(x) has degree (p - 1) (m + 1).

theorem TauCeti.ArtinSchreierMonomial.two_mul_genus (k : Type u_1) [Field k] (p m : ℕ) [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m] : 2 * genus k (FunctionField k p m) = (p - 1) * (m - 1)

The genus of y ^ p - y = x ^ m is (p - 1) (m - 1) / 2: the Hurwitz genus formula over k(x) with the different (p - 1) (m + 1) P_∞.

The two classical instances

theorem TauCeti.ArtinSchreierMonomial.genus_functionField_two_three (k : Type u_1) [Field k] [CharP k 2] : genus k (FunctionField k 2 3) = 1

y ^ 2 - y = x ^ 3 in characteristic two has genus one. Its different 4 P_∞ is wild: with the tame count P_∞ instead, the Hurwitz formula would read 2 g - 2 = -3.

theorem TauCeti.ArtinSchreierMonomial.two_mul_genus_functionField_two (k : Type u_1) [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (hp : p ≠ 2) : 2 * genus k (FunctionField k p 2) = p - 1

y ^ p - y = x ^ 2 has genus (p - 1) / 2 for an odd prime p.