The residue degree of a height-one prime over ℚ

A height-one prime 𝔭 of 𝓞 K lies over a unique rational prime p, and its absolute norm is p ^ f for f the residue degree Ideal.inertiaDeg 𝔭.asIdeal ℤ. This file names the two objects that description involves and records their elementary theory.

Main definitions

• TauCeti.rationalPrimeBelow 𝔭 is the rational prime below a height-one prime 𝔭 of 𝓞 K, namely the absolute norm of 𝔭 ∩ ℤ.
• TauCeti.higherDegreePrimes K is the set of height-one primes of 𝓞 K whose residue degree over ℚ exceeds 1.
• TauCeti.primesDividing K n hn is the finite set of height-one primes of 𝓞 K whose rational prime below divides a nonzero integer n.

Main results

• TauCeti.absNorm_eq_rationalPrimeBelow_pow: the absolute norm of 𝔭 is the rational prime below it raised to the residue degree.
• TauCeti.mem_higherDegreePrimes_iff_not_prime_absNorm: a height-one prime has residue degree above one exactly when its absolute norm is not a prime number.
• TauCeti.rationalPrimeBelow_pow_le_absNorm: the norm of 𝔭 is at least the rational prime below it raised to any power at most the residue degree.
• TauCeti.mem_higherDegreePrimes_of_one_lt_inertiaDeg: residue degree above one over an intermediate number field forces residue degree above one over ℚ.
• IsDedekindDomain.HeightOneSpectrum.absNorm_eq_absNorm_under_of_inertiaDeg_eq_one: a prime of residue degree one over an intermediate number field has the norm of the prime below it.
• TauCeti.card_filter_rationalPrimeBelow_le_finrank: at most [K : ℚ] height-one primes have a given rational prime below them.
• IsDedekindDomain.HeightOneSpectrum.encard_setOf_under_eq_le_finrank: at most [E : K] height-one primes of E contract to a given height-one prime of an intermediate number field K.
• IsDedekindDomain.HeightOneSpectrum.absNorm_dvd_rationalPrimeBelow_pow_finrank: the absolute norm of 𝔭 divides p ^ [K : ℚ], so the residue degree is at most the degree of the field.
• TauCeti.asIdeal_eq_span_singleton_of_absNorm_eq_pow_finrank: a prime of full residue degree is inert, that is, generated by the rational prime below it.
• IsDedekindDomain.HeightOneSpectrum.intCast_mem_asIdeal_iff: an integer belongs to a height-one prime exactly when the rational prime below it divides that integer.
• TauCeti.mem_primesDividing: the defining condition for membership in primesDividing.

Implementation notes

rationalPrimeBelow is named rather than spelled out as Ideal.absNorm (Ideal.under ℤ 𝔭.asIdeal) because the estimates downstream fibre the primes over it: keeping it a single head symbol is what makes the fibrewise rewriting elaborate, and it is the object Chebotarev will name when it compares a prime of K with the rational prime under it.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §8.

def TauCeti.higherDegreePrimes (K : Type u_2) [Field K] : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The height-one primes of 𝓞 K whose residue degree over ℚ is greater than one, that is, whose absolute norm is a proper power of the rational prime below them.

Equations

• TauCeti.higherDegreePrimes K = {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | 1 < 𝔭.asIdeal.inertiaDeg ℤ}

@[simp]

theorem TauCeti.mem_higherDegreePrimes {K : Type u_1} [Field K] {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} : 𝔭 ∈ higherDegreePrimes K ↔ 1 < 𝔭.asIdeal.inertiaDeg ℤ

The rational prime below a height-one prime

noncomputable def TauCeti.rationalPrimeBelow {K : Type u_1} [Field K] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ℕ

The rational prime below a height-one prime 𝔭 of 𝓞 K, that is, the residue characteristic of 𝔭. It is the absolute norm of the prime 𝔭 ∩ ℤ of ℤ.

Equations

• TauCeti.rationalPrimeBelow 𝔭 = Ideal.absNorm (Ideal.under ℤ 𝔭.asIdeal)

theorem TauCeti.rationalPrimeBelow_def {K : Type u_1} [Field K] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : rationalPrimeBelow 𝔭 = Ideal.absNorm (Ideal.under ℤ 𝔭.asIdeal)

The defining formula for TauCeti.rationalPrimeBelow.

theorem TauCeti.under_eq_span_rationalPrimeBelow {K : Type u_1} [Field K] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Ideal.under ℤ 𝔭.asIdeal = Ideal.span {↑(rationalPrimeBelow 𝔭)}

The prime of ℤ below a height-one prime 𝔭 of 𝓞 K is the ideal generated by TauCeti.rationalPrimeBelow 𝔭. This is the bridge that lets a fibre of the map rationalPrimeBelow be recognised as a set of primes over one ideal of ℤ.

theorem TauCeti.prime_rationalPrimeBelow {K : Type u_1} [Field K] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Nat.Prime (rationalPrimeBelow 𝔭)

The rational prime below a height-one prime really is a prime number.

theorem TauCeti.absNorm_eq_rationalPrimeBelow_pow {K : Type u_1} [Field K] [NumberField K] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Ideal.absNorm 𝔭.asIdeal = rationalPrimeBelow 𝔭 ^ 𝔭.asIdeal.inertiaDeg ℤ

The absolute norm of a height-one prime is the rational prime below it raised to the residue degree.

theorem TauCeti.mem_higherDegreePrimes_iff_not_prime_absNorm {K : Type u_1} [Field K] [NumberField K] {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} : 𝔭 ∈ higherDegreePrimes K ↔ ¬Nat.Prime (Ideal.absNorm 𝔭.asIdeal)

A height-one prime has residue degree above one exactly when its absolute norm is not a prime number: the norm is p ^ f, which is prime precisely for f = 1.

theorem TauCeti.rationalPrimeBelow_pow_le_absNorm {K : Type u_1} [Field K] [NumberField K] {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {n : ℕ} (hn : n ≤ 𝔭.asIdeal.inertiaDeg ℤ) : rationalPrimeBelow 𝔭 ^ n ≤ Ideal.absNorm 𝔭.asIdeal

The absolute norm of a height-one prime is at least the rational prime below it raised to any exponent bounded by the residue degree. The matching bound from above is the divisibility IsDedekindDomain.HeightOneSpectrum.absNorm_dvd_rationalPrimeBelow_pow_finrank. Use TauCeti.absNorm_eq_rationalPrimeBelow_pow for the exact value instead, and TauCeti.mem_higherDegreePrimes to supply the hypothesis at the common instance n = 2.

theorem TauCeti.mem_higherDegreePrimes_of_one_lt_inertiaDeg {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [Field E] [Algebra K E] {𝔓 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers E)} (h : 1 < 𝔓.asIdeal.inertiaDeg (NumberField.RingOfIntegers K)) : 𝔓 ∈ higherDegreePrimes E

A height-one prime of 𝓞 E whose residue degree over a number field K below E exceeds one has residue degree above one over ℚ, since residue degrees multiply along ℤ → 𝓞 K → 𝓞 E.

theorem IsDedekindDomain.HeightOneSpectrum.absNorm_eq_absNorm_under_of_inertiaDeg_eq_one {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [Field E] [NumberField E] [Algebra K E] {𝔓 : HeightOneSpectrum (NumberField.RingOfIntegers E)} (h : 𝔓.asIdeal.inertiaDeg (NumberField.RingOfIntegers K) = 1) : Ideal.absNorm 𝔓.asIdeal = Ideal.absNorm (under (NumberField.RingOfIntegers K) 𝔓).asIdeal

A height-one prime of 𝓞 E of residue degree one over a number field K below E has the same absolute norm as the prime of 𝓞 K below it.

Fibring the primes over the rational primes below them

theorem TauCeti.card_filter_rationalPrimeBelow_le_finrank {K : Type u_1} [Field K] [NumberField K] (F : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (m : ℕ) : {𝔮 ∈ F | rationalPrimeBelow 𝔮 = m}.card ≤ Module.finrank ℚ K

In any finite set of height-one primes of 𝓞 K, at most [K : ℚ] have a given rational prime below them: this is the height-one-spectrum fibre form of TauCeti.NumberField.card_primesOverFinset_le_finrank.

theorem IsDedekindDomain.HeightOneSpectrum.encard_setOf_under_eq_le_finrank {K : Type u_1} [Field K] [NumberField K] {E : Type u_2} [Field E] [NumberField E] [Algebra K E] (p : HeightOneSpectrum (NumberField.RingOfIntegers K)) : {P : HeightOneSpectrum (NumberField.RingOfIntegers E) | under (NumberField.RingOfIntegers K) P = p}.encard ≤ ↑(Module.finrank K E)

At most [E : K] height-one primes of E contract to a given height-one prime of K.

Inert primes

theorem IsDedekindDomain.HeightOneSpectrum.asIdeal_dvd_span_singleton_rationalPrimeBelow {K : Type u_1} [Field K] [NumberField K] (𝔭 : HeightOneSpectrum (NumberField.RingOfIntegers K)) : 𝔭.asIdeal ∣ Ideal.span {↑(TauCeti.rationalPrimeBelow 𝔭)}

Every height-one prime divides the ideal generated by the rational prime below it.

theorem IsDedekindDomain.HeightOneSpectrum.absNorm_dvd_rationalPrimeBelow_pow_finrank {K : Type u_1} [Field K] [NumberField K] (𝔭 : HeightOneSpectrum (NumberField.RingOfIntegers K)) : Ideal.absNorm 𝔭.asIdeal ∣ TauCeti.rationalPrimeBelow 𝔭 ^ Module.finrank ℚ K

The residue degree is at most the degree of the field. The absolute norm of a height-one prime 𝔭 divides p ^ [K : ℚ], where p is the rational prime below 𝔭: indeed 𝔭 divides the ideal generated by p, whose absolute norm is that power.

theorem TauCeti.asIdeal_eq_span_singleton_of_absNorm_eq_pow_finrank {K : Type u_1} [Field K] [NumberField K] {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h : Ideal.absNorm 𝔭.asIdeal = rationalPrimeBelow 𝔭 ^ Module.finrank ℚ K) : 𝔭.asIdeal = Ideal.span {↑(rationalPrimeBelow 𝔭)}

A prime of full residue degree is inert. If the absolute norm of 𝔭 is the full power p ^ [K : ℚ] of the rational prime below it, then 𝔭 is the ideal generated by p: the two ideals are comparable and have the same absolute norm.

The primes dividing an integer

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.intCast_mem_asIdeal_iff {K : Type u_1} [Field K] (𝔭 : HeightOneSpectrum (NumberField.RingOfIntegers K)) (n : ℤ) : ↑n ∈ 𝔭.asIdeal ↔ ↑(TauCeti.rationalPrimeBelow 𝔭) ∣ n

An integer belongs to a height-one prime exactly when the rational prime below it divides that integer.

noncomputable def TauCeti.primesDividing (K : Type u_2) [Field K] [NumberField K] (n : ℤ) (hn : n ≠ 0) : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The height-one primes of 𝓞 K dividing a nonzero integer n: those whose rational prime below divides n. This is the excluded set an ideal-theoretic Artin map of conductor n is defined away from.

Equations

• TauCeti.primesDividing K n hn = ⋯.toFinset

@[simp]

theorem TauCeti.mem_primesDividing {K : Type u_1} [Field K] [NumberField K] {n : ℤ} (hn : n ≠ 0) (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : 𝔭 ∈ primesDividing K n hn ↔ ↑(rationalPrimeBelow 𝔭) ∣ n

The defining condition for membership in primesDividing.