Ramification and the relative discriminant

For a separable extension of fraction fields of Dedekind domains, a prime divides the relative discriminant exactly when some prime above it is ramified. Here ramification is expressed intrinsically by failure of Algebra.IsUnramifiedAt; no residue-field separability is required.

Main results

• TauCeti.dvd_relDiscr_iff_exists_not_isUnramifiedAt: a prime divides the relative discriminant exactly when the extension ramifies at a prime above it.

This is the relative-discriminant ramification criterion of Neukirch, Algebraic Number Theory, Chapter III, §2, Proposition 12.

theorem TauCeti.dvd_relDiscr_iff_exists_not_isUnramifiedAt {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)] {p : Ideal A} [p.IsPrime] : p ∣ relDiscr A B ↔ ∃ (P : ↑(p.primesOver B)), ¬Algebra.IsUnramifiedAt A ↑P

A prime divides the relative discriminant exactly when a prime above it is ramified. Ramification means failure of Algebra.IsUnramifiedAt, so this statement does not need the residue extensions to be separable.