Relative discriminants of separable extensions

This file develops the first arithmetic properties of the relative discriminant ideal. For a separable extension of fraction fields, the relative discriminant is nonzero, and in a tower of Dedekind domains it satisfies the usual transitivity formula.

Main results

• TauCeti.relDiscr_ne_bot: the relative discriminant of a separable extension is nonzero.
• TauCeti.relDiscr_tower: the relative discriminant formula for a tower of Dedekind domains.

The tower formula is the ideal version of Neukirch, Algebraic Number Theory, Chapter III, §2, Proposition 10.

theorem TauCeti.relDiscr_ne_bot {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] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] : relDiscr A B ≠ ⊥

The relative discriminant is nonzero when the extension of fraction fields is separable.

theorem TauCeti.relDiscr_tower {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] {C : Type u_3} [CommRing C] [IsDedekindDomain C] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.Finite B C] [Module.Finite A C] [Module.IsTorsionFree B C] [Module.IsTorsionFree A C] [Algebra.IsSeparable (FractionRing A) (FractionRing C)] : relDiscr A C = relDiscr A B ^ Module.finrank B C * (Ideal.relNorm A) (relDiscr B C)

The relative discriminant satisfies the transitivity formula in a tower of Dedekind domains when the top extension of fraction fields is separable.