Torsion points and the exhaustive gcd divisor

The affine normalization used in TorsionGcdDivisorBound need not be finite over the polynomial ring defining the selected K(X)-model. This file bridges that mismatch without assuming an algebra map between the two normalizations. A valuation subring dominating the affine local ring of a torsion point determines a height-one prime in the finite integral closure of K[X]. Distinct affine points determine distinct valuation subrings, hence distinct finite places. Both powered coordinate functions have positive order there.

Consequently rational torsion points inject into the finite part of the exhaustive place type. Each selected place contributes at least one to the degree-weighted positive gcd divisor used by the global Wronskian argument.

noncomputable def BGS.CorvajaZannier.fractionEmbeddingRangeEquiv {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] : A ≃+* ↥(algebraMap A L).range

The fraction-field embedding, with codomain restricted to its range.

Equations

• BGS.CorvajaZannier.fractionEmbeddingRangeEquiv = RingEquiv.ofBijective (algebraMap A L).rangeRestrict ⋯

noncomputable def BGS.CorvajaZannier.maximalIdealInFractionEmbeddingRange {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] (m : MaximalSpectrum A) : Ideal ↥(algebraMap A L).range

The image of a maximal ideal inside the embedded copy of A in L.

Equations

• BGS.CorvajaZannier.maximalIdealInFractionEmbeddingRange m = Ideal.map BGS.CorvajaZannier.fractionEmbeddingRangeEquiv.toRingHom m.asIdeal

noncomputable def BGS.CorvajaZannier.dominatingValuationSubring {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] (m : MaximalSpectrum A) : ValuationSubring L

A valuation subring of the fraction field dominating the affine local ring at m.

Equations

• BGS.CorvajaZannier.dominatingValuationSubring m = Classical.choose ⋯

theorem BGS.CorvajaZannier.range_le_dominatingValuationSubring {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] (m : MaximalSpectrum A) : (algebraMap A L).range ≤ (dominatingValuationSubring m).toSubring

theorem BGS.CorvajaZannier.algebraMap_mem_dominatingValuationSubring_nonunits_of_mem {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] (m : MaximalSpectrum A) (r : A) (hr : r ∈ m.asIdeal) : (algebraMap A L) r ∈ (dominatingValuationSubring m).nonunits

noncomputable def BGS.CorvajaZannier.coordinateRingToDominatingValuationSubring {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] (m : MaximalSpectrum A) : A →+* ↥(dominatingValuationSubring m)

The affine ring map into its dominating valuation subring.

Equations

• BGS.CorvajaZannier.coordinateRingToDominatingValuationSubring m = (Subring.inclusion ⋯).comp (algebraMap A L).rangeRestrict

theorem BGS.CorvajaZannier.pointIdeal_eq_comap_dominatingValuationSubring_maximalIdeal {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] (m : MaximalSpectrum A) : m.asIdeal = Ideal.comap (coordinateRingToDominatingValuationSubring m) (IsLocalRing.maximalIdeal ↥(dominatingValuationSubring m))

theorem BGS.CorvajaZannier.pointIdeal_eq_of_dominatingValuationSubring_eq {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {m n : MaximalSpectrum A} (h : dominatingValuationSubring m = dominatingValuationSubring n) : m.asIdeal = n.asIdeal

Equality of the chosen dominating valuation subrings forces equality of the affine centers.

theorem BGS.CorvajaZannier.integralClosure_le_dominatingValuationSubring {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) : (integralClosure P L).toSubring ≤ (dominatingValuationSubring m).toSubring

noncomputable def BGS.CorvajaZannier.integralClosureToDominatingValuationSubring {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) : ↥(integralClosure P L) →+* ↥(dominatingValuationSubring m)

The finite integral closure maps into the valuation subring because the selected polynomial base is already contained in the affine ring.

Equations

• BGS.CorvajaZannier.integralClosureToDominatingValuationSubring m hbase = Subring.inclusion ⋯

noncomputable def BGS.CorvajaZannier.dominatingIntegralClosurePrime {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) : Ideal ↥(integralClosure P L)

The center of the dominating valuation on the finite integral closure.

Equations

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

theorem BGS.CorvajaZannier.dominatingIntegralClosurePrime_isPrime {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) : (dominatingIntegralClosurePrime m hbase).IsPrime

noncomputable def BGS.CorvajaZannier.dominatingIntegralClosurePlace {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) (hne : dominatingIntegralClosurePrime m hbase ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure P L)

A nonzero center in the finite integral closure, regarded as a finite place.

Equations

• BGS.CorvajaZannier.dominatingIntegralClosurePlace m hbase hne = { asIdeal := BGS.CorvajaZannier.dominatingIntegralClosurePrime m hbase, isPrime := ⋯, ne_bot := hne }

theorem BGS.CorvajaZannier.valuationSubringAt_dominatingIntegralClosurePlace_le {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] [IsDedekindDomain ↥(integralClosure P L)] [IsFractionRing (↥(integralClosure P L)) L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) (hne : dominatingIntegralClosurePrime m hbase ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L (dominatingIntegralClosurePlace m hbase hne) ≤ dominatingValuationSubring m

theorem BGS.CorvajaZannier.valuationSubringAt_dominatingIntegralClosurePlace_eq {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] [IsDedekindDomain ↥(integralClosure P L)] [IsFractionRing (↥(integralClosure P L)) L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) (hne : dominatingIntegralClosurePrime m hbase ≠ ⊥) (hV : dominatingValuationSubring m ≠ ⊤) : IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L (dominatingIntegralClosurePlace m hbase hne) = dominatingValuationSubring m

theorem BGS.CorvajaZannier.dominatingIntegralClosurePlace_valuation_isEquiv {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] [IsDedekindDomain ↥(integralClosure P L)] [IsFractionRing (↥(integralClosure P L)) L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) (hne : dominatingIntegralClosurePrime m hbase ≠ ⊥) (hV : dominatingValuationSubring m ≠ ⊤) : (IsDedekindDomain.HeightOneSpectrum.valuation L (dominatingIntegralClosurePlace m hbase hne)).IsEquiv (dominatingValuationSubring m).valuation

theorem BGS.CorvajaZannier.finitePlaceOrder_dominatingIntegralClosurePlace_pos_of_mem {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] [IsDedekindDomain ↥(integralClosure P L)] [IsFractionRing (↥(integralClosure P L)) L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) (hne : dominatingIntegralClosurePrime m hbase ≠ ⊥) (hV : dominatingValuationSubring m ≠ ⊤) (r : A) (hr : r ∈ m.asIdeal) (hr0 : (algebraMap A L) r ≠ 0) : 0 < finitePlaceOrder (dominatingIntegralClosurePlace m hbase hne) ((algebraMap A L) r)

theorem BGS.CorvajaZannier.exists_integralClosurePlace_orders_positive {A : Type u_1} {L : Type u_2} [CommRing A] [Field L] [Algebra A L] [IsFractionRing A L] {P : Type u_3} [CommRing P] [Algebra P L] [IsDedekindDomain ↥(integralClosure P L)] [IsFractionRing (↥(integralClosure P L)) L] (m : MaximalSpectrum A) (hbase : ∀ (p : P), (algebraMap P L) p ∈ (algebraMap A L).range) (r s : A) (hr : r ∈ m.asIdeal) (hs : s ∈ m.asIdeal) (hr0 : (algebraMap A L) r ≠ 0) (hs0 : (algebraMap A L) s ≠ 0) (b : ↥(integralClosure P L)) (hb : (algebraMap (↥(integralClosure P L)) L) b = (algebraMap A L) r) : ∃ (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure P L)), IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L q = dominatingValuationSubring m ∧ 0 < finitePlaceOrder q ((algebraMap A L) r) ∧ 0 < finitePlaceOrder q ((algebraMap A L) s)

A nonzero integral element at a maximal ideal gives a centered finite place where both prescribed elements have positive order.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.exhaustiveGcdPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from (Polynomial K) to L used in the torsion exhaustive gcd divisor bound construction.

Equations

• BGS.CorvajaZannier.exhaustiveGcdPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.exhaustiveGcdPolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.CorvajaZannier.exhaustiveGcdFiniteIntegralClosureIsDedekindDomain (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.exhaustiveGcdFiniteIntegralClosureIsFractionRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncFiniteIntegralClosure K L)) L

theorem BGS.CorvajaZannier.exhaustiveGcdFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

noncomputable def BGS.CorvajaZannier.finiteExtensionGcdSupport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) : Finset (FiniteExtensionPlace K L)

Common finite support of the two principal divisors on the exhaustive place type.

Equations

• BGS.CorvajaZannier.finiteExtensionGcdSupport K L x y = (BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L x).support ∪ (BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L y).support

noncomputable def BGS.CorvajaZannier.finiteExtensionGcdMultiplicity (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (v : FiniteExtensionPlace K L) : ℕ

Positive local gcd multiplicity of two nonzero rational functions.

Equations

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

noncomputable def BGS.CorvajaZannier.finiteExtensionGcdWeightedDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) : ℕ

Degree of the positive gcd divisor on the exhaustive place type.

Equations

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

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_inl_eq_finitePlaceOrder (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (q : FiniteExtensionFinitePlace K L) : (finiteExtensionPrincipalDivisor K L x) (Sum.inl q) = finitePlaceOrder q x

On a finite place, the exhaustive principal-divisor coefficient is the normalized order computed directly in L.

theorem BGS.CorvajaZannier.finiteExtensionPlaceDegree_inl_pos (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (q : FiniteExtensionFinitePlace K L) : 0 < finiteExtensionPlaceDegree K L (Sum.inl q)

theorem BGS.CorvajaZannier.inl_mem_finiteExtensionGcdSupport_of_orders_positive (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (q : FiniteExtensionFinitePlace K L) (hxpos : 0 < finitePlaceOrder q x) : Sum.inl q ∈ finiteExtensionGcdSupport K L x y

theorem BGS.CorvajaZannier.one_le_finiteExtensionGcdMultiplicity_mul_degree_inl_of_orders_positive (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (q : FiniteExtensionFinitePlace K L) (hxpos : 0 < finitePlaceOrder q x) (hypos : 0 < finitePlaceOrder q y) : 1 ≤ finiteExtensionGcdMultiplicity K L x y (Sum.inl q) * finiteExtensionPlaceDegree K L (Sum.inl q)

theorem BGS.CorvajaZannier.polynomial_algebraMap_mem_planeCurveCoordinateRing_range {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (P : Polynomial K) : have hx := ⋯; (algebraMap (Polynomial K) (PlaneCurveFunctionField f)) P ∈ (algebraMap (PlaneCurveCoordinateRing f) (PlaneCurveFunctionField f)).range

The selected polynomial parameter belongs to the affine coordinate ring inside the curve's function field.

theorem BGS.CorvajaZannier.exists_torsionPoint_exhaustiveFinitePlace_orders_positive {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [Fintype K] [DecidableEq K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : have this := ⋯; have hx := ⋯; let this_1 := planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; have this_6 := ⋯; have this_7 := ⋯; ∃ (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial K) (PlaneCurveFunctionField f))), IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (PlaneCurveFunctionField f) q = dominatingValuationSubring (torsionPointMaximalIdeal f firstOrder secondOrder z) ∧ 0 < finitePlaceOrder q (planeCurveFunction f 0 ^ firstOrder - 1) ∧ 0 < finitePlaceOrder q (planeCurveFunction f 1 ^ secondOrder - 1)

Every rational torsion point produces an actual finite place of the K[X] integral-closure model at which both powered coordinate functions have positive order. The valuation-subring equality records its affine center and will make the choice injective.

noncomputable def BGS.CorvajaZannier.torsionPointExhaustiveFinitePlace {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [Fintype K] [DecidableEq K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : have hx := ⋯; FiniteExtensionFinitePlace K (PlaneCurveFunctionField f)

The finite place in the exhaustive K[X]-integral-closure model selected above a rational torsion point.

Equations

• BGS.CorvajaZannier.torsionPointExhaustiveFinitePlace hf hpartialSecond firstOrder secondOrder hfirstNonzero hsecondNonzero z = Classical.choose ⋯

theorem BGS.CorvajaZannier.torsionPointExhaustiveFinitePlace_spec {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [Fintype K] [DecidableEq K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) (z : TorusCurveTorsionPoint f firstOrder secondOrder) : have hx := ⋯; IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (PlaneCurveFunctionField f) (torsionPointExhaustiveFinitePlace hf hpartialSecond firstOrder secondOrder hfirstNonzero hsecondNonzero z) = dominatingValuationSubring (torsionPointMaximalIdeal f firstOrder secondOrder z) ∧ 0 < finitePlaceOrder (torsionPointExhaustiveFinitePlace hf hpartialSecond firstOrder secondOrder hfirstNonzero hsecondNonzero z) (planeCurveFunction f 0 ^ firstOrder - 1) ∧ 0 < finitePlaceOrder (torsionPointExhaustiveFinitePlace hf hpartialSecond firstOrder secondOrder hfirstNonzero hsecondNonzero z) (planeCurveFunction f 1 ^ secondOrder - 1)

The selected exhaustive finite place is centered at the given affine torsion point, and both powered coordinate functions have positive order there.

theorem BGS.CorvajaZannier.torsionPointExhaustiveFinitePlace_injective {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [Fintype K] [DecidableEq K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) : have hx := ⋯; Function.Injective (torsionPointExhaustiveFinitePlace hf hpartialSecond firstOrder secondOrder hfirstNonzero hsecondNonzero)

Distinct rational torsion points have distinct selected finite places in the exhaustive K[X]-model.

noncomputable def BGS.CorvajaZannier.planeCurveExhaustiveTorsionGcdWeightedDegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [DecidableEq K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (firstOrder secondOrder : ℕ) : ℕ

Degree of the positive gcd divisor of the two powered coordinate functions, taken on the exhaustive finite-and-infinite place model attached to the first coordinate.

Equations

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

theorem BGS.CorvajaZannier.torsionPoint_card_le_planeCurveExhaustiveTorsionGcdWeightedDegree {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} [Fintype K] [DecidableEq K] (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (firstOrder secondOrder : ℕ) (hfirstNonzero : planeCurveFunction f 0 ^ firstOrder - 1 ≠ 0) (hsecondNonzero : planeCurveFunction f 1 ^ secondOrder - 1 ≠ 0) : Fintype.card (TorusCurveTorsionPoint f firstOrder secondOrder) ≤ planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond firstOrder secondOrder

Rational torsion points inject into the positive gcd divisor on the exhaustive place model. The residue-degree weight of every selected place is positive, so each point contributes at least one to its weighted degree.