Torsion points contribute to the normalization gcd divisor

This file upgrades the pointwise normalization result to a finite divisor inequality. For any Dedekind normalization model of the plane-curve function field, one branch is chosen over each rational torsion point. Distinct points give distinct branches, both torsion functions have positive order there, and therefore the number of torsion points is bounded by the sum of the local gcd multiplicities.

noncomputable def BGS.CorvajaZannier.liftedTorsionPointNormalizationBranch {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {B : Type u_2} [CommRing B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : MaximalSpectrum B

Choose a branch in an arbitrary Dedekind integral-closure model above the maximal ideal defined by a torsion point.

Equations

• BGS.CorvajaZannier.liftedTorsionPointNormalizationBranch firstOrder secondOrder z = { asIdeal := Classical.choose ⋯, isMaximal := ⋯ }

theorem BGS.CorvajaZannier.liftedTorsionPointNormalizationBranch_liesOver {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {B : Type u_2} [CommRing B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : (liftedTorsionPointNormalizationBranch firstOrder secondOrder z).asIdeal.LiesOver (torsionPointMaximalIdeal f firstOrder secondOrder z).asIdeal

theorem BGS.CorvajaZannier.liftedTorsionPointNormalizationBranch_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {B : Type u_2} [CommRing B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] (firstOrder secondOrder : ℕ) : Function.Injective (liftedTorsionPointNormalizationBranch firstOrder secondOrder)

Chosen branches above distinct torsion points are distinct because their contractions to the affine coordinate ring are distinct.

noncomputable def BGS.CorvajaZannier.torsionPointFinitePlace {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : IsDedekindDomain.HeightOneSpectrum B

The finite place selected above a torsion point. It is obtained from the positive-order branch theorem, so its defining prime is the chosen branch.

Equations

• BGS.CorvajaZannier.torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z = Classical.choose ⋯

theorem BGS.CorvajaZannier.torsionPointFinitePlace_spec {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z).asIdeal = (liftedTorsionPointNormalizationBranch firstOrder secondOrder z).asIdeal ∧ 1 ≤ finitePlaceOrder (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z) (planeCurveFunction f 0 ^ firstOrder - 1) ∧ 1 ≤ finitePlaceOrder (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z) (planeCurveFunction f 1 ^ secondOrder - 1) ∧ 1 ≤ min (finitePlaceOrder (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z) (planeCurveFunction f 0 ^ firstOrder - 1)) (finitePlaceOrder (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z) (planeCurveFunction f 1 ^ secondOrder - 1))

theorem BGS.CorvajaZannier.torsionPointFinitePlace_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) : Function.Injective (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero)

noncomputable def BGS.CorvajaZannier.torsionGcdPlaceSupport {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra B (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) : Finset (IsDedekindDomain.HeightOneSpectrum B)

The finite support containing every chosen torsion place.

Equations

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

theorem BGS.CorvajaZannier.torsionPointFinitePlace_mem_torsionGcdPlaceSupport {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z ∈ torsionGcdPlaceSupport firstOrder secondOrder

noncomputable def BGS.CorvajaZannier.torsionGcdMultiplicity {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra B (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (v : IsDedekindDomain.HeightOneSpectrum B) : ℕ

The natural-number local gcd multiplicity of the two torsion functions.

Equations

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

theorem BGS.CorvajaZannier.one_le_torsionGcdMultiplicity_torsionPointFinitePlace {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : 1 ≤ torsionGcdMultiplicity firstOrder secondOrder (torsionPointFinitePlace firstOrder secondOrder hfirstNonzero hsecondNonzero z)

Every chosen torsion branch contributes at least one to the local gcd multiplicity.

theorem BGS.CorvajaZannier.torsionPoint_card_le_torsionGcdMultiplicity_sum {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDedekindDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [Algebra.IsIntegral (PlaneCurveCoordinateRing f) B] [FaithfulSMul (PlaneCurveCoordinateRing f) B] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] [IsFractionRing B (PlaneCurveFunctionField f)] (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) : Fintype.card (TorusCurveTorsionPoint f firstOrder secondOrder) ≤ ∑ v ∈ torsionGcdPlaceSupport firstOrder secondOrder, torsionGcdMultiplicity firstOrder secondOrder v

The torsion-point count is bounded by the finite sum of local gcd multiplicities on any Dedekind normalization model.