Ramification at primes dividing a cyclotomic level

For a cyclotomic extension of ℚ, a prime dividing the level ramifies, provided that a prime of norm two divides the level to at least the second power. This excludes primes dividing the level from Frobenius fibres when the level is not congruent to two modulo four.

References

• L. Washington, Introduction to Cyclotomic Fields, Chapter 2.
• IsCyclotomicExtension.Rat.ramificationIdx_eq in Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal supplies the ramification-index formula.

theorem NumberField.Chebotarev.mem_ramifiedPrimes_of_natCast_mem (F : Type u_1) [Field F] [NumberField F] (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ F] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ)} (hn : Ideal.absNorm 𝔭.asIdeal = 2 → 4 ∣ n) (hm : ↑n ∈ 𝔭.asIdeal) : 𝔭 ∈ ramifiedPrimes ℚ F

Every prime dividing a cyclotomic level ramifies, provided the level is divisible by four when the prime has norm two.