A wild place: y² + y = x³ over 𝔽₂

Let W be the Weierstrass curve y² + y = x³ over 𝔽₂, Mathlib's model ofJ0 of j = 0, an elliptic curve, and let F(W) = 𝔽₂(x, y) be its function field, a quadratic extension of 𝔽₂(x). This file computes the different of F(W) / 𝔽₂(x) and finds it concentrated at the place at infinity, with exponent 4, twice the ramification index 2: the place at infinity is wildly ramified, and Dedekind's tame formula d = e - 1 fails there (Stichtenoth, Theorem 3.5.1 and Proposition 3.7.8).

The computation runs the Hurwitz genus formula backwards. Away from infinity the derivative 2y + 1 = 1 of the defining equation is a unit, so every finite place is unramified with different exponent 0. The place at infinity is the unique place over the infinite place of 𝔽₂(x), with ramification index 2. Since F(W) has genus 1, the Hurwitz genus formula 2g - 2 = -2 [F(W) : 𝔽₂(x)] + deg Diff gives deg Diff = 4, and the place at infinity is rational, so its different exponent is 4.

Main results

• TauCeti.ArtinSchreier.differentExponent_eq_zero_of_ne_infinity: every finite place of 𝔽₂(x, y) is unramified over 𝔽₂(x).
• TauCeti.ArtinSchreier.differentExponent_infinity: the different exponent at infinity is 4.
• TauCeti.ArtinSchreier.isWild_infinity and TauCeti.ArtinSchreier.ramificationIdx_infinity_ne_differentExponent_add_one: the place at infinity is wild, and the tame formula e = d + 1 fails there.

References

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

instance TauCeti.ArtinSchreier.instFactIsUnitZModOfNatNat_tauCeti : Fact (IsUnit 3)

3 = 1 is a unit in 𝔽₂, so Mathlib's model y² + y = x³ of j = 0 is an elliptic curve.

theorem TauCeti.ArtinSchreier.instIsDedekindDomainCoordinateRingZModOfNatNatToAffineOfJ0_tauCeti : IsDedekindDomain (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine.CoordinateRing

instance TauCeti.ArtinSchreier.instCharPFunctionFieldZModOfNatNatToAffineOfJ0_tauCeti : CharP (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine.FunctionField 2

The function field 𝔽₂(x, y) has characteristic 2, which is what makes the derivative 2y + 1 of the defining equation equal to 1.

@[simp]

theorem TauCeti.ArtinSchreier.differentExponent_eq_zero_of_ne_infinity (Q : Place (ZMod 2) (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine.FunctionField) (hQ : Q ≠ Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine) : Place.differentExponent (ZMod 2) (RatFunc (ZMod 2)) Q = 0

Away from infinity, y² + y = x³ is unramified: at a place Q of 𝔽₂(x, y) other than the place at infinity, x is regular and the derivative 2y + 1 = 1 of the defining equation is a unit, so the different exponent of Q over 𝔽₂(x) is 0.

theorem TauCeti.ArtinSchreier.different_eq : Divisor.different (ZMod 2) (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine.FunctionField ⋯ = ↑(Place.differentExponent (ZMod 2) (RatFunc (ZMod 2)) (Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine)) • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine)

The different of 𝔽₂(x, y) / 𝔽₂(x) is supported at the place at infinity, with multiplicity its different exponent there.

@[simp]

theorem TauCeti.ArtinSchreier.differentExponent_infinity : Place.differentExponent (ZMod 2) (RatFunc (ZMod 2)) (Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine) = 4

The different exponent at infinity is 4: the Hurwitz genus formula over 𝔽₂(x), with genus 1 and degree 2, gives deg Diff = 4, and the different is concentrated at the rational place at infinity.

theorem TauCeti.ArtinSchreier.isWild_infinity : Place.IsWild (ZMod 2) (RatFunc (ZMod 2)) (Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine)

The place at infinity of y² + y = x³ is wild: its different exponent 4 is at least its ramification index 2.

theorem TauCeti.ArtinSchreier.ramificationIdx_infinity_ne_differentExponent_add_one : Place.ramificationIdx (RatFunc (ZMod 2)) (Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine) ≠ Place.differentExponent (ZMod 2) (RatFunc (ZMod 2)) (Place.infinity (WeierstrassCurve.ofJ0 (ZMod 2)).toAffine) + 1

The tame formula fails at infinity: e = 2 while d + 1 = 5.