The different divisor and the primitive-element derivative

For a finite separable extension represented by an integral primitive element, the different ideal divides the principal ideal generated by the derivative of the integral minimal polynomial. This file packages that fact at four levels:

• effective finitely supported divisors of nonzero Dedekind ideals;
• coefficientwise and arbitrary nonnegative weighted bounds for the different;
• the corresponding local finite-place order inequality; and
• the field norm identity relating the derivative to the power-basis discriminant.

Thus all ramified finite-place contributions represented by the different are controlled by one principal divisor. No canonical-divisor or genus estimate is assumed here.

noncomputable def BGS.CorvajaZannier.idealMultiplicityDivisor {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) (hI : I ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum R →₀ ℕ

The effective divisor associated to a nonzero integral ideal of a Dedekind domain.

Equations

• BGS.CorvajaZannier.idealMultiplicityDivisor I hI = { support := ⋯.toFinset, toFun := fun (v : IsDedekindDomain.HeightOneSpectrum R) => multiplicity v.asIdeal I, mem_support_toFun := ⋯ }

@[simp]

theorem BGS.CorvajaZannier.idealMultiplicityDivisor_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum R) : (idealMultiplicityDivisor I hI) v = multiplicity v.asIdeal I

theorem BGS.CorvajaZannier.idealMultiplicityDivisor_mono {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (h : J ≤ I) : idealMultiplicityDivisor I hI ≤ idealMultiplicityDivisor J hJ

theorem BGS.CorvajaZannier.idealMultiplicityDivisor_weightedSum_mono {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) (h : J ≤ I) (weight : IsDedekindDomain.HeightOneSpectrum R → ℕ) : ((idealMultiplicityDivisor I hI).sum fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℕ) => e * weight v) ≤ (idealMultiplicityDivisor J hJ).sum fun (v : IsDedekindDomain.HeightOneSpectrum R) (e : ℕ) => e * weight v

noncomputable def BGS.CorvajaZannier.differentMultiplicityDivisor (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [IsDomain A] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] (hDifferent : differentIdeal A B ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum B →₀ ℕ

The effective different divisor of a finite separable Dedekind extension.

Equations

• BGS.CorvajaZannier.differentMultiplicityDivisor A B hDifferent = BGS.CorvajaZannier.idealMultiplicityDivisor (differentIdeal A B) hDifferent

@[simp]

theorem BGS.CorvajaZannier.differentMultiplicityDivisor_apply (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [IsDomain A] [IsDedekindDomain B] [Algebra A B] [Module.IsTorsionFree A B] (hDifferent : differentIdeal A B ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum B) : (differentMultiplicityDivisor A B hDifferent) v = multiplicity v.asIdeal (differentIdeal A B)

theorem BGS.CorvajaZannier.minpolyDerivative_ne_zero {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] (x : B) : (Polynomial.aeval x) (Polynomial.derivative (minpoly A x)) ≠ 0

In a separable function-field extension, the integral minimal-polynomial derivative of every integral element is nonzero.

theorem BGS.CorvajaZannier.minpolyDerivative_span_ne_bot {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] (x : B) : Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))} ≠ ⊥

theorem BGS.CorvajaZannier.differentIdeal_ne_bot_of_primitiveElement {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) : differentIdeal A B ≠ ⊥

A separable primitive element supplies a nonzero element of the different, so the different ideal itself is nonzero.

theorem BGS.CorvajaZannier.differentIdeal_dvd_minpolyDerivativeSpan {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) : differentIdeal A B ∣ Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}

The different divides the principal ideal generated by the derivative of a primitive element's integral minimal polynomial.

theorem BGS.CorvajaZannier.differentIdeal_multiplicity_le_minpolyDerivativeSpan {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) (v : IsDedekindDomain.HeightOneSpectrum B) : multiplicity v.asIdeal (differentIdeal A B) ≤ multiplicity v.asIdeal (Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))})

At every finite prime, the different exponent is bounded by the order of the primitive element's minimal-polynomial derivative.

theorem BGS.CorvajaZannier.differentPrime_dvd_minpolyDerivativeSpan {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) (v : IsDedekindDomain.HeightOneSpectrum B) (hv : v.asIdeal ∣ differentIdeal A B) : v.asIdeal ∣ Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}

theorem BGS.CorvajaZannier.differentMultiplicityDivisor_le_minpolyDerivativeDivisor {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) : differentMultiplicityDivisor A B ⋯ ≤ idealMultiplicityDivisor (Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}) ⋯

theorem BGS.CorvajaZannier.differentMultiplicityWeightedSum_le_minpolyDerivative {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) (weight : IsDedekindDomain.HeightOneSpectrum B → ℕ) : ((differentMultiplicityDivisor A B ⋯).sum fun (v : IsDedekindDomain.HeightOneSpectrum B) (e : ℕ) => e * weight v) ≤ (idealMultiplicityDivisor (Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}) ⋯).sum fun (v : IsDedekindDomain.HeightOneSpectrum B) (e : ℕ) => e * weight v

theorem BGS.CorvajaZannier.finite_differentPrimes_of_primitiveElement {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) : {v : IsDedekindDomain.HeightOneSpectrum B | v.asIdeal ∣ differentIdeal A B}.Finite

theorem BGS.CorvajaZannier.finitePlaceOrder_algebraMap_eq_multiplicity {R : Type u_1} {F : Type u_2} [CommRing R] [IsDedekindDomain R] [Field F] [Algebra R F] [IsFractionRing R F] (v : IsDedekindDomain.HeightOneSpectrum R) (a : R) (ha : a ≠ 0) : finitePlaceOrder v ((algebraMap R F) a) = ↑(multiplicity v.asIdeal (Ideal.span {a}))

theorem BGS.CorvajaZannier.differentIdeal_multiplicity_le_finitePlaceOrder_minpolyDerivative {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [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] [IsFractionRing A K] [IsFractionRing B L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) (v : IsDedekindDomain.HeightOneSpectrum B) : ↑(multiplicity v.asIdeal (differentIdeal A B)) ≤ finitePlaceOrder v ((algebraMap B L) ((Polynomial.aeval x) (Polynomial.derivative (minpoly A x))))

theorem BGS.CorvajaZannier.discr_powerBasisOfPrimitiveElement_eq_norm_minpolyDerivative {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] (x : B) (hx : K[(algebraMap B L) x] = ⊤) : have pb := PowerBasis.ofAdjoinEqTop' ⋯ hx; Algebra.discr K ⇑pb.basis = (-1) ^ (Module.finrank K L * (Module.finrank K L - 1) / 2) * (Algebra.norm K) ((algebraMap B L) ((Polynomial.aeval x) (Polynomial.derivative (minpoly A x))))

The field norm of the integral minimal-polynomial derivative is the power-basis discriminant, up to the standard sign.