Genus counting for Weierstrass function fields

At the unique infinite place the coordinate functions have orders -2 and -3. The Weierstrass basis {1, y} therefore supplies r independent functions in L(r·∞), while the missing pole order one gives ℓ(∞) = 1. The general bounded-defect family theorem then gives genus one. Finally, a degree-zero canonical divisor is moved to zero by its unique nonzero Riemann–Roch section.

theorem WeierstrassCurve.Affine.Chart.instCoordinateConstantsTowerGenus {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : IsScalarTower k W.CoordinateRing K

theorem WeierstrassCurve.Affine.Chart.yCoord_ne_zero {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : W.yCoord K ≠ 0

theorem WeierstrassCurve.Affine.Chart.yCoord_order_at_infinity {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : ((FunctionField.Chart.principalDivisorA k K) (Additive.ofMul (Units.mk0 (W.yCoord K) ⋯))) (infinityPlace K) = -3

noncomputable def WeierstrassCurve.Affine.Chart.infinityDivisor {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : FunctionField.Chart.DivisorA k K

The effective degree-one divisor supported at the unique infinite place.

Equations

• WeierstrassCurve.Affine.Chart.infinityDivisor K = Finsupp.single (WeierstrassCurve.Affine.Chart.infinityPlace K) 1

theorem WeierstrassCurve.Affine.Chart.deg_infinityDivisor {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : FunctionField.Chart.deg k K (infinityDivisor K) = 1

theorem WeierstrassCurve.Affine.Chart.polarDivisor_XK_eq_two_infinity {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : FunctionField.Chart.polarDivisor k K (FunctionField.Chart.XK k K) = 2 • infinityDivisor K

theorem WeierstrassCurve.Affine.Chart.yCoord_mem_ringOfIntegers {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] : ∃ (a : ↥(FunctionField.ringOfIntegers k K)), ↑a = W.yCoord K

theorem WeierstrassCurve.Affine.Chart.polarDivisor_yCoord_zero_at_finite {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : (FunctionField.Chart.polarDivisor k K (W.yCoord K)) (Sum.inl v) = 0

theorem WeierstrassCurve.Affine.Chart.polarDivisor_yCoord_eq_three_infinity {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : FunctionField.Chart.polarDivisor k K (W.yCoord K) = 3 • infinityDivisor K

theorem WeierstrassCurve.Affine.Chart.valuation_aeval_XK {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (p : Polynomial k) (hp : p ≠ 0) : (FunctionField.Chart.placeValuation k K (infinityPlace K)) ((Polynomial.aeval (FunctionField.Chart.XK k K)) p) = WithZero.exp (2 * ↑p.natDegree)

theorem WeierstrassCurve.Affine.Chart.valuation_aeval_XK_mul_yCoord {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (q : Polynomial k) (hq : q ≠ 0) : (FunctionField.Chart.placeValuation k K (infinityPlace K)) ((Polynomial.aeval (FunctionField.Chart.XK k K)) q * W.yCoord K) = WithZero.exp (2 * ↑q.natDegree + 3)

theorem WeierstrassCurve.Affine.Chart.ell_infinity_eq_one {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : FunctionField.Chart.ell k K (infinityDivisor K) = 1

theorem WeierstrassCurve.Affine.Chart.ell_nsmul_infinity_ge_add {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (r a b : ℕ) (ha : ∀ (j : Fin a), 2 * ↑j ≤ r) (hb : ∀ (j : Fin b), 2 * ↑j + 3 ≤ r) : a + b ≤ FunctionField.Chart.ell k K (r • infinityDivisor K)

theorem WeierstrassCurve.Affine.Chart.ell_nsmul_infinity_ge {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (r : ℕ) : r ≤ FunctionField.Chart.ell k K (r • infinityDivisor K)

theorem WeierstrassCurve.Affine.Chart.genus_eq_one_counting {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] [FunctionField.IsFullConstantField k K] : FunctionField.Chart.genus k K = 1

theorem WeierstrassCurve.Affine.Chart.zero_isCanonical_of_genus_eq_one {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] [FunctionField.IsFullConstantField k K] (hg : FunctionField.Chart.genus k K = 1) : FunctionField.Chart.IsCanonical k K 0