The completely split primes as the identity Artin fibre

Let L / K be a finite Galois extension of number fields. Among the fibres of the Artin class studied in TauCeti.NumberTheory.Chebotarev.FrobeniusPrimeSet, the fibre of the identity class 1 is distinguished: it consists exactly of the primes of 𝓞 K that split completely in L.

Two readings of membership in frobeniusPrimeSet K L 1 are recorded. The residue-degree reading asks for a prime 𝔭 unramified in L, and says that f(Q/𝔭) is 1 at one — hence, since L / K is Galois, at every — prime Q of 𝓞 L above 𝔭. The counting reading needs no hypothesis at all: 𝔭 carries the identity Artin class exactly when 𝓞 L has the full complement of [L : K] primes above 𝔭.

That asymmetry is the point of the file. A full complement of primes above 𝔭 already forces the ramification index at every prime above 𝔭 to be 1, hence forces 𝔭 to be unramified — that is Ideal.isUnramifiedAt_of_ncard_primesOver_eq_finrank, in TauCeti.NumberTheory.NumberField.SplitsCompletely.Basic. So the counting characterization and its set-level corollary both stand unconditionally, and frobeniusPrimeSet K L 1 is the set of completely split primes on the nose, with no finite exceptional set to discard.

Main results

• NumberField.Chebotarev.mem_frobeniusPrimeSet_one_iff_inertiaDeg_eq_one: for 𝔭 unramified in L, membership in the identity fibre is residue degree one at a prime above 𝔭.
• NumberField.Chebotarev.mem_frobeniusPrimeSet_one_iff_ncard_primesOver_eq_finrank: the same membership, read as a count of the primes above 𝔭.
• NumberField.Chebotarev.inertiaDeg_eq_one_of_mem_frobeniusPrimeSet_one: a member of the identity fibre has residue degree one at every prime above it.
• NumberField.Chebotarev.frobeniusPrimeSet_one_eq_setOf_ncard_primesOver_eq_finrank: as a set, the identity fibre is the primes of 𝓞 K with [L : K] primes of 𝓞 L above them.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9, where the Frobenius at an unramified prime is trivial exactly when that prime splits completely.

theorem NumberField.Chebotarev.mem_frobeniusPrimeSet_one_iff_inertiaDeg_eq_one {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} (hur : ∀ (Q : Ideal (RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver 𝔭.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q) (Q : Ideal (RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver 𝔭.asIdeal] : 𝔭 ∈ frobeniusPrimeSet K L 1 ↔ Q.inertiaDeg (RingOfIntegers K) = 1

The identity fibre is residue degree one. For 𝔭 unramified in L and Q a prime of 𝓞 L above 𝔭, the prime 𝔭 carries the identity Artin class exactly when f(Q/𝔭) = 1.

The residue degree is common to all primes above 𝔭, so the choice of Q is immaterial; see inertiaDeg_eq_one_of_mem_frobeniusPrimeSet_one.

theorem NumberField.Chebotarev.mem_frobeniusPrimeSet_one_iff_ncard_primesOver_eq_finrank {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} : 𝔭 ∈ frobeniusPrimeSet K L 1 ↔ (𝔭.asIdeal.primesOver (RingOfIntegers L)).ncard = Module.finrank K L

The identity fibre is complete splitting. A height-one prime of 𝓞 K carries the identity Artin class in L exactly when 𝓞 L has [L : K] primes above it.

No unramifiedness hypothesis is needed: complete splitting already implies it, so requiring it separately would be redundant.

theorem NumberField.Chebotarev.inertiaDeg_eq_one_of_mem_frobeniusPrimeSet_one {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} (h : 𝔭 ∈ frobeniusPrimeSet K L 1) (Q : Ideal (RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver 𝔭.asIdeal] : Q.inertiaDeg (RingOfIntegers K) = 1

Residue degree one at every prime above. A member of the identity fibre has residue degree 1 at each prime of 𝓞 L lying over it, not merely at one of them.

theorem NumberField.Chebotarev.frobeniusPrimeSet_one_eq_setOf_ncard_primesOver_eq_finrank {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : frobeniusPrimeSet K L 1 = {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) | (𝔭.asIdeal.primesOver (RingOfIntegers L)).ncard = Module.finrank K L}

The identity fibre is exactly the completely split primes. A height-one prime of 𝓞 K carries the identity Artin class in L if and only if 𝓞 L has [L : K] primes above it.

Complete splitting is therefore a fibre of the Artin class with no exceptional set attached, so a density statement for the fibre is a density statement for the completely split primes.