Wronskian order estimates at a Dedekind DVR place

This file proves the determinant-level local estimate directly in a fraction field equipped with a height-one-place order. It avoids passage to Laurent series: the only local input is a DVR-preserving derivation which sends a chosen uniformizer to one.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_finset_prod {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] {ι : Type u_3} (v : IsDedekindDomain.HeightOneSpectrum R) (s : Finset ι) (g : ι → L) : finitePlaceOrderTop v (∏ i ∈ s, g i) = ∑ i ∈ s, finitePlaceOrderTop v (g i)

The order of a finite product is the sum of the orders, including zero factors via WithTop.

theorem BGS.CorvajaZannier.le_finitePlaceOrderTop_finset_sum_of_forall {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] {ι : Type u_3} (v : IsDedekindDomain.HeightOneSpectrum R) (b : WithTop ℤ) (s : Finset ι) (g : ι → L) (h : ∀ i ∈ s, b ≤ finitePlaceOrderTop v (g i)) : b ≤ finitePlaceOrderTop v (∑ i ∈ s, g i)

If every summand has order at least b, then their finite sum also has order at least b. This is the cancellation step in the determinant estimate.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_le_intCast_mul {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (z : ℤ) (x : L) : finitePlaceOrderTop v x ≤ finitePlaceOrderTop v (↑z * x)

Multiplication by an integer coefficient cannot decrease finite-place order. This handles the permutation signs in the Leibniz determinant formula.

def BGS.CorvajaZannier.indexedDedekindLocalWronskian {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} (D : Derivation C L L) (ε : ι → ℕ) (f : ι → L) : Matrix ι ι L

An indexed ordinary-derivation Wronskian over the fraction field. The function ε records the derivative order assigned to each row.

Equations

• BGS.CorvajaZannier.indexedDedekindLocalWronskian D ε f i j = (⇑D)^[ε i] (f j)

def BGS.CorvajaZannier.indexedDedekindLocalColumnCombination {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] (f : ι → L) (A : Matrix ι ι C) : ι → L

Apply a constant scalar matrix to the columns of an indexed fraction-field family.

Equations

• BGS.CorvajaZannier.indexedDedekindLocalColumnCombination f A j = ∑ i : ι, A i j • f i

theorem BGS.CorvajaZannier.indexedDedekindLocalWronskian_columnCombination {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] (D : Derivation C L L) (ε : ι → ℕ) (f : ι → L) (A : Matrix ι ι C) : indexedDedekindLocalWronskian D ε (indexedDedekindLocalColumnCombination f A) = indexedDedekindLocalWronskian D ε f * A.map ⇑(algebraMap C L)

Constant column operations commute with the indexed DVR Wronskian.

theorem BGS.CorvajaZannier.indexedDedekindLocalWronskian_det_columnCombination_of_det_eq_one {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (D : Derivation C L L) (ε : ι → ℕ) (f : ι → L) (A : Matrix ι ι C) (hA : A.det = 1) : (indexedDedekindLocalWronskian D ε (indexedDedekindLocalColumnCombination f A)).det = (indexedDedekindLocalWronskian D ε f).det

A determinant-one constant column operation preserves the indexed DVR Wronskian determinant.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_det_lower_bound_of_preserves {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (ε : ι → ℕ) (f : ι → L) : ∑ j : ι, finitePlaceOrderTop v (f j) + ↑(-∑ i : ι, ↑(ε i)) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D ε f).det

For any DVR-preserving derivation, the indexed Wronskian determinant has order at least the sum of its column orders minus the sum of its row derivative orders. Cancellation in the determinant expansion is included.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_det_lower_bound {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (_hDπ : D ((algebraMap R L) π) = 1) (ε : ι → ℕ) (f : ι → L) : ∑ j : ι, finitePlaceOrderTop v (f j) + ↑(-∑ i : ι, ↑(ε i)) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D ε f).det

The normalized-uniformizer form retained for compatibility with the existing local-parameter API.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_det_nonnegative_of_integral {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] {C : Type u_3} [Field C] [Algebra C 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) (ε : ι → ℕ) (f : ι → L) (hfIntegral : ∀ (j : ι), ∃ (r : R), f j = (algebraMap R L) r) : 0 ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D ε f).det

If every column is represented by an element of the DVR and the derivation preserves the DVR, then the indexed Wronskian determinant is regular. This is the direct DVR analogue of the regular local auxiliary case.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_dedekindLocalWronskian_det_lower_bound_after_columnCombination_of_preserves {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (ε : ι → ℕ) (f : ι → L) (A : Matrix ι ι C) (hA : A.det = 1) : ∑ j : ι, finitePlaceOrderTop v (indexedDedekindLocalColumnCombination f A j) + ↑(-∑ i : ι, ↑(ε i)) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D ε f).det

The indexed determinant estimate after a determinant-one constant column operation, assuming only that the derivation preserves the DVR.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_det_lower_bound_after_columnCombination {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (hDπ : D ((algebraMap R L) π) = 1) (ε : ι → ℕ) (f : ι → L) (A : Matrix ι ι C) (hA : A.det = 1) : ∑ j : ι, finitePlaceOrderTop v (indexedDedekindLocalColumnCombination f A j) + ↑(-∑ i : ι, ↑(ε i)) ≤ finitePlaceOrderTop v (indexedDedekindLocalWronskian D ε f).det

The indexed determinant estimate after a determinant-one constant column operation. This normalized form is retained for the local-parameter API.

theorem BGS.CorvajaZannier.indexedDedekindLocalWronskian_det_changeParameter {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {n : ℕ} (e : ι ≃ Fin n) (ε : ι → ℕ) (hε : ∀ (i : ι), ε i = ↑(e i)) (D E : Derivation C L L) (a : L) (hD : D = a • E) (f : ι → L) : (indexedDedekindLocalWronskian D ε f).det = a ^ n.choose 2 * (indexedDedekindLocalWronskian E ε f).det

Change of parameter for an indexed ordinary Wronskian whose derivative orders are 0, ..., n - 1, transported along an explicit equivalence.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_indexedDedekindLocalWronskian_det_lower_bound_of_scaled_preserves {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {n : ℕ} (e : ι ≃ Fin n) (ε : ι → ℕ) (hε : ∀ (i : ι), ε i = ↑(e i)) (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (c : L) (hScaledIntegral : ∀ (r : R), ∃ (s : R), (c • D) ((algebraMap R L) r) = (algebraMap R L) s) (f : ι → L) : ∑ j : ι, finitePlaceOrderTop v (f j) + ↑(-∑ i : ι, ↑(ε i)) ≤ n.choose 2 • finitePlaceOrderTop v c + finitePlaceOrderTop v (indexedDedekindLocalWronskian D ε f).det

Indexed scaled-derivation estimate. The equivalence certifies that the row orders are precisely the ordinary derivative orders, so the scalar costs the expected triangular exponent.

def BGS.CorvajaZannier.dedekindLocalWronskian {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (D : Derivation C L L) (f : Fin n → L) : Matrix (Fin n) (Fin n) L

The ordinary n × n Wronskian, with derivative orders 0, ..., n - 1.

Equations

• BGS.CorvajaZannier.dedekindLocalWronskian D f = BGS.CorvajaZannier.indexedDedekindLocalWronskian D (fun (i : Fin n) => ↑i) f

theorem BGS.CorvajaZannier.dedekindLocalWronskian_eq_derivationWronskian {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] (D : Derivation C L L) {n : ℕ} (f : Fin n → L) : dedekindLocalWronskian D f = Algebra.derivationWronskian D f

The direct Dedekind-local Wronskian is definitionally the ordinary derivation Wronskian used by the change-of-parameter theorem.

theorem BGS.CorvajaZannier.dedekindLocalWronskian_det_changeParameter {L : Type u_2} [Field L] {C : Type u_3} [Field C] [Algebra C L] (D E : Derivation C L L) (a : L) (hD : D = a • E) {n : ℕ} (f : Fin n → L) : (dedekindLocalWronskian D f).det = a ^ n.choose 2 * (dedekindLocalWronskian E f).det

Change of parameter for the direct Dedekind-local Wronskian. In particular this permits replacing a global derivation by a DVR-preserving scalar multiple while recording the exact triangular valuation cost.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_dedekindLocalWronskian_det_lower_bound_of_preserves {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (f : Fin n → L) : ∑ j : Fin n, finitePlaceOrderTop v (f j) + ↑(-↑(n * (n - 1) / 2)) ≤ finitePlaceOrderTop v (dedekindLocalWronskian D f).det

For a DVR-preserving derivation, the ordinary Wronskian loses at most the triangular number n * (n - 1) / 2 from the sum of its column orders.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_dedekindLocalWronskian_det_lower_bound_of_scaled_preserves {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (c : L) (hScaledIntegral : ∀ (r : R), ∃ (s : R), (c • D) ((algebraMap R L) r) = (algebraMap R L) s) (f : Fin n → L) : ∑ j : Fin n, finitePlaceOrderTop v (f j) + ↑(-↑(n * (n - 1) / 2)) ≤ n.choose 2 • finitePlaceOrderTop v c + finitePlaceOrderTop v (dedekindLocalWronskian D f).det

A scalar multiple of the ambient derivation may be used to obtain a DVR-preserving local derivation. The right side records exactly the order of the scalar to the Wronskian triangular exponent; no false formula for iterates of c • D is used.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_dedekindLocalWronskian_det_lower_bound {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] {C : Type u_3} [Field C] [Algebra C L] {n : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (D : Derivation C L L) (hDIntegral : ∀ (r : R), ∃ (s : R), D ((algebraMap R L) r) = (algebraMap R L) s) (hDπ : D ((algebraMap R L) π) = 1) (f : Fin n → L) : ∑ j : Fin n, finitePlaceOrderTop v (f j) + ↑(-↑(n * (n - 1) / 2)) ≤ finitePlaceOrderTop v (dedekindLocalWronskian D f).det

The ordinary Wronskian loses at most the triangular number n * (n - 1) / 2 from the sum of its column orders. This normalized form is retained for the local-parameter API.