Ramified support in towers of number fields #
Ramification cannot disappear after extending the top field of a tower: if a prime of ๐ K
ramifies in L, then it also ramifies in every finite extension M of L. Equivalently, the
ramified support of L / K is contained in that of M / K.
The result follows from the tower formula for relative discriminants. The relative discriminant
of L / K occurs to the positive power [M : L] as a factor of the relative discriminant of
M / K, so each of its prime divisors remains a prime divisor upstairs.
Main result #
TauCeti.NumberField.ramifiedSupport_mono: the ramified support is monotone in the top field of a tower.
References #
- J. Neukirch, Algebraic Number Theory, Chapter III, ยง2.
theorem
TauCeti.NumberField.ramifiedSupport_mono
(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]
:
ramifiedSupport K L โ ramifiedSupport K M
Ramified support is monotone in a tower. If K โ L โ M is a tower of number
fields, every prime of ๐ K ramified in L is also ramified in M.