The genus formula for Artin--Schreier extensions

For F' = F(y) with y ^ p - y = u, supply reduced representatives of the class of u at every place of F. On a finite set S, these representatives have pole orders m P prime to p; outside S, they are regular. The conductor divisor on F has coefficient m P + 1 on S and zero elsewhere. Total ramification and the local different formula give

p • Diff(F'/F) = (p - 1) • Con (∑ P ∈ S, (m P + 1) P).

Taking degrees gives [k' : k] deg Diff = (p - 1) ∑ P ∈ S, (m P + 1) deg P. For a nontrivial Artin--Schreier class, Hurwitz then computes the genus:

[k' : k] (2g' - 2) = p (2g - 2) + (p - 1) ∑ P ∈ S, (m P + 1) deg P.

The hypotheses supply the representatives, not their ramification data. No perfectness of constants or residue fields is assumed. Over imperfect residue fields such representatives need not exist. The genus formula uses exact constants and the finite separable constant-field extension required by the Hurwitz theorem.

isIntegrallyClosedIn_of_exists_reduced_artinSchreier_pole proves exactness of the extension's constants from a single supplied reduced pole. For a finite nonempty set of reduced poles, two_mul_genus_sub_two_eq_of_exists_reduced_artinSchreier_poles derives nontriviality and exactness of the constants over any function field with exact constants. For an extension of k(x), two_mul_genus_eq_of_exists_reduced_artinSchreier_poles_ratFunc specialises this to 2g = (p - 1) (∑ P ∈ S, (m P + 1) deg P - 2). Finiteness, separability, nontriviality, and exactness of the constants are derived from the equation and a pole. For a single pole, two_mul_genus_eq_of_exists_reduced_artinSchreier_pole_ratFunc gives 2g = (p - 1) ((m + 1) deg P - 2) directly.

References

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

theorem TauCeti.Divisor.nsmul_different_eq_zsmul_conorm_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'] (hF : IsFunctionField k F) (hF' : IsFunctionField 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) (S : Finset (Place k F)) (m : Place k F → ℕ) (hpole : ∀ P ∈ S, ∃ (w : F), P.ord (u - (w ^ p - w)) = -↑(m P) ∧ ¬↑p ∣ P.ord (u - (w ^ p - w))) (hreg : ∀ P ∉ S, ∃ (w : F), u - (w ^ p - w) ∈ P.integers) : p • different k' F' hF = (↑p - 1) • (conorm k' F') (AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity S fun (P : Place k F) => m P + 1)

The different of an Artin--Schreier extension is computed by the conorm of its reduced conductor divisor. This is a divisor identity, before taking degrees or imposing exact constants. The supplied pole orders are necessarily positive because they are not divisible by p.

theorem TauCeti.Divisor.finrank_mul_degree_different_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'] (hF : IsFunctionField k F) (hF' : IsFunctionField 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) (S : Finset (Place k F)) (m : Place k F → ℕ) (hpole : ∀ P ∈ S, ∃ (w : F), P.ord (u - (w ^ p - w)) = -↑(m P) ∧ ¬↑p ∣ P.ord (u - (w ^ p - w))) (hreg : ∀ P ∉ S, ∃ (w : F), u - (w ^ p - w) ∈ P.integers) : ↑(Module.finrank k k') * degree (different k' F' hF) = (↑p - 1) * ∑ P ∈ S, (↑(m P) + 1) * ↑P.degree

The weighted degree of the Artin--Schreier different, for supplied reduced representatives. A reduced pole forces the extension degree to be p; when there are no reduced poles, the different is zero. The factor [k' : k] accounts for a possible enlargement of the constant field. No exactness or constant-field separability is needed for this degree identity.

theorem TauCeti.artinSchreier_genus_formula {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'] (hF : IsFunctionField k F) (hF' : IsFunctionField 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) (S : Finset (Place k F)) (m : Place k F → ℕ) (hpole : ∀ P ∈ S, ∃ (w : F), P.ord (u - (w ^ p - w)) = -↑(m P) ∧ ¬↑p ∣ P.ord (u - (w ^ p - w))) (hreg : ∀ P ∉ S, ∃ (w : F), u - (w ^ p - w) ∈ P.integers) [Algebra.IsSeparable k k'] (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (hu : ∀ (w : F), w ^ p - w ≠ u) : ↑(Module.finrank k k') * (2 * ↑(genus k' F') - 2) = ↑p * (2 * ↑(genus k F) - 2) + (↑p - 1) * ∑ P ∈ S, (↑(m P) + 1) * ↑P.degree

The Artin--Schreier genus formula, cross-multiplied for a possible constant-field extension. The representatives may vary with the place. Pole orders are weighted by residue field degrees, not by the number of poles.

theorem TauCeti.isIntegrallyClosedIn_of_exists_reduced_artinSchreier_pole {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn 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) (P : Place k F) (hpole : ∃ (w : F), P.ord (u - (w ^ p - w)) < 0 ∧ ¬↑p ∣ P.ord (u - (w ^ p - w))) : IsIntegrallyClosedIn k F'

An Artin--Schreier extension of a function field with exact constants acquires no new constants if one supplied representative has a pole of order prime to p. Finiteness and separability follow from the equation and the generator hypothesis.

theorem TauCeti.two_mul_genus_sub_two_eq_of_exists_reduced_artinSchreier_poles {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn 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) (S : Finset (Place k F)) (m : Place k F → ℕ) (hS : S.Nonempty) (hord : ∀ P ∈ S, ∃ (w : F), P.ord (u - (w ^ p - w)) = -↑(m P)) (hprime : ∀ P ∈ S, ¬p ∣ m P) (hreg : ∀ Q ∉ S, ∃ (w : F), u - (w ^ p - w) ∈ Q.integers) : 2 * ↑(genus k F') - 2 = ↑p * (2 * ↑(genus k F) - 2) + (↑p - 1) * ∑ P ∈ S, (↑(m P) + 1) * ↑P.degree

An Artin--Schreier extension of a function field with exact constants and a finite nonempty set of supplied reduced poles has no new constants. Its genus is determined by 2g' - 2 = p (2g - 2) + (p - 1) ∑ P ∈ S, (m P + 1) deg P. Finiteness, separability, nontriviality, and exactness of the extension's constants follow from the equation and a pole. The representatives may vary with the place.

theorem TauCeti.two_mul_genus_eq_of_exists_reduced_artinSchreier_poles_ratFunc {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] (p : ℕ) [Fact (Nat.Prime p)] [CharP (RatFunc k) p] {y : F} {u : RatFunc k} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap (RatFunc k) F) u) (S : Finset (Place k (RatFunc k))) (m : Place k (RatFunc k) → ℕ) (hS : S.Nonempty) (hord : ∀ P ∈ S, ∃ (w : RatFunc k), P.ord (u - (w ^ p - w)) = -↑(m P)) (hprime : ∀ P ∈ S, ¬p ∣ m P) (hreg : ∀ Q ∉ S, ∃ (w : RatFunc k), u - (w ^ p - w) ∈ Q.integers) : 2 * ↑(genus k F) = (↑p - 1) * (∑ P ∈ S, (↑(m P) + 1) * ↑P.degree - 2)

An Artin--Schreier extension of k(x) with supplied reduced representatives and a finite nonempty set of poles of orders prime to p has genus determined by 2g = (p - 1) (∑ P ∈ S, (m P + 1) deg P - 2). The representatives may vary with the place. For one rational pole of order m, this is 2g = (p - 1) (m - 1). Finiteness, separability, nontriviality, and exactness of the constants follow from the equation and a pole.

theorem TauCeti.two_mul_genus_eq_of_exists_reduced_artinSchreier_pole_ratFunc {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] (p : ℕ) [Fact (Nat.Prime p)] [CharP (RatFunc k) p] {y : F} {u : RatFunc k} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ p - y = (algebraMap (RatFunc k) F) u) (P : Place k (RatFunc k)) (m : ℕ) (hord : ∃ (w : RatFunc k), P.ord (u - (w ^ p - w)) = -↑m) (hprime : ¬p ∣ m) (hreg : ∀ (Q : Place k (RatFunc k)), Q ≠ P → ∃ (w : RatFunc k), u - (w ^ p - w) ∈ Q.integers) : 2 * ↑(genus k F) = (↑p - 1) * ((↑m + 1) * ↑P.degree - 2)

An Artin--Schreier extension of k(x) with a single supplied reduced pole of order m prime to p has genus determined by 2g = (p - 1) ((m + 1) deg P - 2). Representatives may vary with the place; finiteness, separability, nontriviality, and exactness of the constants follow from the equation and the pole.