The relation between the ramified primes of a quadratic field #
Let K = ℚ(√d) be a quadratic number field, presented by θ : 𝓞 K with
minpoly ℤ θ = X ^ 2 - d and Algebra.adjoin ℚ {θ} = ⊤, with d squarefree. Every rational
prime p dividing d ramifies, so p 𝓞 K = 𝔭 ^ 2 for the unique prime 𝔭 of 𝓞 K above it
(TauCeti.Multiquadratic.map_span_eq_sq_of_dvd_fundamentalDiscriminant). Squaring the principal
ideal (θ) gives (d), which is the product of those p 𝓞 K; cancelling the square in the
factorisation monoid of ideals leaves
(θ) = ∏_{p ∣ d} 𝔭_p.
This is an explicit relation of genus theory. The classes [𝔭_p] of the ramified primes are
2-torsion (NumberField.classGroupMk0_sq_eq_one_of_mem_ramifiedPrimes), so they span an
elementary-2 subgroup of Cl(𝓞 K), a priori of order at most 2 ^ t with t the number
of ramified primes (ncard_ramifiedPrimes_eq_card). The identity above says that the product of
those spanning classes over p ∣ d is trivial, so they are generated by all but one prime factor
of d and span at most 2 ^ (t - 1) classes. The matching lower bound is not proved here. In the
2-rank
formula rank = t - 1 of the Multiquadratic roadmap this is where the - 1 comes from; for real
quadratic fields that exact formula concerns the narrow class group, while this file only gives an
upper bound in the ordinary class group.
Because the ramified primes are exactly those dividing fundamentalDiscriminant d, which is d
or 4 * d, the product here runs over p ∣ d. It covers all ramified primes unless
d ≡ 3 (mod 4), in which case exactly the ramified prime 2 is omitted. That is why the counting
statement takes the ambient set of ramified primes as a parameter s and only asks that it contain
the prime factors of d: the relation lives on the prime factors of the radicand, while the classes
being counted are those of all the ramified primes.
The primes above the rational primes involved may be supplied by the caller as a family (P for
the ideal identity, Q for the class-group statements). The theorem
exists_span_singleton_eq_prod_primeFactors also chooses a family with the nonzero-divisor
packaging needed by ClassGroup.mk0.
The classical source for the relation and its use in genus theory is D. A. Cox, Primes of the Form x² + ny², Chapter 3, and F. Lemmermeyer, Reciprocity Laws, Chapter 6.
Main results #
TauCeti.Multiquadratic.mem_ramifiedPrimes_of_mem_primeFactors: a prime factor of the radicand ramifies.TauCeti.Multiquadratic.span_singleton_eq_prod_primeFactors:(θ) = ∏_{p ∣ d} 𝔭_p.TauCeti.Multiquadratic.exists_span_singleton_eq_prod_primeFactors: a family of primes above the prime factors ofdexists and satisfies this identity.TauCeti.Multiquadratic.prod_classGroupMk0_eq_one: the product of the classes[𝔭_p]over the prime factors ofdis trivial inCl(𝓞 K).TauCeti.Multiquadratic.prod_classGroupMk0_eq_prod_sdiff: consequently the class of a sub-product is the class of its complementary sub-product.TauCeti.Multiquadratic.natCard_closure_image_classGroupMk0_le: the subgroup generated by the classes of the ramified primes has at most2 ^ (t - 1)elements.
A prime factor of the radicand is a ramified prime of ℚ(√d).
The square root of the radicand generates the product of the ramified primes dividing it.
Let K = ℚ(√d) with d squarefree, and for every prime factor p of d let P p be the prime
of 𝓞 K above p. Then the principal ideal generated by θ is the product of those primes:
(θ) = ∏_{p ∣ d} 𝔭_p.
Squaring both sides gives (d) = ∏_p p 𝓞 K, which holds because p 𝓞 K = 𝔭_p ^ 2 at every
ramified prime and d is squarefree; the ideals of a Dedekind domain form a factorisation monoid
with no 2-torsion, so the squares may be cancelled.
There is a family of prime ideals above the prime factors of d for which the square root
relation holds. The ideals are packaged as non-zero-divisors, so the same family can be used in
the class-group results below.
An explicit relation of genus theory. In Cl(𝓞 K) for K = ℚ(√d) with d squarefree, the
product of the classes of the primes above the prime factors of d is trivial: their product is
the principal ideal (θ) by span_singleton_eq_prod_primeFactors.
Together with the fact that each such class is 2-torsion
(NumberField.classGroupMk0_sq_eq_one_of_mem_ramifiedPrimes) this bounds the elementary-2 subgroup
they span by 2 ^ (t - 1) elements.
Complementary sub-products of the primes above the prime factors of d have the same
class. For a subset S of the prime factors of d, the class of ∏_{p ∈ S} 𝔭_p equals the
class of the complementary
product ∏_{p ∉ S} 𝔭_p. This is prod_classGroupMk0_eq_one combined with the 2-torsion of the
individual classes, and it is the concrete form of an explicit relation among the generators of
the elementary-2 subgroup spanned by the ramified-prime classes.
The classes of the ramified primes generate a subgroup of order at most
2 ^ (t - 1). Let s be a finite set of ramified primes of K = ℚ(√d) containing every
prime factor of d, with Q p the prime of 𝓞 K above p ∈ s. Then the subgroup of
Cl(𝓞 K) generated by their classes has at most 2 ^ (#s - 1) elements.
The classes are involutions, so the subgroup they generate is the set of sub-products, of which
there are at most 2 ^ #s; the relation prod_classGroupMk0_eq_one over the prime factors of d
removes one generator (TauCeti.natCard_closure_image_le_two_pow_card_sub_one). The hypothesis
1 < |d| excludes d = -1, the one radicand with no prime factor and hence no relation.
This is only an upper bound in the ordinary class group; no matching lower bound is asserted.