Reciprocal normalization at a finite base place

This file supplies the local algebraic bridge used in the Corvaja--Zannier middle game. If a polynomial relation f(v) = 0 has unit value f(c), the reciprocal parameter z = (v-c)⁻¹ satisfies a monic integral equation. The normalization preserves primitive generation, becomes the minimal polynomial under the full-degree hypothesis, and changes the discriminant only by a unit. Consequently its discriminant has exactly the same order at every finite base place as the discriminant of f.

The fixed-degree reflection/resultant identities are proved here because the coefficient-reversal discriminant formula needed for a nonmonic relation was not previously available in Mathlib in this form.

def BGS.CorvajaZannier.reflectSylvesterEquiv (m n : ℕ) : Fin (n + m) ≃ Fin (m + n)

Reverse and exchange the two index blocks of a Sylvester matrix.

Equations

• BGS.CorvajaZannier.reflectSylvesterEquiv m n = (finCongr ⋯).trans Fin.revPerm

theorem BGS.CorvajaZannier.sylvester_reflect {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) : (Polynomial.reflect m f).sylvester (Polynomial.reflect n g) m n = (Matrix.reindex (reflectSylvesterEquiv m n) (reflectSylvesterEquiv m n)) (g.sylvester f n m)

theorem BGS.CorvajaZannier.resultant_reflect {R : Type u_1} [CommRing R] (f g : Polynomial R) (m n : ℕ) : (Polynomial.reflect m f).resultant (Polynomial.reflect n g) m n = (-1) ^ (m * n) * f.resultant g m n

Reversing both coefficient lists changes the fixed-degree resultant only by the standard interchange sign.

theorem BGS.CorvajaZannier.reflect_derivative_relation {R : Type u_1} [CommRing R] (f : Polynomial R) (n : ℕ) (hf : f.natDegree ≤ n) : Polynomial.reflect (n - 1) (Polynomial.derivative f) = Polynomial.C ↑n * Polynomial.reflect n f - Polynomial.X * Polynomial.derivative (Polynomial.reflect n f)

theorem BGS.CorvajaZannier.natDegree_reflect_eq {F : Type u_2} [Field F] (f : Polynomial F) (n : ℕ) (hf : f.natDegree ≤ n) (hzero : f.coeff 0 ≠ 0) : (Polynomial.reflect n f).natDegree = n

theorem BGS.CorvajaZannier.resultant_reflect_derivative_balance {F : Type u_2} [Field F] (f : Polynomial F) (n : ℕ) (hf : f.natDegree ≤ n) (hzero : f.coeff 0 ≠ 0) : (Polynomial.reflect n f).leadingCoeff * (Polynomial.reflect n f).resultant (Polynomial.reflect (n - 1) (Polynomial.derivative f)) n (n - 1) = (Polynomial.reflect n f).coeff 0 * (Polynomial.reflect n f).resultant (Polynomial.derivative (Polynomial.reflect n f)) n (n - 1)

theorem BGS.CorvajaZannier.discr_reflect_eq {F : Type u_2} [Field F] (f : Polynomial F) (hzero : f.coeff 0 ≠ 0) : (Polynomial.reflect f.natDegree f).discr = f.discr

Reversing a polynomial of positive degree with nonzero constant term preserves its discriminant.

theorem BGS.CorvajaZannier.discr_taylor_eq {F : Type u_2} [Field F] (f : Polynomial F) (c : F) : ((Polynomial.taylor c) f).discr = f.discr

Translation of the variable preserves the discriminant.

theorem BGS.CorvajaZannier.discr_C_mul {F : Type u_2} [Field F] (f : Polynomial F) (b : F) (hb : b ≠ 0) : (Polynomial.C b * f).discr = b ^ (2 * f.natDegree - 2) * f.discr

Scaling every coefficient by b scales the discriminant by b^(2 * degree - 2).

noncomputable def BGS.CorvajaZannier.reciprocalTranslate {R : Type u_1} [CommRing R] (f : Polynomial R) (c : R) : Polynomial R

The reciprocal translate Z^deg(f) * f(c + Z⁻¹), represented without Laurent polynomials as the reflection of the Taylor translate.

Equations

• BGS.CorvajaZannier.reciprocalTranslate f c = Polynomial.reflect f.natDegree ((Polynomial.taylor c) f)

theorem BGS.CorvajaZannier.reciprocalTranslate_natDegree_eq {R : Type u_1} [CommRing R] (f : Polynomial R) (c : R) (heval : Polynomial.eval c f ≠ 0) : (reciprocalTranslate f c).natDegree = f.natDegree

theorem BGS.CorvajaZannier.reciprocalTranslate_leadingCoeff {R : Type u_1} [CommRing R] (f : Polynomial R) (c : R) (heval : Polynomial.eval c f ≠ 0) : (reciprocalTranslate f c).leadingCoeff = Polynomial.eval c f

theorem BGS.CorvajaZannier.discr_map_of_injective {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [IsDomain S] (φ : R →+* S) (hφ : Function.Injective ⇑φ) (f : Polynomial R) : (Polynomial.map φ f).discr = φ f.discr

Discriminants commute with an injective coefficient map.

theorem BGS.CorvajaZannier.reciprocalTranslate_discr {F : Type u_2} [Field F] (f : Polynomial F) (c : F) (heval : Polynomial.eval c f ≠ 0) : (reciprocalTranslate f c).discr = f.discr

theorem BGS.CorvajaZannier.aeval_reciprocalTranslate_inv_sub_eq_zero {A : Type u_2} {L : Type u_3} [CommRing A] [Field L] [Algebra A L] (f : Polynomial A) (c : A) (v : L) (hvc : v ≠ (algebraMap A L) c) (hv : (Polynomial.aeval v) f = 0) : (Polynomial.aeval (v - (algebraMap A L) c)⁻¹) (reciprocalTranslate f c) = 0

theorem BGS.CorvajaZannier.adjoin_inv_sub_eq_top_of_adjoin_eq_top {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (c : K) (v : L) (hv : K[v] = ⊤) : K[(v - (algebraMap K L) c)⁻¹] = ⊤

Replacing a primitive element v by (v - c)⁻¹ preserves primitive generation. This is the field-theoretic half of the reciprocal local normalization used below.

noncomputable def BGS.CorvajaZannier.unitNormalizedReciprocalTranslate {A : Type u_2} [CommRing A] (f : Polynomial A) (c : A) (u : Aˣ) : Polynomial A

Divide a reciprocal translate by its unit leading coefficient.

Equations

• BGS.CorvajaZannier.unitNormalizedReciprocalTranslate f c u = Polynomial.C ↑u⁻¹ * BGS.CorvajaZannier.reciprocalTranslate f c

theorem BGS.CorvajaZannier.unitNormalizedReciprocalTranslate_map {A : Type u_2} [CommRing A] {S : Type u_4} [CommRing S] (φ : A →+* S) (hφ : Function.Injective ⇑φ) (f : Polynomial A) (c : A) (u : Aˣ) : Polynomial.map φ (unitNormalizedReciprocalTranslate f c u) = unitNormalizedReciprocalTranslate (Polynomial.map φ f) (φ c) ((Units.map ↑φ) u)

theorem BGS.CorvajaZannier.unitNormalizedReciprocalTranslate_monic {A : Type u_2} [CommRing A] [Nontrivial A] (f : Polynomial A) (c : A) (u : Aˣ) (hu : Polynomial.eval c f = ↑u) : (unitNormalizedReciprocalTranslate f c u).Monic

theorem BGS.CorvajaZannier.aeval_unitNormalizedReciprocalTranslate_inv_sub_eq_zero {A : Type u_2} {L : Type u_3} [CommRing A] [Field L] [Algebra A L] (f : Polynomial A) (c : A) (u : Aˣ) (v : L) (hvc : v ≠ (algebraMap A L) c) (hv : (Polynomial.aeval v) f = 0) : (Polynomial.aeval (v - (algebraMap A L) c)⁻¹) (unitNormalizedReciprocalTranslate f c u) = 0

theorem BGS.CorvajaZannier.isIntegral_inv_sub_of_eval_eq_unit {A : Type u_2} {L : Type u_3} [CommRing A] [Nontrivial A] [Field L] [Algebra A L] (f : Polynomial A) (c : A) (u : Aˣ) (v : L) (hu : Polynomial.eval c f = ↑u) (hvc : v ≠ (algebraMap A L) c) (hv : (Polynomial.aeval v) f = 0) : IsIntegral A (v - (algebraMap A L) c)⁻¹

If f(c) is a unit, the reciprocal local parameter (v-c)⁻¹ is integral over the coefficient ring.

theorem BGS.CorvajaZannier.unitNormalizedReciprocalTranslate_discr {F : Type u_2} [Field F] (f : Polynomial F) (c : F) (u : Fˣ) (hu : Polynomial.eval c f = ↑u) : (unitNormalizedReciprocalTranslate f c u).discr = ↑u⁻¹ ^ (2 * f.natDegree - 2) * f.discr

theorem BGS.CorvajaZannier.map_unitNormalizedReciprocalTranslate_discr {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] (hAK : Function.Injective ⇑(algebraMap A K)) (f : Polynomial A) (c : A) (u : Aˣ) (hu : Polynomial.eval c f = ↑u) : (algebraMap A K) (unitNormalizedReciprocalTranslate f c u).discr = (algebraMap A K) ↑u⁻¹ ^ (2 * f.natDegree - 2) * (algebraMap A K) f.discr

After embedding the coefficient ring in a field, normalization changes the discriminant only by the displayed unit power.

theorem BGS.CorvajaZannier.minpoly_inv_sub_eq_map_unitNormalizedReciprocalTranslate {A : Type u_2} {K : Type u_3} {L : Type u_4} [CommRing A] [IsDomain A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsFractionRing A K] [FiniteDimensional K L] (f : Polynomial A) (c : A) (u : Aˣ) (v : L) (hu : Polynomial.eval c f = ↑u) (hvc : v ≠ (algebraMap A L) c) (hv : (Polynomial.aeval v) f = 0) (hprimitive : K[v] = ⊤) (hdegree : f.natDegree = Module.finrank K L) : minpoly K (v - (algebraMap A L) c)⁻¹ = Polynomial.map (algebraMap A K) (unitNormalizedReciprocalTranslate f c u)

If the original equation has the full extension degree, then its monic reciprocal normalization is exactly the minimal polynomial of (v-c)⁻¹ over the fraction field.

theorem BGS.CorvajaZannier.exists_reciprocal_integral_primitive_and_different_bound {A : Type u_2} {K : Type u_3} {L : Type u_4} {B : Type u_5} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra A B] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsIntegrallyClosed A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsDedekindDomain B] [Module.IsTorsionFree A B] (f : Polynomial A) (c : A) (u : Aˣ) (v : L) (hu : Polynomial.eval c f = ↑u) (hvc : v ≠ (algebraMap A L) c) (hv : (Polynomial.aeval v) f = 0) (hprimitive : K[v] = ⊤) (w : IsDedekindDomain.HeightOneSpectrum B) : ∃ (z : B), (algebraMap B L) z = (v - (algebraMap A L) c)⁻¹ ∧ K[(algebraMap B L) z] = ⊤ ∧ multiplicity w.asIdeal (differentIdeal A B) ≤ multiplicity w.asIdeal (Ideal.span {(Polynomial.aeval z) (Polynomial.derivative (minpoly A z))})

A reciprocal translate whose value at the center is a unit gives an integral primitive element, and its minimal-polynomial derivative bounds the different at every finite prime.

@[simp]

theorem BGS.CorvajaZannier.finitePlaceOrderTop_algebraMap_unit {A : Type u_2} {K : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) (u : Aˣ) : finitePlaceOrderTop v ((algebraMap A K) ↑u) = 0

A base-ring unit has order zero at every finite place.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_map_unitNormalizedReciprocalTranslate_discr {A : Type u_2} {K : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A) (f : Polynomial A) (c : A) (u : Aˣ) (hu : Polynomial.eval c f = ↑u) : finitePlaceOrderTop v ((algebraMap A K) (unitNormalizedReciprocalTranslate f c u).discr) = finitePlaceOrderTop v ((algebraMap A K) f.discr)

Unit-normalizing a reciprocal translate preserves the discriminant order at every finite place of the coefficient ring.

theorem BGS.CorvajaZannier.finitePlaceOrderTop_minpoly_inv_sub_discr {A : Type u_2} {K : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_4} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] (v₀ : IsDedekindDomain.HeightOneSpectrum A) (f : Polynomial A) (c : A) (u : Aˣ) (v : L) (hu : Polynomial.eval c f = ↑u) (hvc : v ≠ (algebraMap A L) c) (hv : (Polynomial.aeval v) f = 0) (hprimitive : K[v] = ⊤) (hdegree : f.natDegree = Module.finrank K L) : finitePlaceOrderTop v₀ (minpoly K (v - (algebraMap A L) c)⁻¹).discr = finitePlaceOrderTop v₀ ((algebraMap A K) f.discr)

Under the full-degree primitive-element hypothesis, the discriminant of the reciprocal element's minimal polynomial has exactly the order of the original equation's discriminant at every finite base place.