The primes of a number field ramifying in a finite extension

For an extension L / K of number fields, a height-one prime 𝔭 of 𝓞 K is ramified in L when some prime Q of 𝓞 L lying over it is ramified, i.e. when

¬ ∀ (Q : Ideal (𝓞 L)) [Q.IsPrime] [Q.LiesOver 𝔭.asIdeal], Algebra.IsUnramifiedAt (𝓞 K) Q.

Only finitely many 𝔭 are ramified, because each of them is the contraction of a prime dividing the different ideal differentIdeal (𝓞 K) (𝓞 L), which is nonzero and so has finitely many prime divisors. That finiteness is what lets the ramified primes be packaged as a Finset, which is the form Chebotarev's exceptional set is used in: the density statements discard ramifiedPrimes K L and argue about the complement.

The ramification condition is spelled out with Mathlib's Algebra.IsUnramifiedAt rather than wrapped in a named predicate, matching how the roadmap states it. A Prop-valued abbreviation for "𝔭 is unramified in L" would duplicate Algebra.IsUnramifiedIn.

Main definitions

• NumberField.Chebotarev.ramifiedPrimes: the finite set of height-one primes of 𝓞 K that ramify in L.

Main results

• TauCeti.eventually_isUnramifiedAt_liesOver: almost every finite place has only unramified places above it.
• NumberField.Chebotarev.mem_ramifiedPrimes_iff: the defining condition for membership.
• NumberField.Chebotarev.isUnramifiedAt_of_under_eq: a prime of L over a prime of K above which every prime of L is unramified is unramified over K.
• NumberField.Chebotarev.under_notMem_ramifiedPrimes_iff_isUnramifiedAt: in a Galois extension, unramifiedness can be tested at one prime above the base prime.
• NumberField.Chebotarev.ramifiedPrimes_subset_ramifiedPrimes: for a tower K ⊆ L ⊆ M, every prime of K ramifying in L also ramifies in M.

Relation to the absolute NumberField.ramifiedPrimes

Every name used here already exists one namespace up, and this is deliberate rather than an oversight. TauCeti/NumberTheory/NumberField/RamifiedPrimes.lean carries

• NumberField.ramifiedPrimes (K) : Set ℕ, the rational primes ramifying in K,
• @[simp] NumberField.mem_ramifiedPrimes_iff, proved by Iff.rfl, and
• NumberField.finite_ramifiedPrimes,

i.e. the same short names, in the same shape. They are kept apart rather than unified:

• They are the same shape — "not Algebra.IsUnramifiedIn the top ring at an ideal of the base" — but at different bases. The absolute one is ℤ-to-𝓞 K; this one is 𝓞 K-to-𝓞 L. Neither is an instance of the other without also transporting the carrier.
• The carriers genuinely differ: Set ℕ against Finset (HeightOneSpectrum (𝓞 K)). For K = ℚ the two agree only through 𝓞 ℚ ≃ ℤ and HeightOneSpectrum ℤ ≃ the rational primes, and neither identification is definitional.
• Generalising the absolute version instead would change its carrier, and Tau Ceti keeps no compatibility shims, so every use would have to move in this PR — ten files on main reference that API, seven of them under Multiquadratic/. Its Set ℕ packaging is, in its own docstring, "the form in which t is counted" for genus theory.

Two consequences to be aware of when using this file. First, NumberField.Chebotarev is nested inside NumberField, so within it a bare ramifiedPrimes or mem_ramifiedPrimes_iff resolves to the declaration here and shadows the absolute one; a Chebotarev file that also wants the absolute notion must write _root_.NumberField.ramifiedPrimes. (The finiteness lemma is private, so its name collides only inside this file.) Second, both _iff lemmas are @[simp], but their left-hand sides head-match on different types — membership in a Set ℕ against membership in a Finset (HeightOneSpectrum (𝓞 K)) — so simp never has to choose between them.

References

Adapted from finite_ramifiedIn in CebotarevDensity/Frobenius.lean of CBirkbeck/chebotarev-density (Apache-2.0, Birkbeck--Brasca) at commit 8575c9df1ae0a61120ab5c964c7911414254bec7, where the statement is a Set.Finite over Ideal (𝓞 K) phrased through a source-local unramifiedness predicate. The covering argument through the different ideal is the source's; the carrier is the roadmap's.

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

The primes of K that ramify in L. The height-one primes 𝔭 of 𝓞 K for which some prime of 𝓞 L over 𝔭 is ramified, collected into a Finset by finite_ramifiedPrimes.

This is the relative notion; _root_.NumberField.ramifiedPrimes is the absolute one, over ℤ and valued in Set ℕ. See the module docstring.

@[simp]

theorem NumberField.Chebotarev.mem_ramifiedPrimes_iff {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : 𝔭 ∈ ramifiedPrimes K L ↔ ¬∀ (Q : Ideal (RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver 𝔭.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q

The defining condition for membership in ramifiedPrimes.

theorem NumberField.Chebotarev.isUnramifiedAt_of_under_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (p : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (hur : ∀ (R : Ideal (RingOfIntegers L)) [inst : R.IsPrime] [R.LiesOver p.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) R) (Q : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) (hQp : IsDedekindDomain.HeightOneSpectrum.under (RingOfIntegers K) Q = p) : Algebra.IsUnramifiedAt (RingOfIntegers K) Q.asIdeal

A prime of L over a prime p of K above which every prime of L is unramified is unramified over K.

theorem NumberField.Chebotarev.under_notMem_ramifiedPrimes_iff_isUnramifiedAt {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (Q : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) : IsDedekindDomain.HeightOneSpectrum.under (RingOfIntegers K) Q ∉ ramifiedPrimes K L ↔ Algebra.IsUnramifiedAt (RingOfIntegers K) Q.asIdeal

In a Galois extension, a prime of the base is unramified exactly when one prime above it is unramified.

theorem NumberField.Chebotarev.ramifiedPrimes_subset_ramifiedPrimes {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {M : Type u_3} [Field M] [NumberField M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : ramifiedPrimes K L ⊆ ramifiedPrimes K M

Ramification ascends a tower. For number fields K ⊆ L ⊆ M, a prime of K that ramifies in L also ramifies in M. Equivalently, a prime unramified in M is unramified in every intermediate field.

theorem TauCeti.eventually_isUnramifiedAt_liesOver (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)) in Filter.cofinite, ∀ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal

Almost every finite place of a number field has only unramified primes above it.