Core construction of the degree-one Picard torsor

This file constructs the divisor-class map, proves its bijectivity by Riemann–Roch, and identifies it with the ideal-class map on rational Weierstrass points.

@[instance_reducible]

noncomputable def WeierstrassCurve.Affine.Chart.instDecidableEqRiemannRoch {k : Type u_1} : DecidableEq k

Classical decidable equality used to instantiate the Weierstrass point group law.

Equations

• WeierstrassCurve.Affine.Chart.instDecidableEqRiemannRoch = Classical.decEq k

theorem WeierstrassCurve.Affine.Chart.ell_eq_one_of_deg_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] {W₀ : FunctionField.Chart.DivisorA k K} (hW₀ : FunctionField.Chart.IsCanonical k K W₀) (D : FunctionField.Chart.DivisorA k K) (hg : FunctionField.Chart.genus k K = 1) (hdeg : FunctionField.Chart.deg k K D = 1) : FunctionField.Chart.ell k K D = 1

A degree-one divisor on a genus-one function field has Riemann–Roch dimension one.

@[reducible, inline]

abbrev WeierstrassCurve.Affine.Chart.Internal.FiniteClassGroup {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] : Type u_2

The ideal class group of the finite-integer ring of K/k.

Equations

• WeierstrassCurve.Affine.Chart.Internal.FiniteClassGroup K = ClassGroup ↥(FunctionField.ringOfIntegers k K)

noncomputable def WeierstrassCurve.Affine.Chart.Internal.finitePart {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : FunctionField.Chart.DivisorA k K) : IsDedekindDomain.Divisor ↥(FunctionField.ringOfIntegers k K)

Restriction of an adelic divisor to its finite-place component.

Equations

• WeierstrassCurve.Affine.Chart.Internal.finitePart K D = (Finsupp.sumFinsuppAddEquivProdFinsupp D).1

@[simp]

theorem WeierstrassCurve.Affine.Chart.Internal.finitePart_apply {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : FunctionField.Chart.DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : (finitePart K D) v = D (Sum.inl v)

noncomputable def WeierstrassCurve.Affine.Chart.Internal.finiteDivisorClass {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] : FunctionField.Chart.DivisorA k K →+ Additive (FiniteClassGroup K)

The ideal class represented by the finite part of an adelic divisor.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Affine.Chart.Internal.finiteDivisorClass_principal {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] (u : Kˣ) : (finiteDivisorClass K) ((FunctionField.Chart.principalDivisorA k K) (Additive.ofMul u)) = 0

theorem WeierstrassCurve.Affine.Chart.Internal.eq_single_of_effective_deg_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] {D : FunctionField.Chart.DivisorA k K} (hD : FunctionField.Chart.IsEffective k K D) (hdeg : FunctionField.Chart.deg k K D = 1) : ∃ (v : FunctionField.Chart.PlaceA k K), FunctionField.Chart.placeDegree k K v = 1 ∧ D = Finsupp.single v 1

theorem WeierstrassCurve.Affine.Chart.Internal.finiteDivisorClass_single_infinite {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] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K)) (n : ℤ) : (finiteDivisorClass K) (Finsupp.single (Sum.inr v) n) = 0

theorem WeierstrassCurve.Affine.Chart.Internal.finiteDivisorClass_single_finite {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] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : (finiteDivisorClass K) (Finsupp.single (Sum.inl v) 1) = Additive.ofMul ((ClassGroup.mk K) ((FractionalIdeal.mk0 K) ⟨v.asIdeal, ⋯⟩))

theorem WeierstrassCurve.Affine.Chart.Internal.classGroup_mulEquiv_mk0 {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] (e : R ≃+* S) (I : ↥(nonZeroDivisors (Ideal R))) : (ClassGroup.mulEquiv e) (ClassGroup.mk0 I) = ClassGroup.mk0 ⟨Ideal.map e ↑I, ⋯⟩

noncomputable def WeierstrassCurve.Affine.Chart.Internal.degreeOneClass {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] (z : { v : FunctionField.Chart.PlaceA k K // FunctionField.Chart.placeDegree k K v = 1 }) : ClassGroup W.CoordinateRing

The coordinate-ring ideal class attached to a degree-one place.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Affine.Chart.Internal.degreeOneClass_placeOfPoint {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] (P : W.Point) : degreeOneClass W K ⟨placeOfPoint W K P, ⋯⟩ = Additive.toMul (Point.toClass P)

theorem WeierstrassCurve.Affine.Chart.Internal.degreeOneClass_injective {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] : Function.Injective (degreeOneClass W K)

theorem WeierstrassCurve.Affine.Chart.Internal.degreeOneClass_surjective {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] : Function.Surjective (degreeOneClass W K)

noncomputable def WeierstrassCurve.Affine.Chart.Internal.picTorsor' {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] : { v : FunctionField.Chart.PlaceA k K // FunctionField.Chart.placeDegree k K v = 1 } ≃ ClassGroup W.CoordinateRing

The core equivalence between degree-one places and coordinate-ring ideal classes.

Equations

• WeierstrassCurve.Affine.Chart.Internal.picTorsor' W K = Equiv.ofBijective (WeierstrassCurve.Affine.Chart.Internal.degreeOneClass W K) ⋯

theorem WeierstrassCurve.Affine.Chart.Internal.picTorsor'_compat_groupLaw {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] {x y : k} (h : W.Nonsingular x y) : (picTorsor' W K) ⟨placeOfPoint W K (Point.some x y h), ⋯⟩ = (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)