Canonical different scalings at Dedekind places

This file removes the explicit comparison hypothesis between the trace different and the Kähler differentials from the finite- and infinite-place derivation-scaling certificates.

The different need not be principal globally. At a prescribed height-one place v, Dedekind approximation supplies a global element δ in the different whose principal ideal has exactly the same v-multiplicity. Thus δ is a generator after localization at v. The theorem that the different annihilates relative Kähler differentials then makes δ a derivation-clearing factor. No local power basis or finiteness assertion for a map between two independently localized rings is used.

theorem BGS.CorvajaZannier.exists_element_locally_generating_ideal {R : Type u_1} [CommRing R] [IsDedekindDomain R] (I : Ideal R) (hI : I ≠ ⊥) (v : IsDedekindDomain.HeightOneSpectrum R) : ∃ (a : R), a ≠ 0 ∧ a ∈ I ∧ multiplicity v.asIdeal (Ideal.span {a}) = multiplicity v.asIdeal I

Every nonzero ideal in a Dedekind domain admits, at a prescribed height-one place, a global element which generates that ideal after localization.

theorem BGS.CorvajaZannier.exists_finitePlace_different_localGenerator_scaling_certificate {C : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} {F : Type u_5} [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] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] [Module.Finite S T] [Module.Free S T] [Algebra.IsSeparable (FractionRing S) (FractionRing T)] [Field F] [Algebra T F] [IsFractionRing T F] (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)) : ∃ (δ : T), δ ≠ 0 ∧ δ ∈ differentIdeal S T ∧ multiplicity v.asIdeal (Ideal.span {δ}) = multiplicity v.asIdeal (differentIdeal S T) ∧ finitePlaceOrder v ((algebraMap T F) δ) = ↑(multiplicity v.asIdeal (differentIdeal S T)) ∧ δ ∈ kaehlerDifferentialAnnihilator S T ∧ ∀ (t : T), ∃ (t' : T), (algebraMap T U) δ * E ((algebraMap T U) t) = (algebraMap T U) t'

At every height-one place, a global element locally generates the different and clears the obstruction to preserving the integral closure.

theorem BGS.CorvajaZannier.exists_infinity_different_localGenerator_scaling_certificate {C : Type u_1} {S : Type u_2} {T : Type u_3} {L : Type u_4} [CommRing C] [CommRing S] [CommRing T] [Field L] [Algebra C S] [Algebra C T] [Algebra S T] [Algebra C L] [Algebra S L] [Algebra T L] [IsScalarTower C S T] [IsScalarTower C S L] [IsScalarTower C T L] [IsScalarTower S T L] [IsDomain S] [IsIntegrallyClosed S] [IsDedekindDomain T] [Module.IsTorsionFree S T] [Module.Finite S T] [Module.Free S T] [Algebra.IsSeparable (FractionRing S) (FractionRing T)] [IsFractionRing T L] (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 ∧ δ ∈ differentIdeal S T ∧ multiplicity v.asIdeal (Ideal.span {δ}) = multiplicity v.asIdeal (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'

At a place over the pole of the reciprocal parameter s, the scalar -δ/s² has order equal to the different multiplicity minus twice the ramification index and makes the reparameterized derivation integral.