The ramified support of an extension of number fields

The primes of 𝓞 K that ramify in L are exactly those dividing the relative discriminant relDiscr (𝓞 K) (𝓞 L), and there are finitely many of them. This file collects them into a Finset of height-one primes, the ramified support of L / K.

Finiteness is not an extra hypothesis: the relative discriminant of a separable extension is nonzero (TauCeti.relDiscr_ne_bot), and a nonzero ideal of a Dedekind domain has finitely many prime divisors (Ideal.finite_factors). For number fields the separability is automatic.

Main definitions

• TauCeti.NumberField.ramifiedSupport: the primes of 𝓞 K dividing relDiscr (𝓞 K) (𝓞 L).

Main results

• TauCeti.NumberField.mem_ramifiedSupport: membership is divisibility of the relative discriminant.
• TauCeti.NumberField.mem_ramifiedSupport_iff_exists: equivalently, some prime of 𝓞 L above v has ramification index greater than one — so the name is honest.
• TauCeti.NumberField.ramifiedSupport_self: nothing ramifies in the identity extension, so the support of K / K is empty.
• TauCeti.NumberField.isUnramifiedAway_ramifiedSupport: primes outside the ramified support are unramified throughout the extension.
• TauCeti.NumberField.exists_liesOver_isUnramifiedAt_of_notMem_finset: a place outside a finite set containing the ramified support has an unramified place above it.

References

• J. Neukirch, Algebraic Number Theory, Chapter III, §2.

noncomputable def TauCeti.NumberField.ramifiedSupport (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The ramified support of L / K: the height-one primes of 𝓞 K dividing the relative discriminant relDiscr (𝓞 K) (𝓞 L).

This is a Finset because the relative discriminant is nonzero, a nonzero ideal of a Dedekind domain having only finitely many prime divisors.

@[simp]

theorem TauCeti.NumberField.mem_ramifiedSupport {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} : v ∈ ramifiedSupport K L ↔ v.asIdeal ∣ relDiscr (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

A prime lies in the ramified support exactly when it divides the relative discriminant.

theorem TauCeti.NumberField.mem_ramifiedSupport_iff_exists {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} : v ∈ ramifiedSupport K L ↔ ∃ (P : ↑(v.asIdeal.primesOver (NumberField.RingOfIntegers L))), 1 < (↑P).ramificationIdx (NumberField.RingOfIntegers K)

The ramified support consists of the primes that actually ramify. A prime lies in it exactly when some prime of 𝓞 L above it has ramification index greater than one.

@[simp]

theorem TauCeti.NumberField.ramifiedSupport_self (K : Type u_1) [Field K] [NumberField K] : ramifiedSupport K K = ∅

Nothing ramifies in the identity extension: the ramified support of K / K is empty.

theorem TauCeti.NumberField.isUnramifiedAway_ramifiedSupport {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : v ∉ ramifiedSupport K L → ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q

Every prime outside the ramified support is unramified. If a finite place v does not divide the relative discriminant of L/K, then every prime of L above v is unramified over K. This is the unramified-away hypothesis that specializations of the Artin map consume.

theorem TauCeti.NumberField.exists_liesOver_isUnramifiedAt_of_notMem_finset {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ramifiedSupport K L ⊆ S) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hv : v ∉ ↑S) : ∃ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), w.asIdeal.LiesOver v.asIdeal ∧ Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal

If the places outside a finite set S containing the ramified support of L/K are unramified, then every place of K outside S has an unramified place of L above it.