Relative discriminant ideals

For a finite torsion-free extension A → B of Dedekind domains, the relative discriminant is the ideal of A obtained by taking the relative norm of Mathlib's different ideal of B. This file introduces that carrier, together with the two defining identities that are valid without a separability assumption. The later arithmetic theory uses relDiscr rather than expanding this relative norm of the different at each use site.

noncomputable def TauCeti.relDiscr (A : Type u_3) (B : Type u_4) [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : Ideal A

The relative discriminant ideal of the finite torsion-free extension A → B.

Equations

• TauCeti.relDiscr A B = (Ideal.relNorm A) (differentIdeal A B)

theorem TauCeti.relDiscr_def {A : Type u_1} {B : Type u_2} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : relDiscr A B = (Ideal.relNorm A) (differentIdeal A B)

The relative discriminant is the relative norm of the different ideal.

@[simp]

theorem TauCeti.relDiscr_eq_bot_iff {A : Type u_1} {B : Type u_2} [CommRing A] [IsDedekindDomain A] [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] : relDiscr A B = ⊥ ↔ differentIdeal A B = ⊥

The relative discriminant is zero exactly when the different is zero.

@[simp]

theorem TauCeti.relDiscr_self {A : Type u_1} [CommRing A] [IsDedekindDomain A] : relDiscr A A = ⊤

The relative discriminant of the identity extension is the unit ideal.