Scaling derivations at ramified Dedekind places

Let C → S → T → U be a tower, let D preserve S, and let E be an ambient derivation on U extending D. The transitivity exact sequence for Kähler differentials shows that every element annihilating Ω[T⁄S] clears the obstruction to E preserving T.

For a power basis, the minimal-polynomial derivative supplies such a factor and generates the trace different. For a general ramified extension, the comparison between the trace different and the Kähler annihilator is retained as an explicit hypothesis; mathlib does not currently supply it in the needed generality.

noncomputable def BGS.CorvajaZannier.kaehlerDifferentialAnnihilator (S : Type u_5) (T : Type u_6) [CommRing S] [CommRing T] [Algebra S T] : Ideal T

The ideal of scalars annihilating the relative Kähler differentials.

Equations

• BGS.CorvajaZannier.kaehlerDifferentialAnnihilator S T = Module.annihilator T Ω[T⁄S]

theorem BGS.CorvajaZannier.mem_kaehlerDifferentialAnnihilator_iff {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra S T] (c : T) : c ∈ kaehlerDifferentialAnnihilator S T ↔ ∀ (ω : Ω[T⁄S]), c • ω = 0

theorem BGS.CorvajaZannier.liftKaehlerDifferential_algebraMap_compDer {C : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing C] [CommRing S] [CommRing T] [Algebra C S] [Algebra C T] [Algebra S T] [IsScalarTower C S T] (D : Derivation C S S) : ((Algebra.linearMap S T).compDer D).liftKaehlerDifferential = Algebra.linearMap S T ∘ₗ D.liftKaehlerDifferential

theorem BGS.CorvajaZannier.kaehler_baseChange_evaluation_naturality {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) (z : TensorProduct S T Ω[S⁄C]) : (algebraMap T U) ((LinearMap.liftBaseChange T ((Algebra.linearMap S T).compDer D).liftKaehlerDifferential) z) = E.liftKaehlerDifferential ((KaehlerDifferential.map C C T U) ((KaehlerDifferential.mapBaseChange C S T) z))

Evaluation of a base-changed differential agrees with evaluation by an ambient derivation extending the base derivation.

theorem BGS.CorvajaZannier.scaled_ambientDerivation_preserves_of_mem_kaehlerDifferentialAnnihilator {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) (c : T) (hc : c ∈ kaehlerDifferentialAnnihilator S T) (t : T) : ∃ (t' : T), (algebraMap T U) c * E ((algebraMap T U) t) = (algebraMap T U) t'

A scalar annihilating Ω[T⁄S] makes the scaled ambient derivation preserve T. This is the ramified analogue of formal-étale derivation preservation.

theorem BGS.CorvajaZannier.exists_generator_scaled_ambientDerivation_preserves {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] [IsPrincipalIdealRing T] (I : Ideal T) (hI : I ≠ ⊥) (hIann : I ≤ kaehlerDifferentialAnnihilator S T) (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) : ∃ (c : T), c ≠ 0 ∧ Ideal.span {c} = I ∧ c ∈ kaehlerDifferentialAnnihilator S T ∧ ∀ (t : T), ∃ (t' : T), (algebraMap T U) c * E ((algebraMap T U) t) = (algebraMap T U) t'

A nonzero principal ideal contained in the Kähler annihilator has a nonzero generator which clears the ambient derivation.

theorem BGS.CorvajaZannier.powerBasis_minpolyDerivative_mem_kaehlerDifferentialAnnihilator {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra S T] (pb : PowerBasis S T) : (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly S pb.gen)) ∈ kaehlerDifferentialAnnihilator S T

For a power basis, the derivative of the generator's minimal polynomial annihilates the relative Kähler differentials.

theorem BGS.CorvajaZannier.powerBasis_minpolyDerivative_scaled_ambientDerivation_preserves {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] (pb : PowerBasis S T) (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) (t : T) : ∃ (t' : T), (algebraMap T U) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly S pb.gen))) * E ((algebraMap T U) t) = (algebraMap T U) t'

The minimal-polynomial derivative of a power-basis generator clears the ambient derivation.

theorem BGS.CorvajaZannier.exists_differentGenerator_scaled_ambientDerivation_preserves {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] [IsDomain S] [IsDedekindDomain T] [Module.IsTorsionFree S T] [IsPrincipalIdealRing T] (hDifferent : differentIdeal S T ≠ ⊥) (hDifferentKaehler : differentIdeal S T ≤ kaehlerDifferentialAnnihilator S T) (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) : ∃ (c : T), c ≠ 0 ∧ Ideal.span {c} = differentIdeal S T ∧ c ∈ kaehlerDifferentialAnnihilator S T ∧ ∀ (t : T), ∃ (t' : T), (algebraMap T U) c * E ((algebraMap T U) t) = (algebraMap T U) t'

If the trace different is contained in the Kähler annihilator, a generator of the different is an exact ramified derivation-clearing factor.

theorem BGS.CorvajaZannier.finitePlaceOrder_differentGenerator_eq_multiplicity {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra S T] [IsDomain S] [IsDedekindDomain T] [Module.IsTorsionFree S T] {F : Type u_5} [Field F] [Algebra T F] [IsFractionRing T F] (c : T) (hc : c ≠ 0) (hspan : Ideal.span {c} = differentIdeal S T) (v : IsDedekindDomain.HeightOneSpectrum T) : finitePlaceOrder v ((algebraMap T F) c) = ↑(multiplicity v.asIdeal (differentIdeal S T))

A generator of the different has finite-place order exactly equal to the different multiplicity.

theorem BGS.CorvajaZannier.exists_differentGenerator_scaling_certificate {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] [IsDomain S] [IsDedekindDomain T] [Module.IsTorsionFree S T] {F : Type u_5} [Field F] [Algebra T F] [IsFractionRing T F] [IsPrincipalIdealRing T] (hDifferent : differentIdeal S T ≠ ⊥) (hDifferentKaehler : differentIdeal S T ≤ kaehlerDifferentialAnnihilator S T) (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) : ∃ (c : T), c ≠ 0 ∧ Ideal.span {c} = differentIdeal S T ∧ c ∈ kaehlerDifferentialAnnihilator S T ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum T), finitePlaceOrder v ((algebraMap T F) c) = ↑(multiplicity v.asIdeal (differentIdeal S T))) ∧ ∀ (t : T), ∃ (t' : T), (algebraMap T U) c * E ((algebraMap T U) t) = (algebraMap T U) t'

A single certificate combining ramified derivation preservation with the exact local order of the clearing factor.

theorem BGS.CorvajaZannier.finitePlaceOrder_mul_eq_add {A : Type u_6} {F : Type u_7} [CommRing A] [IsDedekindDomain A] [Field F] [Algebra A F] [IsFractionRing A F] (v : IsDedekindDomain.HeightOneSpectrum A) (x y : F) (hx : x ≠ 0) (hy : y ≠ 0) : finitePlaceOrder v (x * y) = finitePlaceOrder v x + finitePlaceOrder v y

Multiplication of two nonzero field elements adds their finite-place orders. This non-WithTop form is convenient for exact local certificates.

theorem BGS.CorvajaZannier.finitePlaceOrder_inv_eq_neg' {A : Type u_6} {F : Type u_7} [CommRing A] [IsDedekindDomain A] [Field F] [Algebra A F] [IsFractionRing A F] (v : IsDedekindDomain.HeightOneSpectrum A) (x : F) (hx : x ≠ 0) : finitePlaceOrder v x⁻¹ = -finitePlaceOrder v x

Inversion negates finite-place order.

theorem BGS.CorvajaZannier.finitePlaceOrder_neg_eq {A : Type u_6} {F : Type u_7} [CommRing A] [IsDedekindDomain A] [Field F] [Algebra A F] [IsFractionRing A F] (v : IsDedekindDomain.HeightOneSpectrum A) (x : F) (hx : x ≠ 0) : finitePlaceOrder v (-x) = finitePlaceOrder v x

Negating a nonzero field element does not change its finite-place order.

theorem BGS.CorvajaZannier.finitePlaceOrder_algebraMap_uniformizer_eq_ramificationIdx {R : Type u_5} {A : Type u_6} {F : Type u_7} [CommRing R] [IsDomain R] [CommRing A] [IsDedekindDomain A] [Algebra R A] [Module.IsTorsionFree R A] [Field F] [Algebra A F] [IsFractionRing A F] (p : IsDedekindDomain.HeightOneSpectrum R) (v : IsDedekindDomain.HeightOneSpectrum A) [v.asIdeal.LiesOver p.asIdeal] (s : R) (hs : s ≠ 0) (hspan : p.asIdeal = Ideal.span {s}) : finitePlaceOrder v ((algebraMap A F) ((algebraMap R A) s)) = ↑(v.asIdeal.ramificationIdx R)

If s generates a base height-one prime, then its order at a prime above it is exactly the ramification index.

theorem BGS.CorvajaZannier.differentIdeal_eq_span_powerBasis_minpolyDerivative {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra S T] {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra S K] [Algebra T L] [Algebra K L] [Algebra S L] [IsScalarTower S K L] [IsScalarTower S T L] [IsDomain S] [IsFractionRing S K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure T S L] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] (pb : PowerBasis S T) (hprimitive : K[(algebraMap T L) pb.gen] = ⊤) : differentIdeal S T = Ideal.span {(Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly S pb.gen))}

For an integral power basis generated by a primitive field element, the trace different is exactly the principal ideal generated by the minimal-polynomial derivative.

theorem BGS.CorvajaZannier.powerBasis_minpolyDerivative_finitePlaceOrder_eq_differentMultiplicity {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra S T] {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra S K] [Algebra T L] [Algebra K L] [Algebra S L] [IsScalarTower S K L] [IsScalarTower S T L] [IsDomain S] [IsFractionRing S K] [IsFractionRing T L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure T S L] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] (pb : PowerBasis S T) (hprimitive : K[(algebraMap T L) pb.gen] = ⊤) (v : IsDedekindDomain.HeightOneSpectrum T) : finitePlaceOrder v ((algebraMap T L) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly S pb.gen)))) = ↑(multiplicity v.asIdeal (differentIdeal S T))

The power-basis derivative has exact order equal to the different multiplicity at every finite place.

theorem BGS.CorvajaZannier.exists_powerBasis_differentGenerator_scaled_ambientDerivation_preserves {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra S K] [Algebra T L] [Algebra K L] [Algebra S L] [IsScalarTower S K L] [IsScalarTower S T L] [IsDomain S] [IsFractionRing S K] [IsFractionRing T L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure T S L] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] (pb : PowerBasis S T) (hprimitive : K[(algebraMap T L) pb.gen] = ⊤) (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) : ∃ (c : T), c ≠ 0 ∧ Ideal.span {c} = differentIdeal S T ∧ c ∈ kaehlerDifferentialAnnihilator S T ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum T), finitePlaceOrder v ((algebraMap T L) c) = ↑(multiplicity v.asIdeal (differentIdeal S T))) ∧ ∀ (t : T), ∃ (t' : T), (algebraMap T U) c * E ((algebraMap T U) t) = (algebraMap T U) t'

In the power-basis case, the minimal-polynomial derivative simultaneously generates the different, annihilates relative differentials, has exact local different order, and clears the ambient derivation.

theorem BGS.CorvajaZannier.exists_powerBasis_finitePlace_different_scaling_certificate {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommRing C] [CommRing S] [CommRing T] [CommRing U] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C U] [Algebra S U] [Algebra T U] [IsScalarTower C S T] [IsScalarTower C S U] [IsScalarTower C T U] [IsScalarTower S T U] {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra S K] [Algebra T L] [Algebra K L] [Algebra S L] [IsScalarTower S K L] [IsScalarTower S T L] [IsDomain S] [IsFractionRing S K] [IsFractionRing T L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure T S L] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] (pb : PowerBasis S T) (hprimitive : K[(algebraMap T L) pb.gen] = ⊤) (v : IsDedekindDomain.HeightOneSpectrum T) (D : Derivation C S S) (E : Derivation C U U) (hE : ∀ (s : S), E ((algebraMap S U) s) = (algebraMap S U) (D s)) : ∃ (c : T), c ≠ 0 ∧ finitePlaceOrder v ((algebraMap T L) c) = ↑(multiplicity v.asIdeal (differentIdeal S T)) ∧ ∀ (t : T), ∃ (t' : T), (algebraMap T U) c * E ((algebraMap T U) t) = (algebraMap T U) t'

Placewise finite certificate extracted from an integral power basis: one nonzero scalar has exactly the local different order and makes the ambient derivation preserve the local Dedekind ring.

theorem BGS.CorvajaZannier.exists_powerBasis_infinity_different_scaling_certificate {C : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing C] [CommRing S] [CommRing T] [Algebra C S] [Algebra C T] [Algebra S T] [IsScalarTower C S T] {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra S K] [Algebra T L] [Algebra K L] [Algebra S L] [IsScalarTower S K L] [IsScalarTower S T L] [IsDomain S] [IsFractionRing S K] [IsFractionRing T L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure T S L] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] [Algebra C L] [IsScalarTower C S L] [IsScalarTower C T L] (pb : PowerBasis S T) (hprimitive : K[(algebraMap T L) pb.gen] = ⊤) (p : IsDedekindDomain.HeightOneSpectrum S) (v : IsDedekindDomain.HeightOneSpectrum T) [v.asIdeal.LiesOver p.asIdeal] (s : S) (hs : s ≠ 0) (hspan : p.asIdeal = Ideal.span {s}) (Ds : Derivation C S S) (Es DX : Derivation C L L) (hEs : ∀ (r : S), Es ((algebraMap S L) r) = (algebraMap S L) (Ds r)) (hDX : DX = -(algebraMap S L) s ^ 2 • Es) : ∃ (δ : T), δ ≠ 0 ∧ Ideal.span {δ} = differentIdeal S T ∧ have c := -(algebraMap T L) δ / (algebraMap S L) s ^ 2; finitePlaceOrder v c = ↑(multiplicity v.asIdeal (differentIdeal S T)) - 2 * ↑(v.asIdeal.ramificationIdx S) ∧ ∀ (t : T), ∃ (t' : T), c * DX ((algebraMap T L) t) = (algebraMap T L) t'

Exact change from the local parameter derivation D_s to the global X-derivation when s = X⁻¹. If D_X = -s² D_s, dividing a different generator by -s² leaves the scaled derivation unchanged and subtracts 2e from its local order. Thus the resulting scalar realizes exactly the infinity coefficient different exponent - 2 * ramification index of the canonical different divisor.