Local invariants over ℤ and over 𝓞 ℚ

The ring of integers of ℚ is ℤ (Rat.ringOfIntegersEquiv), but the two are different types, and the local invariants of an ideal P of an 𝓞 ℚ-algebra S, such as the ring of integers of a number field, can be taken relative to either base ring: the residue degree P.inertiaDeg ℤ or P.inertiaDeg (𝓞 ℚ), the ramification index P.ramificationIdx ℤ or P.ramificationIdx (𝓞 ℚ), and the arithmetic Frobenius condition IsArithFrobAt ℤ σ P or IsArithFrobAt (𝓞 ℚ) σ P; likewise the different of a number field. Statements about number fields over ℚ as a base field naturally produce the 𝓞 ℚ versions, while statements about rational primes produce the ℤ versions. This file proves that they agree; the comparison lemmas are simp lemmas oriented towards the ℤ forms. It then states the Frobenius order and prime-count formulas of Galois number fields over ℤ, and records the absolute norms of the ideals of 𝓞 ℚ.

Main results

• TauCeti.differentIdeal_ringOfIntegers_rat_eq_int: the differents over 𝓞 ℚ and over ℤ agree.
• Ideal.under_ringOfIntegers_rat_eq_map: the ideal of 𝓞 ℚ below P is the image of the ideal of ℤ below P.
• Ideal.inertiaDeg_ringOfIntegers_rat_eq_int: the residue degrees over 𝓞 ℚ and over ℤ agree.
• Ideal.ramificationIdx_ringOfIntegers_rat_eq_int: the ramification indices over 𝓞 ℚ and over ℤ agree.
• Ideal.isArithFrobAt_ringOfIntegers_rat_iff: the Frobenius conditions over 𝓞 ℚ and over ℤ agree.
• Ideal.inertiaDeg_eq_orderOf and Ideal.ncard_primesOver_mul_inertiaDeg_eq_finrank_of_isUnramifiedAt: the unramified Frobenius order and prime-count formulas over ℤ.
• Ideal.inertiaDeg_dvd_orderOf and Ideal.inertiaDeg_eq_one_iff_mem_inertia: at a possibly ramified prime, the residue degree over ℤ divides the order of a Frobenius, and is 1 exactly when that Frobenius lies in the inertia subgroup.
• Ideal.primesOver_under_ringOfIntegers_rat_eq: for an ideal Q lying over an ideal p of ℤ, the primes above Q ∩ 𝓞 ℚ are the primes above p.
• Rat.HeightOneSpectrum.absNorm_asIdeal: the absolute norm of a height-one prime of 𝓞 ℚ is the rational prime it corresponds to, and Rat.HeightOneSpectrum.exists_absNorm_eq shows every rational prime arises this way.
• Rat.RingOfIntegers.ideal_span_absNorm_eq_self: every ideal of 𝓞 ℚ is generated by its absolute norm.

@[simp]

theorem TauCeti.differentIdeal_ringOfIntegers_rat_eq_int {K : Type u_1} [Field K] [NumberField K] : differentIdeal (NumberField.RingOfIntegers ℚ) (NumberField.RingOfIntegers K) = differentIdeal ℤ (NumberField.RingOfIntegers K)

The different of a number field over 𝓞 ℚ agrees with its different over ℤ.

theorem Rat.algebraMap_int_ringOfIntegers_eq : algebraMap ℤ (NumberField.RingOfIntegers ℚ) = ↑ringOfIntegersEquiv.symm

The structure map ℤ → 𝓞 ℚ is the inverse of Rat.ringOfIntegersEquiv.

theorem Rat.algebraMap_int_ringOfIntegers_bijective : Function.Bijective ⇑(algebraMap ℤ (NumberField.RingOfIntegers ℚ))

The structure map ℤ → 𝓞 ℚ is bijective.

theorem Ideal.under_ringOfIntegers_rat_eq_map {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] (P : Ideal S) : under (NumberField.RingOfIntegers ℚ) P = map (algebraMap ℤ (NumberField.RingOfIntegers ℚ)) (under ℤ P)

The ideal of 𝓞 ℚ below an ideal P is the image of the ideal of ℤ below P.

@[simp]

theorem Ideal.absNorm_under_ringOfIntegers_rat {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] (P : Ideal S) : absNorm (under (NumberField.RingOfIntegers ℚ) P) = absNorm (under ℤ P)

The absolute norm of the ideal of 𝓞 ℚ below P is that of the ideal of ℤ below P.

@[simp]

theorem Ideal.card_quot_under_ringOfIntegers_rat {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] (P : Ideal S) : Nat.card (NumberField.RingOfIntegers ℚ ⧸ under (NumberField.RingOfIntegers ℚ) P) = Nat.card (ℤ ⧸ under ℤ P)

The residue rings of 𝓞 ℚ and of ℤ below P have the same number of elements.

@[simp]

theorem Ideal.isArithFrobAt_ringOfIntegers_rat_iff {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] {G : Type u_2} [Monoid G] [MulSemiringAction G S] [SMulCommClass G ℤ S] [SMulCommClass G (NumberField.RingOfIntegers ℚ) S] (σ : G) (Q : Ideal S) : IsArithFrobAt (NumberField.RingOfIntegers ℚ) σ Q ↔ IsArithFrobAt ℤ σ Q

Frobenius elements over 𝓞 ℚ and over ℤ are the same. An element σ is an arithmetic Frobenius at Q relative to the base ring 𝓞 ℚ exactly when it is one relative to ℤ.

@[simp]

theorem Ideal.inertiaDeg_ringOfIntegers_rat_eq_int {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] (P : Ideal S) : P.inertiaDeg (NumberField.RingOfIntegers ℚ) = P.inertiaDeg ℤ

The residue degree over ℤ is the residue degree over 𝓞 ℚ.

@[simp]

theorem Ideal.ramificationIdx_ringOfIntegers_rat_eq_int {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] [Module.Flat (NumberField.RingOfIntegers ℚ) S] (P : Ideal S) : P.ramificationIdx (NumberField.RingOfIntegers ℚ) = P.ramificationIdx ℤ

The ramification index over ℤ is the ramification index over 𝓞 ℚ.

theorem Ideal.primesOver_under_ringOfIntegers_rat_eq {S : Type u_1} [CommRing S] [Algebra (NumberField.RingOfIntegers ℚ) S] {T : Type u_2} [CommRing T] [Algebra (NumberField.RingOfIntegers ℚ) T] {p : Ideal ℤ} (Q : Ideal T) [Q.LiesOver p] : (under (NumberField.RingOfIntegers ℚ) Q).primesOver S = p.primesOver S

The primes of S above Q ∩ 𝓞 ℚ are the primes above p, when Q lies over the ideal p of ℤ.

@[simp]

theorem Rat.HeightOneSpectrum.absNorm_asIdeal (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) : Ideal.absNorm v.asIdeal = natGenerator v

The absolute norm of a height-one prime of 𝓞 ℚ is the rational prime generating its image in ℤ.

@[simp]

theorem Rat.HeightOneSpectrum.natCast_mem_iff_absNorm_asIdeal_dvd (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) {n : ℕ} : ↑n ∈ v.asIdeal ↔ Ideal.absNorm v.asIdeal ∣ n

A natural number belongs to a rational prime ideal exactly when its norm divides it.

theorem Rat.HeightOneSpectrum.exists_absNorm_eq {p : ℕ} (hp : Nat.Prime p) : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)), Ideal.absNorm v.asIdeal = p

Every rational prime is the absolute norm of a height-one prime of 𝓞 ℚ.

@[simp]

theorem Rat.RingOfIntegers.ideal_span_absNorm_eq_self (J : Ideal (NumberField.RingOfIntegers ℚ)) : Ideal.span {↑(Ideal.absNorm J)} = J

Every ideal of 𝓞 ℚ is generated by its absolute norm, the 𝓞 ℚ form of Int.ideal_span_absNorm_eq_self.

@[simp]

theorem Rat.RingOfIntegers.natCast_dvd_natCast {m n : ℕ} : ↑m ∣ ↑n ↔ m ∣ n

Divisibility of natural numbers in 𝓞 ℚ is divisibility in ℕ, transported along Rat.ringOfIntegersEquiv : 𝓞 ℚ ≃+* ℤ.

theorem Ideal.inertiaDeg_eq_orderOf {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers ℚ) Q] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : Q.inertiaDeg ℤ = orderOf σ

At an unramified prime of a Galois number field, the residue degree over ℤ is the order of a Frobenius.

theorem Ideal.inertiaDeg_dvd_orderOf {K : Type u_1} [Field K] [NumberField K] (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : Q.inertiaDeg ℤ ∣ orderOf σ

At any prime of a number field, ramified or not, the residue degree over ℤ divides the order of a Frobenius. This is Ideal.inertiaDeg_dvd_orderOf_of_isArithFrobAt with base ring ℤ.

theorem Ideal.inertiaDeg_eq_one_iff_mem_inertia {K : Type u_1} [Field K] [NumberField K] (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : Q.inertiaDeg ℤ = 1 ↔ σ ∈ inertia Gal(K/ℚ) Q

At any prime of a number field, ramified or not, the residue degree over ℤ is 1 exactly when a Frobenius lies in the inertia subgroup. This is Ideal.inertiaDeg_eq_one_iff_mem_inertia_of_isArithFrobAt with base ring ℤ.

theorem Ideal.ncard_primesOver_mul_inertiaDeg_eq_finrank_of_isUnramifiedAt {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] {p : ℕ} [NeZero p] (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] [Q.LiesOver (span {↑p})] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers ℚ) Q] : ((span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard * Q.inertiaDeg ℤ = Module.finrank ℚ K

At an unramified prime of a Galois number field, the number of primes above p times the residue degree is [K : ℚ].