Orders at Dedekind places

Extend local orders to zero using a top value and prove their arithmetic and derivation estimates through uniformizers.

theorem BGS.CorvajaZannier.finitePlaceOrder_add_ge_min {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) : min (finitePlaceOrder v x) (finitePlaceOrder v y) ≤ finitePlaceOrder v (x + y)

The additive order at a finite place satisfies the ultrametric inequality on nonzero inputs.

noncomputable def BGS.CorvajaZannier.finitePlaceOrderTop {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) : WithTop ℤ

The order attached to a height-one prime, with the zero element assigned infinite order.

Equations

• BGS.CorvajaZannier.finitePlaceOrderTop v x = if x = 0 then ⊤ else ↑(BGS.CorvajaZannier.finitePlaceOrder v x)

@[simp]

theorem BGS.CorvajaZannier.finitePlaceOrderTop_zero {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) : finitePlaceOrderTop v 0 = ⊤

@[simp]

theorem BGS.CorvajaZannier.finitePlaceOrderTop_eq_top_iff {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) : finitePlaceOrderTop v x = ⊤ ↔ x = 0

theorem BGS.CorvajaZannier.finitePlaceOrderTop_eq_coe {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) (hx : x ≠ 0) : finitePlaceOrderTop v x = ↑(finitePlaceOrder v x)

theorem BGS.CorvajaZannier.finitePlaceOrderTop_add_ge_min {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : L) : min (finitePlaceOrderTop v x) (finitePlaceOrderTop v y) ≤ finitePlaceOrderTop v (x + y)

theorem BGS.CorvajaZannier.finitePlaceOrderTop_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) (x y : L) : finitePlaceOrderTop v (x * y) = finitePlaceOrderTop v x + finitePlaceOrderTop v y

@[simp]

theorem BGS.CorvajaZannier.finitePlaceOrderTop_one {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) : finitePlaceOrderTop v 1 = 0

theorem BGS.CorvajaZannier.finitePlaceOrderTop_pow {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (x : L) (n : ℕ) : finitePlaceOrderTop v (x ^ n) = n • finitePlaceOrderTop v x

The order of a natural power is the corresponding natural multiple of the order. The WithTop formulation also covers a zero base.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_algebraMap_nonnegative {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (a : R) : 0 ≤ finitePlaceOrderTop v ((algebraMap R L) a)

A regular element of the Dedekind domain has nonnegative order at every height-one place.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_exists_lift_of_nonnegative {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] (x : L) (hx : 0 ≤ finitePlaceOrderTop (IsDiscreteValuationRing.maximalIdeal R) x) : ∃ (r : R), x = (algebraMap R L) r

An element of nonnegative local order lifts to the discrete valuation ring.

theorem BGS.CorvajaZannier.finitePlaceOrder_unit_mul_uniformizer_zpow {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (u : Rˣ) (n : ℤ) : finitePlaceOrder v ((algebraMap R L) ↑u * (algebraMap R L) π ^ n) = n

At the place generated by a uniformizer, a unit times its n-th integer power has order exactly n.

theorem BGS.CorvajaZannier.finitePlaceOrder_uniformizer_zpow {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (n : ℤ) : finitePlaceOrder v ((algebraMap R L) π ^ n) = n

theorem BGS.CorvajaZannier.finitePlaceOrderTop_uniformizer_zpow {R : Type u_1} {L : Type u_2} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] [IsDiscreteValuationRing R] (v : IsDedekindDomain.HeightOneSpectrum R) (π : R) (hπ : Irreducible π) (hπIdeal : v.asIdeal = Ideal.span {π}) (n : ℤ) : finitePlaceOrderTop v ((algebraMap R L) π ^ n) = ↑n

theorem BGS.CorvajaZannier.finitePlaceOrderTop_derivation_ge_sub_one_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] (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) (x : L) : finitePlaceOrderTop v x + ↑(-1) ≤ finitePlaceOrderTop v (D x)

Any derivation preserving a DVR lowers order by at most one. No normalization of the derivative of the chosen uniformizer is required. The WithTop-valued statement includes the cases x = 0 and D x = 0.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_derivation_ge_sub_one {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] (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) (x : L) : finitePlaceOrderTop v x + ↑(-1) ≤ finitePlaceOrderTop v (D x)

The normalized-uniformizer version retained for callers that naturally construct a local derivative.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_derivation_iterate_ge_sub_nat_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] (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) (r : ℕ) (x : L) : finitePlaceOrderTop v x + ↑(-↑r) ≤ finitePlaceOrderTop v ((⇑D)^[r] x)

Iterating any DVR-preserving derivation lowers finite-place order by at most the number of iterations.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_derivation_iterate_ge_sub_nat {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] (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) (r : ℕ) (x : L) : finitePlaceOrderTop v x + ↑(-↑r) ≤ finitePlaceOrderTop v ((⇑D)^[r] x)

The iterated normalized-uniformizer version retained for compatibility with the local Wronskian API.