Corvaja--Zannier case (i) at a Dedekind DVR place

This file transports the repeated-leading-term cancellation argument of Corvaja--Zannier's local case (i) from Laurent series to the fraction field of a discrete valuation ring. Constants are assumed to surject onto the residue field. This is precisely the input needed to cancel equal-order leading terms; no coefficient field or completion is chosen.

The Wronskian estimate only assumes that the derivation preserves the DVR. In particular, a column of nonnegative order and every one of its iterated derivatives remain regular. Combining this with determinant-one elimination gives the source bound q * ord(rho) for the full auxiliary family.

Source provenance: published pages 1935--1936; checked semantic reconstruction Papers/CorvajaZannier2013/CorvajaZannier2013.tex, lines 640--685.

noncomputable def BGS.CorvajaZannier.dedekindPoleDepth {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) : ℕ

The depth of the pole of x at v; zero has pole depth zero.

Equations

• BGS.CorvajaZannier.dedekindPoleDepth v x = if x = 0 then 0 else (-BGS.CorvajaZannier.finitePlaceOrder v x).toNat

noncomputable def BGS.CorvajaZannier.dedekindPoleWeight {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] {k : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) (f : Fin k → L) : ℕ

A terminating measure for repeated leading-term cancellation.

Equations

• BGS.CorvajaZannier.dedekindPoleWeight v f = ∑ i : Fin k, BGS.CorvajaZannier.dedekindPoleDepth v (f i)

@[simp]

theorem BGS.CorvajaZannier.dedekindPoleDepth_zero {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) : dedekindPoleDepth v 0 = 0

def BGS.CorvajaZannier.NegativeFinitePlaceOrdersPairwiseDistinct {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] {ι : Type u_4} (v : IsDedekindDomain.HeightOneSpectrum R) (f : ι → L) : Prop

All negative finite-place orders in a family are pairwise distinct.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.dedekindPoleDepth_pos_iff {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) : 0 < dedekindPoleDepth v x ↔ finitePlaceOrderTop v x < 0

@[simp]

theorem BGS.CorvajaZannier.dedekindPoleDepth_eq_zero_iff {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) : dedekindPoleDepth v x = 0 ↔ 0 ≤ finitePlaceOrderTop v x

theorem BGS.CorvajaZannier.exists_constant_dedekindPoleDepth_sub_mul_lt {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (x y : L) (hxneg : finitePlaceOrderTop v x < 0) (hyneg : finitePlaceOrderTop v y < 0) (horder : finitePlaceOrderTop v x = finitePlaceOrderTop v y) : ∃ (c : C), dedekindPoleDepth v (x - (algebraMap C L) c * y) < dedekindPoleDepth v x ∧ finitePlaceOrderTop v x < finitePlaceOrderTop v (x - (algebraMap C L) c * y)

Equal negative orders have a constant cancellation which strictly lowers the pole-depth measure.

theorem BGS.CorvajaZannier.indexedDedekindLocalColumnCombination_mul {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] {k : ℕ} (f : Fin k → L) (A B : Matrix (Fin k) (Fin k) C) : indexedDedekindLocalColumnCombination (indexedDedekindLocalColumnCombination f A) B = indexedDedekindLocalColumnCombination f (A * B)

Successive constant column combinations compose by matrix multiplication.

theorem BGS.CorvajaZannier.exists_det_one_dedekindColumnMatrix_negativeOrdersPairwiseDistinct {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] {k : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (a : ℤ) (f : Fin k → L) (hf : ∀ (i : Fin k), ↑a ≤ finitePlaceOrderTop v (f i)) : ∃ (A : Matrix (Fin k) (Fin k) C), A.det = 1 ∧ NegativeFinitePlaceOrdersPairwiseDistinct v (indexedDedekindLocalColumnCombination f A) ∧ ∀ (i : Fin k), ↑a ≤ finitePlaceOrderTop v (indexedDedekindLocalColumnCombination f A i)

Repeated equal negative orders can be eliminated by a determinant-one constant matrix, while preserving a common lower order bound.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_derivation_iterate_nonnegative_of_nonnegative {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra C L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (m : ℕ) (x : L) (hx : 0 ≤ finitePlaceOrderTop v x) : 0 ≤ finitePlaceOrderTop v ((⇑D)^[m] x)

A DVR-preserving derivation and all of its iterates preserve the nonnegative-order part of the fraction field.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_det_lower_bound_of_poles {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra C L] [IsFractionRing R L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (epsilonOrder : ι → ℕ) (g : ι → L) (poles : Finset ι) (E : ℤ) (hpole : ∀ i ∈ poles, finitePlaceOrderTop v (g i) < 0) (hregular : ∀ i ∉ poles, 0 ≤ finitePlaceOrderTop v (g i)) (hselected : ∀ (σ : Equiv.Perm ι), ∑ i ∈ poles, ↑(epsilonOrder (σ i)) ≤ E) : ↑(∑ i ∈ poles, finitePlaceOrder v (g i) - E) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D epsilonOrder g).det

In a DVR-preserving Wronskian, only the pole columns pay a derivative order cost.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_caseI_epsilon_plus_one_lower_bound {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra C L] [IsFractionRing R L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (epsilonOrder : ι → ℕ) (g : ι → L) (rhoOrder : ℤ) (epsilon : ℕ) (hgdistinct : NegativeFinitePlaceOrdersPairwiseDistinct v g) (hglower : ∀ (i : ι), ↑rhoOrder ≤ finitePlaceOrderTop v (g i)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : ι), epsilonOrder i ≤ epsilon) (hcardRho : rhoOrder ≤ -↑{i : ι | finitePlaceOrderTop v (g i) < 0}.card) (hcardEpsilon : {i : ι | finitePlaceOrderTop v (g i) < 0}.card ≤ epsilon + 1) : ↑(rhoOrder * ↑(epsilon + 1)) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D epsilonOrder g).det

The exact intermediate case-(i) estimate at a Dedekind DVR place.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_caseI_q_lower_bound {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra C L] [IsFractionRing R L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (epsilonOrder : ι → ℕ) (g : ι → L) (rhoOrder : ℤ) (epsilon q : ℕ) (hgdistinct : NegativeFinitePlaceOrdersPairwiseDistinct v g) (hglower : ∀ (i : ι), ↑rhoOrder ≤ finitePlaceOrderTop v (g i)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : ι), epsilonOrder i ≤ epsilon) (hcardRho : rhoOrder ≤ -↑{i : ι | finitePlaceOrderTop v (g i) < 0}.card) (hcardEpsilon : {i : ι | finitePlaceOrderTop v (g i) < 0}.card ≤ epsilon + 1) (hrho : rhoOrder ≤ 0) (hepsilonQ : epsilon + 1 ≤ q) : ↑(↑q * rhoOrder) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D epsilonOrder g).det

Source case (i), in the final q * rhoOrder form, at a Dedekind DVR place.

theorem BGS.CorvajaZannier.card_negativeFinitePlaceOrders_le_neg {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] {ι : Type u_4} [Fintype ι] (v : IsDedekindDomain.HeightOneSpectrum R) (g : ι → L) (a : ℤ) (ha : a ≤ 0) (hgdistinct : NegativeFinitePlaceOrdersPairwiseDistinct v g) (hglower : ∀ (i : ι), ↑a ≤ finitePlaceOrderTop v (g i)) : a ≤ -↑{i : ι | finitePlaceOrderTop v (g i) < 0}.card

Pairwise-distinct negative finite-place orders bounded below by a nonpositive integer are no more numerous than its pole depth.

theorem BGS.CorvajaZannier.exists_dedekindCaseI_columnMatrix_and_q_wronskian_bound {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] {k : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (epsilonOrder : Fin k → ℕ) (f : Fin k → L) (a : ℤ) (epsilon q : ℕ) (ha : a ≤ 0) (hf : ∀ (i : Fin k), ↑a ≤ finitePlaceOrderTop v (f i)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ q) : ∃ (A : Matrix (Fin k) (Fin k) C), A.det = 1 ∧ (indexedDedekindLocalWronskian D epsilonOrder (indexedDedekindLocalColumnCombination f A)).det = (indexedDedekindLocalWronskian D epsilonOrder f).det ∧ ↑(↑q * a) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D epsilonOrder f).det

Complete local case (i) for an arbitrary Fin k fraction-field family.

def BGS.CorvajaZannier.dedekindCaseIColumnMatrix {C : Type u_1} [Field C] (h k : ℕ) (A : Matrix (Fin k) (Fin k) C) : Matrix (Fin k ⊕ Fin (k + 1) × Fin h) (Fin k ⊕ Fin (k + 1) × Fin h) C

Extend a first-block operation by the identity on the grid columns.

Equations

• BGS.CorvajaZannier.dedekindCaseIColumnMatrix h k A = Matrix.fromBlocks A 0 0 1

theorem BGS.CorvajaZannier.dedekindCaseIColumnMatrix_det {C : Type u_1} [Field C] (h k : ℕ) (A : Matrix (Fin k) (Fin k) C) : (dedekindCaseIColumnMatrix h k A).det = A.det

theorem BGS.CorvajaZannier.indexedDedekindLocalColumnCombination_dedekindCaseIColumnMatrix_inl {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] (h k : ℕ) (f : Fin k ⊕ Fin (k + 1) × Fin h → L) (A : Matrix (Fin k) (Fin k) C) (i : Fin k) : indexedDedekindLocalColumnCombination f (dedekindCaseIColumnMatrix h k A) (Sum.inl i) = indexedDedekindLocalColumnCombination (fun (j : Fin k) => f (Sum.inl j)) A i

theorem BGS.CorvajaZannier.indexedDedekindLocalColumnCombination_dedekindCaseIColumnMatrix_inr {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] (h k : ℕ) (f : Fin k ⊕ Fin (k + 1) × Fin h → L) (A : Matrix (Fin k) (Fin k) C) (rs : Fin (k + 1) × Fin h) : indexedDedekindLocalColumnCombination f (dedekindCaseIColumnMatrix h k A) (Sum.inr rs) = f (Sum.inr rs)

def BGS.CorvajaZannier.dedekindCaseITransformedLocalAuxiliaryFamily {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] (u w rho : L) (h k : ℕ) (A : Matrix (Fin k) (Fin k) C) : Fin k ⊕ Fin (k + 1) × Fin h → L

The full Dedekind-local auxiliary family after eliminating repeated orders in its first block.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.dedekindCaseITransformedLocalAuxiliaryFamily_inl {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] (u w rho : L) (h k : ℕ) (A : Matrix (Fin k) (Fin k) C) (i : Fin k) : dedekindCaseITransformedLocalAuxiliaryFamily u w rho h k A (Sum.inl i) = indexedDedekindLocalColumnCombination (fun (j : Fin k) => dedekindLocalAuxiliaryFamily u w rho h k (Sum.inl j)) A i

@[simp]

theorem BGS.CorvajaZannier.dedekindCaseITransformedLocalAuxiliaryFamily_inr {C : Type u_1} {L : Type u_3} [Field C] [Field L] [Algebra C L] (u w rho : L) (h k : ℕ) (A : Matrix (Fin k) (Fin k) C) (rs : Fin (k + 1) × Fin h) : dedekindCaseITransformedLocalAuxiliaryFamily u w rho h k A (Sum.inr rs) = dedekindLocalAuxiliaryFamily u w rho h k (Sum.inr rs)

theorem BGS.CorvajaZannier.exists_dedekindLocalAuxiliaryFamily_caseI_columnMatrix {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (u w rho : L) (h k : ℕ) (hrhoNe : rho ≠ 0) (huOrder : finitePlaceOrderTop v u = 0) (hrhoOrder : finitePlaceOrder v rho < 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ finitePlaceOrderTop v (u ^ ↑rs.1 * w ^ ↑rs.2)) : ∃ (A : Matrix (Fin k) (Fin k) C), A.det = 1 ∧ NegativeFinitePlaceOrdersPairwiseDistinct v (dedekindCaseITransformedLocalAuxiliaryFamily u w rho h k A) ∧ (∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), ↑(finitePlaceOrder v rho) ≤ finitePlaceOrderTop v (dedekindCaseITransformedLocalAuxiliaryFamily u w rho h k A i)) ∧ ∀ (rs : Fin (k + 1) × Fin h), dedekindCaseITransformedLocalAuxiliaryFamily u w rho h k A (Sum.inr rs) = dedekindLocalAuxiliaryFamily u w rho h k (Sum.inr rs)

Source-facing case-(i) elimination for the full auxiliary family. The ratio block starts at the common negative order of rho, while the grid columns are assumed regular.

theorem BGS.CorvajaZannier.exists_dedekindLocalAuxiliaryFamily_caseI_q_wronskian_bound {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (u w rho : L) (h k : ℕ) (epsilonOrder : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (epsilon q : ℕ) (hrhoNe : rho ≠ 0) (huOrder : finitePlaceOrderTop v u = 0) (hrhoOrder : finitePlaceOrder v rho < 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ finitePlaceOrderTop v (u ^ ↑rs.1 * w ^ ↑rs.2)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ q) : ∃ (A : Matrix (Fin k) (Fin k) C), A.det = 1 ∧ (indexedDedekindLocalWronskian D epsilonOrder (dedekindCaseITransformedLocalAuxiliaryFamily u w rho h k A)).det = (indexedDedekindLocalWronskian D epsilonOrder (dedekindLocalAuxiliaryFamily u w rho h k)).det ∧ ↑(↑q * finitePlaceOrder v rho) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D epsilonOrder (dedekindLocalAuxiliaryFamily u w rho h k)).det

Full Dedekind-DVR case (i): determinant-one repeated cancellation on the first block preserves the original Wronskian and proves the exact q * ord(rho) lower bound.

theorem BGS.CorvajaZannier.exists_dedekindAuxiliaryFamily_caseI_q_wronskian_bound {C : Type u_1} {R : Type u_2} {L : Type u_3} [Field C] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra C R] [Algebra R L] [Algebra C L] [IsScalarTower C R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (u w : L) (h k : ℕ) (epsilonOrder : Fin k ⊕ Fin (k + 1) × Fin h → ℕ) (epsilon q : ℕ) (hrhoNe : (1 - u) / (1 - w) ≠ 0) (huOrder : finitePlaceOrderTop v u = 0) (hrhoOrder : finitePlaceOrder v ((1 - u) / (1 - w)) < 0) (hgridRegular : ∀ (rs : Fin (k + 1) × Fin h), 0 ≤ finitePlaceOrderTop v (u ^ ↑rs.1 * w ^ ↑rs.2)) (hepsilonInjective : Function.Injective epsilonOrder) (hepsilonMax : ∀ (i : Fin k ⊕ Fin (k + 1) × Fin h), epsilonOrder i ≤ epsilon) (hk : k ≤ epsilon + 1) (hepsilonQ : epsilon + 1 ≤ q) : ∃ (A : Matrix (Fin k) (Fin k) C), A.det = 1 ∧ (indexedDedekindLocalWronskian D epsilonOrder (indexedDedekindLocalColumnCombination (auxiliaryFamily u w h k) (dedekindCaseIColumnMatrix h k A))).det = (indexedDedekindLocalWronskian D epsilonOrder (auxiliaryFamily u w h k)).det ∧ ↑(↑q * finitePlaceOrder v ((1 - u) / (1 - w))) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D epsilonOrder (auxiliaryFamily u w h k)).det

The same endpoint for the source auxiliaryFamily, specialized to rho = (1-u)/(1-w).