A conjugation-stable prime over an unramified rational prime is inert

Let K be a number field of degree 2 over ℚ. Such a field is Galois by Mathlib's Algebra.IsQuadraticExtension.isGalois instance, and its Galois group has order 2. Consequently the two elements of that group act on the primes of 𝓞 K above a rational prime p transitively, and a prime 𝔭 above p fixed by the nontrivial automorphism is the only prime above p.

Adding that p is unramified turns that into

p 𝓞 K = 𝔭,

so p is inert and 𝔭 is principal. Together with the ramified case (TauCeti.NumberTheory.NumberField.Quadratic.TotalRamification, where p 𝓞 K = 𝔭 ^ 2) this disposes of every prime that quadratic conjugation fixes: it is either principal, or one of the finitely many primes above a ramified rational prime. That dichotomy is what makes the classes of the ramified primes generate the ambiguous ideal classes of K in TauCeti.NumberTheory.NumberField.Quadratic.Conjugation.Ambiguous.Ideal, the descent step of the ambiguous class number formula of genus theory.

The automorphism is supplied as a ℚ-algebra automorphism f of K together with a ring automorphism σ of 𝓞 K restricting it; that is the shape in which NumberField.ringOfIntegersQuadraticConj and NumberField.coe_ringOfIntegersQuadraticConj present quadratic conjugation.

See D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2, for the classical genus theory in which this dichotomy is used.

Main results

• NumberField.primesOver_eq_singleton_of_map_eq_self: a prime fixed by the nontrivial automorphism is the unique prime above the rational prime it lies over.
• NumberField.map_span_eq_of_notMem_ramifiedPrimes: if that rational prime is moreover unramified, then p 𝓞 K = 𝔭, so 𝔭 is principal.

theorem NumberField.primesOver_eq_singleton_of_map_eq_self {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hp : Nat.Prime p) {f : Gal(K/ℚ)} (hf : f ≠ 1) {σ : RingOfIntegers K ≃+* RingOfIntegers K} (hσ : ∀ (x : RingOfIntegers K), ↑(σ x) = f ↑x) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] (hfix : Ideal.map σ 𝔭 = 𝔭) : (Ideal.span {↑p}).primesOver (RingOfIntegers K) = {𝔭}

A conjugation-stable prime is the unique prime above its rational prime. In a quadratic number field the Galois group has order two, so it acts transitively on the primes above a rational prime p through the single nontrivial automorphism f. A prime 𝔭 above p that f fixes is therefore the whole of that orbit.

theorem NumberField.map_span_eq_of_notMem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hp : Nat.Prime p) (hmem : p ∉ ramifiedPrimes K) {f : Gal(K/ℚ)} (hf : f ≠ 1) {σ : RingOfIntegers K ≃+* RingOfIntegers K} (hσ : ∀ (x : RingOfIntegers K), ↑(σ x) = f ↑x) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] (hfix : Ideal.map σ 𝔭 = 𝔭) : Ideal.map (algebraMap ℤ (RingOfIntegers K)) (Ideal.span {↑p}) = 𝔭

A conjugation-stable prime over an unramified rational prime is inert. If p does not ramify in the quadratic number field K and the prime 𝔭 above it is fixed by the nontrivial automorphism, then p 𝓞 K = 𝔭: the ideal generated by p is already prime.