Relative discriminants of number fields

This file specializes the relative discriminant ideal to rings of integers. It identifies the relative discriminant over ℤ with the principal ideal generated by the signed absolute discriminant, and states transitivity with the field degree as exponent.

Main results

• TauCeti.NumberField.relDiscr_int_ringOfIntegers: the relative discriminant over ℤ is generated by NumberField.discr.
• TauCeti.NumberField.relDiscr_tower: the relative discriminant formula in a tower of number fields.

@[simp]

theorem TauCeti.NumberField.relDiscr_int_ringOfIntegers (K : Type u_1) [Field K] [NumberField K] : relDiscr ℤ (NumberField.RingOfIntegers K) = Ideal.span {NumberField.discr K}

The relative discriminant of the ring of integers of a number field over ℤ is the ideal generated by its signed absolute discriminant.

theorem TauCeti.NumberField.relDiscr_tower (K : Type u_1) [Field K] [NumberField K] {L : Type u_2} {M : Type u_3} [Field L] [NumberField L] [Field M] [NumberField M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] : relDiscr (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers M) = relDiscr (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ^ Module.finrank L M * (Ideal.relNorm (NumberField.RingOfIntegers K)) (relDiscr (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M))

The relative discriminant satisfies the transitivity formula in a tower of number fields.