Affine centers and normalization of torsion points

Construct coordinate-ring evaluations and their maximal ideals, and compare affine torsion points with normalization places.

@[reducible, inline]

abbrev BGS.CorvajaZannier.AffinePlaneCurvePoint {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Type u_1

An affine rational point of the plane curve f = 0.

Equations

• BGS.CorvajaZannier.AffinePlaneCurvePoint f = { z : K × K // (MvPolynomial.eval ![z.1, z.2]) f = 0 }

noncomputable def BGS.CorvajaZannier.planeCurvePointEval {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (z : AffinePlaneCurvePoint f) : PlaneCurveCoordinateRing f →+* K

Evaluation at an affine rational point, descended to the coordinate ring.

Equations

• BGS.CorvajaZannier.planeCurvePointEval f z = Ideal.Quotient.lift (Ideal.span {f}) (MvPolynomial.eval₂Hom (RingHom.id K) ![(↑z).1, (↑z).2]) ⋯

@[simp]

theorem BGS.CorvajaZannier.planeCurvePointEval_coordinate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (z : AffinePlaneCurvePoint f) (i : Fin 2) : (planeCurvePointEval f z) (planeCurveCoordinate f i) = ![(↑z).1, (↑z).2] i

@[simp]

theorem BGS.CorvajaZannier.planeCurvePointEval_algebraMap {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (z : AffinePlaneCurvePoint f) (c : K) : (planeCurvePointEval f z) ((algebraMap K (PlaneCurveCoordinateRing f)) c) = c

theorem BGS.CorvajaZannier.planeCurvePointEval_surjective {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (z : AffinePlaneCurvePoint f) : Function.Surjective ⇑(planeCurvePointEval f z)

noncomputable def BGS.CorvajaZannier.affinePlaneCurvePointMaximalIdeal {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (z : AffinePlaneCurvePoint f) : MaximalSpectrum (PlaneCurveCoordinateRing f)

The maximal ideal of the affine coordinate ring attached to a rational point.

Equations

• BGS.CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z = { asIdeal := RingHom.ker (BGS.CorvajaZannier.planeCurvePointEval f z), isMaximal := ⋯ }

theorem BGS.CorvajaZannier.affinePlaneCurvePointMaximalIdeal_injective {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Function.Injective (affinePlaneCurvePointMaximalIdeal f)

Distinct rational affine points define distinct maximal ideals.

@[reducible, inline]

abbrev BGS.CorvajaZannier.TorusCurveTorsionPoint {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) : Type u_1

A torsion point in the finite-field intersection, as a finite subtype.

Equations

• BGS.CorvajaZannier.TorusCurveTorsionPoint f firstOrder secondOrder = ↥(BGS.External.torusCurveTorsionIntersection K f firstOrder secondOrder)

def BGS.CorvajaZannier.torsionPointToAffinePlaneCurvePoint {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : AffinePlaneCurvePoint f

Forget the unit witnesses and regard a torsion point as an affine point of the plane curve.

Equations

• BGS.CorvajaZannier.torsionPointToAffinePlaneCurvePoint f firstOrder secondOrder z = ⟨(↑(↑z).1, ↑(↑z).2), ⋯⟩

theorem BGS.CorvajaZannier.torsionPointToAffinePlaneCurvePoint_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) : Function.Injective (torsionPointToAffinePlaneCurvePoint f firstOrder secondOrder)

noncomputable def BGS.CorvajaZannier.torsionPointMaximalIdeal {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : MaximalSpectrum (PlaneCurveCoordinateRing f)

A finite-field torsion point determines a maximal ideal of the affine coordinate ring.

Equations

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

theorem BGS.CorvajaZannier.torsionPointMaximalIdeal_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) : Function.Injective (torsionPointMaximalIdeal f firstOrder secondOrder)

theorem BGS.CorvajaZannier.first_torsionFunction_mem_torsionPointMaximalIdeal {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : planeCurveCoordinate f 0 ^ firstOrder - 1 ∈ (torsionPointMaximalIdeal f firstOrder secondOrder z).asIdeal

The first torsion function belongs to the maximal ideal of its point.

theorem BGS.CorvajaZannier.second_torsionFunction_mem_torsionPointMaximalIdeal {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : planeCurveCoordinate f 1 ^ secondOrder - 1 ∈ (torsionPointMaximalIdeal f firstOrder secondOrder z).asIdeal

The second torsion function belongs to the maximal ideal of its point.

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.PlaneCurveNormalization {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Subalgebra (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)

The affine normalization of the plane-curve coordinate ring inside its fraction field.

Equations

• BGS.CorvajaZannier.PlaneCurveNormalization f = integralClosure (BGS.CorvajaZannier.PlaneCurveCoordinateRing f) (BGS.CorvajaZannier.PlaneCurveFunctionField f)

noncomputable def BGS.CorvajaZannier.planeCurveNormalizationBranch {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m : MaximalSpectrum (PlaneCurveCoordinateRing f)) : MaximalSpectrum ↥(PlaneCurveNormalization f)

Choose one normalization branch above an affine maximal ideal. Lying over guarantees that such a branch exists; no smoothness is assumed.

Equations

• BGS.CorvajaZannier.planeCurveNormalizationBranch f m = { asIdeal := Classical.choose ⋯, isMaximal := ⋯ }

theorem BGS.CorvajaZannier.planeCurveNormalizationBranch_liesOver {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (m : MaximalSpectrum (PlaneCurveCoordinateRing f)) : (planeCurveNormalizationBranch f m).asIdeal.LiesOver m.asIdeal

theorem BGS.CorvajaZannier.planeCurveNormalizationBranch_injective {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] : Function.Injective (planeCurveNormalizationBranch f)

Chosen normalization branches above distinct affine maximal ideals remain distinct, because their contractions are distinct.

noncomputable def BGS.CorvajaZannier.torsionPointNormalizationBranch {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : MaximalSpectrum ↥(PlaneCurveNormalization f)

The chosen branch of the normalization above a torsion point.

Equations

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

theorem BGS.CorvajaZannier.torsionPointNormalizationBranch_injective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (firstOrder secondOrder : ℕ) : Function.Injective (torsionPointNormalizationBranch f firstOrder secondOrder)

theorem BGS.CorvajaZannier.first_torsionFunction_mem_normalizationBranch {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : (algebraMap (PlaneCurveCoordinateRing f) ↥(PlaneCurveNormalization f)) (planeCurveCoordinate f 0 ^ firstOrder - 1) ∈ (torsionPointNormalizationBranch f firstOrder secondOrder z).asIdeal

The first torsion function vanishes on the chosen normalization branch.

theorem BGS.CorvajaZannier.second_torsionFunction_mem_normalizationBranch {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) [IsDomain (PlaneCurveCoordinateRing f)] (firstOrder secondOrder : ℕ) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : (algebraMap (PlaneCurveCoordinateRing f) ↥(PlaneCurveNormalization f)) (planeCurveCoordinate f 1 ^ secondOrder - 1) ∈ (torsionPointNormalizationBranch f firstOrder secondOrder z).asIdeal

The second torsion function vanishes on the chosen normalization branch.

instance BGS.CorvajaZannier.planeCurveIntegralClosureIsFractionRing {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [IsDomain (PlaneCurveCoordinateRing f)] {B : Type u_2} [CommRing B] [IsDomain B] [Algebra (PlaneCurveCoordinateRing f) B] [Algebra B (PlaneCurveFunctionField f)] [IsScalarTower (PlaneCurveCoordinateRing f) B (PlaneCurveFunctionField f)] [IsIntegralClosure B (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)] : IsFractionRing B (PlaneCurveFunctionField f)

An integral-closure model of the plane-curve function field has that function field as its fraction field.

theorem BGS.CorvajaZannier.one_le_finitePlaceOrder_of_mem {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (a : R) (ha : a ∈ v.asIdeal) (ha0 : a ≠ 0) : 1 ≤ finitePlaceOrder v ((algebraMap R L) a)

Membership in a height-one prime gives at least one unit of additive finite-place order.

theorem BGS.CorvajaZannier.liftedNormalizationBranch_torsion_orders_positive {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)] [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) (branch : MaximalSpectrum B) (hbranch : branch.asIdeal.LiesOver (torsionPointMaximalIdeal f firstOrder secondOrder z).asIdeal) : ∃ (v : IsDedekindDomain.HeightOneSpectrum B), v.asIdeal = branch.asIdeal ∧ 1 ≤ finitePlaceOrder v (planeCurveFunction f 0 ^ firstOrder - 1) ∧ 1 ≤ finitePlaceOrder v (planeCurveFunction f 1 ^ secondOrder - 1) ∧ 1 ≤ min (finitePlaceOrder v (planeCurveFunction f 0 ^ firstOrder - 1)) (finitePlaceOrder v (planeCurveFunction f 1 ^ secondOrder - 1))

Generic local bridge for any Dedekind integral-closure model B of the curve's function field. A maximal ideal of B lying over the torsion point is a finite place, and both torsion functions have order at least one there.

The branch is an explicit parameter, so a later global normalization or projective model can supply its own chosen lift.