The different ideal

This file supplies general lemmas about trace-dual fractional ideals. The coercion result connects the fractional-ideal and submodule trace duals, allowing submodule results such as localization to be transferred to fractional ideals. The elementwise descriptions of the trace dual of S and of the different ideal, each as the inverse of the other, are what read the different off valuations and transport it along automorphisms. The identity-extension trace-dual theorem gives the unit different, which is used to compute the relative discriminant of the identity extension. The trace criterion TauCeti.dvd_differentIdeal_iff_forall_intTrace_mem decides when an ideal I with I * Q = p · B divides the different ideal of an extension of Dedekind domains. The multiplicity lemmas express divisibility by powers of a prime and Dedekind's universal e - 1 bound as bounds on the different exponent.

theorem TauCeti.pow_dvd_differentIdeal_iff_le_multiplicity (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B} [P.IsPrime] (hP : P ≠ ⊥) {n : ℕ} : P ^ n ∣ differentIdeal A B ↔ n ≤ multiplicity P (differentIdeal A B)

The characteristic property of the different exponent at a nonzero prime P of B: P ^ n divides the different ideal exactly when n is at most the multiplicity of P in it.

theorem TauCeti.ramificationIdx_sub_one_le_multiplicity_differentIdeal (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.IsPrime] [P.LiesOver p] : P.ramificationIdx A - 1 ≤ multiplicity P (differentIdeal A B)

Dedekind's different theorem, first part, as a bound on the exponent: the multiplicity of a prime P over a nonzero prime p in the different ideal is at least e(P ∣ p) - 1.

@[simp]

theorem TauCeti.FractionalIdeal.coe_dual_one_of_isDomain {R : Type uR} {S : Type uS} {K : Type uK} {L : Type uL} [CommRing R] [CommRing S] [Field K] [Field L] [Algebra R S] [Algebra R K] [Algebra K L] [Algebra R L] [Algebra S L] [IsScalarTower R K L] [IsScalarTower R S L] [IsDomain R] [IsFractionRing R K] [IsFractionRing S L] [IsIntegrallyClosed R] [IsIntegralClosure S R L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsDomain S] : ↑(FractionalIdeal.dual R K 1) = Submodule.traceDual R K 1

Over a domain, the fractional-ideal trace dual of one coerces to the submodule trace dual.

theorem TauCeti.mem_traceDual_one_iff_forall_mem_differentIdeal {R : Type uR} {S : Type uS} {K : Type uK} {L : Type uL} [CommRing R] [CommRing S] [Field K] [Field L] [Algebra R S] [Algebra R K] [Algebra K L] [Algebra R L] [Algebra S L] [IsScalarTower R K L] [IsScalarTower R S L] [IsDomain R] [IsFractionRing R K] [IsFractionRing S L] [IsIntegrallyClosed R] [IsIntegralClosure S R L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsDedekindDomain S] [Module.IsTorsionFree R S] {x : L} : x ∈ Submodule.traceDual R K 1 ↔ ∀ y ∈ differentIdeal R S, x * (algebraMap S L) y ∈ 1

The trace dual of S is the inverse of the different ideal, elementwise: an element of L has integral traces against S exactly when it multiplies the different ideal of S / R into S.

theorem TauCeti.mem_differentIdeal_iff_forall_mem_traceDual {R : Type uR} {S : Type uS} {K : Type uK} {L : Type uL} [CommRing R] [CommRing S] [Field K] [Field L] [Algebra R S] [Algebra R K] [Algebra K L] [Algebra R L] [Algebra S L] [IsScalarTower R K L] [IsScalarTower R S L] [IsDomain R] [IsFractionRing R K] [IsFractionRing S L] [IsIntegrallyClosed R] [IsIntegralClosure S R L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsDedekindDomain S] [Module.IsTorsionFree R S] {y : S} : y ∈ differentIdeal R S ↔ ∀ x ∈ Submodule.traceDual R K 1, x * (algebraMap S L) y ∈ 1

The different ideal is the inverse of the trace dual of S, elementwise: an element of S lies in the different ideal of S / R exactly when it multiplies the trace dual of S into S.

@[simp]

theorem TauCeti.apply_mem_traceDual_one_iff {R : Type uR} {S : Type uS} {K : Type uK} {L : Type uL} [CommRing R] [CommRing S] [Field K] [Field L] [Algebra R S] [Algebra R K] [Algebra K L] [Algebra R L] [Algebra S L] [IsScalarTower R K L] [IsScalarTower R S L] [IsFractionRing R K] [IsIntegralClosure S R L] [FiniteDimensional K L] {σ : Gal(L/K)} {x : L} : σ x ∈ Submodule.traceDual R K 1 ↔ x ∈ Submodule.traceDual R K 1

The trace dual of S is stable under the automorphisms of L / K: an automorphism maps S onto itself and preserves the trace of L / K.

@[simp]

theorem TauCeti.galRestrict_apply_mem_differentIdeal_iff {R : Type uR} {S : Type uS} {K : Type uK} {L : Type uL} [CommRing R] [CommRing S] [Field K] [Field L] [Algebra R S] [Algebra R K] [Algebra K L] [Algebra R L] [Algebra S L] [IsScalarTower R K L] [IsScalarTower R S L] [IsDomain R] [IsFractionRing R K] [IsFractionRing S L] [IsIntegrallyClosed R] [IsIntegralClosure S R L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsDedekindDomain S] [Module.IsTorsionFree R S] {σ : Gal(L/K)} {y : S} : ((galRestrict R K L S) σ) y ∈ differentIdeal R S ↔ y ∈ differentIdeal R S

The different ideal is stable under the automorphisms of L / K, acting on S through their restrictions galRestrict.

theorem TauCeti.dvd_differentIdeal_iff_forall_intTrace_mem (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} (hp : p ≠ ⊥) (I Q : Ideal B) (hIQ : I * Q = Ideal.map (algebraMap A B) p) : I ∣ differentIdeal A B ↔ ∀ x ∈ Q, (Algebra.intTrace A B) x ∈ p

The trace criterion for divisibility of the different ideal. If I * Q = p · B for a nonzero ideal p of A, then I divides differentIdeal A B exactly when the integral trace carries the complement Q into p.

This upgrades Mathlib's one-way not_dvd_differentIdeal_of_intTrace_not_mem to an equivalence. The converse direction adapts the argument that Mathlib runs inline in pow_sub_one_dvd_differentIdeal_aux and dvd_differentIdeal_of_not_isSeparable (Mathlib/RingTheory/DedekindDomain/Different.lean, Andrew Yang).

@[simp]

theorem TauCeti.traceDual_one_fractionRing_self {A : Type u_1} [CommRing A] [IsDomain A] : Submodule.traceDual A (FractionRing A) 1 = 1

The trace dual of the unit submodule is the unit submodule for the identity extension of a domain to its fraction field.

@[simp]

theorem TauCeti.differentIdeal_self {D : Type u_2} [CommRing D] [IsDedekindDomain D] : differentIdeal D D = ⊤

The different ideal of the identity extension of a Dedekind domain is the unit ideal.