Leading-term cancellation at a Dedekind DVR place

At a discrete valuation place, two nonzero functions of the same order have unit leading coefficients. If the derivation-constant field surjects onto the residue field, one can subtract a constant multiple of one function from the other and cancel that leading coefficient. The result either vanishes or has strictly larger order.

This is the global-Dedekind analogue of the Laurent-series cancellation used in Corvaja--Zannier case (i). The surjectivity hypothesis is stated directly on the residue field, so the theorem can be applied independently of how the constant field is presented.

theorem BGS.CorvajaZannier.one_le_finitePlaceOrder_algebraMap_of_mem {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing 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)

A nonzero regular element lying in the place has positive order.

theorem BGS.CorvajaZannier.exists_constant_unit_sub_mul_mem {C : Type u_1} {R : Type u_2} [Field C] [CommRing R] [Algebra C R] (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap C v.asIdeal.ResidueField)) (u w : Rˣ) : ∃ (c : C), ↑u - (algebraMap C R) c * ↑w ∈ v.asIdeal

Residue-field surjectivity lets constants cancel the ratio of two unit leading coefficients.

theorem BGS.CorvajaZannier.exists_constant_finitePlaceOrder_sub_mul_eq_zero_or_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) (hx : x ≠ 0) (hy : y ≠ 0) (horder : finitePlaceOrder v x = finitePlaceOrder v y) : ∃ (c : C), x - (algebraMap C L) c * y = 0 ∨ finitePlaceOrder v x < finitePlaceOrder v (x - (algebraMap C L) c * y)

If constants surject onto the residue field at v, equal-order nonzero functions have a constant leading-term cancellation. The cancelled function is either zero or has strictly larger finite-place order.

No uniformizer is part of the interface: one is chosen internally from the DVR structure, and uniqueness of the maximal ideal identifies it with v.

theorem BGS.CorvajaZannier.exists_frobeniusSubfield_constant_finitePlaceOrder_sub_mul_eq_zero_or_lt {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] {K : Type u_4} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K R] [Algebra K L] [IsScalarTower K R L] (v : IsDedekindDomain.HeightOneSpectrum R) (hresidue : Function.Surjective ⇑(algebraMap K 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)

Over a perfect field of constants, the cancelling coefficient may be regarded as an element of the Frobenius subfield L^p, which is the constant field of the separating derivation used by Corvaja--Zannier.

The residue-surjectivity hypothesis is deliberately imposed on the genuine constant field K: the full subfield L^p is not contained in a nontrivial valuation ring. Perfectness embeds K into L^p, and this is exactly enough to make the column operation linear over the derivation-constant field.