The different of an odd-degree squarefree polynomial model

For y² = f(x) with f squarefree of positive odd degree, there is a unique place above infinity, and it is rational. Away from characteristic two the different is the zero divisor of y plus that place. In particular, every zero of y occurs with coefficient one. This identifies the different itself, not just its degree, and applies over arbitrary constant fields, without requiring the roots of f to be rational.

This gives an explicit ramification divisor (the different) for odd-degree hyperelliptic models, including the genus-two model y² = x⁵ - 1.

References

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 6.2.3 and Example 3.7.6.

theorem TauCeti.different_ratFunc_eq_zeros_add_of_sq_eq_of_odd {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hodd : Odd f.natDegree) {y : Fˣ} (hgen : (RatFunc k)⟮↑y⟯ = ⊤) (hy : ↑y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) {P : Place k F} : Place.restrict k (RatFunc k) P = Place.infty k → Divisor.different k F ⋯ = Divisor.zeros ⋯ y + AlgebraicGeometry.WeilDivisor.ofPoint P

The different of an odd-degree squarefree polynomial model: away from characteristic two, Diff(F/k(x)) = (y)₀ + P∞. The zero divisor includes the closed points over all irreducible factors of f, not just its roots in the constant field.

theorem TauCeti.Divisor.coeff_zeros_eq_one_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (hF : IsFunctionField k F) {f : Polynomial k} (hf : Squarefree f) {y : Fˣ} (hgen : (RatFunc k)⟮↑y⟯ = ⊤) (hy : ↑y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) {Q : Place k F} (hQ : Q ∈ (zeros hF y).support) : AlgebraicGeometry.WeilDivisor.coeff (zeros hF y) Q = 1

Every zero of y in a squarefree polynomial model has multiplicity one, in every degree and characteristic.

theorem TauCeti.different_ratFunc_eq_ofFinset_add_of_sq_eq_of_odd {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hodd : Odd f.natDegree) {y : Fˣ} (hgen : (RatFunc k)⟮↑y⟯ = ⊤) (hy : ↑y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) {P : Place k F} : Place.restrict k (RatFunc k) P = Place.infty k → Divisor.different k F ⋯ = AlgebraicGeometry.WeilDivisor.ofFinset (Divisor.zeros ⋯ y).support + AlgebraicGeometry.WeilDivisor.ofPoint P

The different as the divisor of distinct closed points: the zeros of y in an odd-degree squarefree polynomial model each contribute once, together with the unique place at infinity. No splitting assumption on the polynomial over the constant field is needed.