Ramification and relative discriminants of number fields #
For an extension of number fields, the primes dividing the relative discriminant are exactly the primes below an upper prime whose ramification index is greater than one. This is the classical ramification criterion in the number-field setting, where finite residue fields make ramification equivalent to a nontrivial ramification index.
Main results #
TauCeti.NumberField.dvd_relDiscr_iff_exists_one_lt_ramificationIdx: a prime divides the relative discriminant exactly when a prime above it has ramification index greater than one.
theorem
TauCeti.NumberField.dvd_relDiscr_iff_exists_one_lt_ramificationIdx
{K : Type u_1}
{L : Type u_2}
[Field K]
[NumberField K]
[Field L]
[NumberField L]
[Algebra K L]
{p : Ideal (NumberField.RingOfIntegers K)}
[p.IsPrime]
:
p ∣ relDiscr (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↔ ∃ (P : ↑(p.primesOver (NumberField.RingOfIntegers L))), 1 < (↑P).ramificationIdx (NumberField.RingOfIntegers K)
A prime divides a number-field relative discriminant exactly when an upper prime has ramification index greater than one.