Corvaja--Zannier case (i) over a perfect residue field

The usual leading-coefficient cancellation in local case (i) does not require the global constant field to surject onto the residue field. In characteristic p, it is enough that the residue field is perfect. Given the ratio of two unit leading coefficients, choose its p-th root in the residue field, lift that root to the DVR, and use the p-th power of the lift. This coefficient is regular and belongs to the Frobenius subfield of the fraction field, hence is killed by the separating derivation.

This file packages that argument and then repeats the determinant-one elimination from DedekindAuxiliaryCaseI with coefficients in the Frobenius subfield. No algebra structure from the whole Frobenius subfield to the DVR is asserted: such a structure would be false at a nontrivial place.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_regular_unit_sub_mul_mem_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (u w : Rˣ) : ∃ (c : ↥(frobeniusSubfield L p)) (b : R), (algebraMap (↥(frobeniusSubfield L p)) L) c = (algebraMap R L) b ∧ ↑u - b * ↑w ∈ v.asIdeal

Over a perfect residue field, the ratio of two unit leading coefficients can be cancelled by a regular element whose image in the fraction field is a p-th power.

The extra witness b : R records regularity of the coefficient; its image in L is the coefficient represented by c : L^p.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_finitePlaceOrder_sub_mul_eq_zero_or_lt_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (horder : finitePlaceOrder v x = finitePlaceOrder v y) : ∃ (c : ↥(frobeniusSubfield L p)), x - (algebraMap (↥(frobeniusSubfield L p)) L) c * y = 0 ∨ finitePlaceOrder v x < finitePlaceOrder v (x - (algebraMap (↥(frobeniusSubfield L p)) L) c * y)

Equal-order nonzero functions admit a strict leading-term cancellation with a coefficient in the Frobenius subfield whenever the residue field is perfect.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_dedekindPoleDepth_sub_mul_lt_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (x y : L) (hxneg : finitePlaceOrderTop v x < 0) (hyneg : finitePlaceOrderTop v y < 0) (horder : finitePlaceOrderTop v x = finitePlaceOrderTop v y) : ∃ (c : ↥(frobeniusSubfield L p)), dedekindPoleDepth v (x - (algebraMap (↥(frobeniusSubfield L p)) L) c * y) < dedekindPoleDepth v x ∧ finitePlaceOrderTop v x < finitePlaceOrderTop v (x - (algebraMap (↥(frobeniusSubfield L p)) L) c * y)

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

theorem BGS.CorvajaZannier.exists_det_one_frobeniusSubfield_columnMatrix_negativeOrdersPairwiseDistinct_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] {k : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (a : ℤ) (f : Fin k → L) (hf : ∀ (i : Fin k), ↑a ≤ finitePlaceOrderTop v (f i)) : ∃ (A : Matrix (Fin k) (Fin k) ↥(frobeniusSubfield L p)), 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 over the Frobenius subfield by a determinant-one matrix when the residue field is perfect.

Unlike the constant-field version, this theorem does not require an algebra map from the coefficient field to the DVR.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_dedekindCaseI_columnMatrix_and_q_wronskian_bound_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] {k : ℕ} (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (D : Derivation (↥(frobeniusSubfield L p)) 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) ↥(frobeniusSubfield L p)), 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 a Fin k family, with coefficients in the Frobenius subfield and no residue-surjectivity assumption.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_dedekindLocalAuxiliaryFamily_caseI_columnMatrix_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField 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) ↥(frobeniusSubfield L p)), 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 over the Frobenius subfield. Perfectness of the residue field replaces surjectivity from a global constant field.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_dedekindLocalAuxiliaryFamily_caseI_q_wronskian_bound_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (D : Derivation (↥(frobeniusSubfield L p)) 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) ↥(frobeniusSubfield L p)), 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) over the Frobenius subfield: perfect residue fields supply every leading-term cancellation, the determinant-one column operation preserves the Wronskian, and the exact q * ord(rho) lower bound follows.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_dedekindAuxiliaryFamily_caseI_q_wronskian_bound_of_perfect_residue {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] [CharP L p] (v : IsDedekindDomain.HeightOneSpectrum R) [PerfectField v.asIdeal.ResidueField] (D : Derivation (↥(frobeniusSubfield L p)) 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) ↥(frobeniusSubfield L p)), 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

Source auxiliaryFamily endpoint, specialized to rho = (1-u)/(1-w), over a perfect residue field.