The ray class number formula

Let 𝔪 be a modulus of a number field K, and write A 𝔪 = (𝓞 K ⧸ 𝔪.finitePart)ˣ × (𝔪.infinitePart → ℤˣ) for its residue units and prescribed signs. The exact sequence constructed in TauCeti.NumberTheory.NumberField.Global.RayClass.Exact is

1 → unitsCongruenceSubgroup 𝔪 → (𝓞 K)ˣ → A 𝔪 → RayClassGroup 𝔪 → ClassGroup (𝓞 K) → 1

and this file reads off the ray class number formula

#(RayClassGroup 𝔪) * [(𝓞 K)ˣ : unitsCongruenceSubgroup 𝔪]
  = #(ClassGroup (𝓞 K)) * #(𝓞 K ⧸ 𝔪.finitePart)ˣ * 2 ^ #𝔪.infinitePart.

The right-hand tail A 𝔪 → RayClassGroup 𝔪 → ClassGroup (𝓞 K) → 1 refines the exact tail of TauCeti.NumberTheory.NumberField.Global.RayClass.Exact, whose left-hand term is the larger group primeToSubgroup 𝔪: by residueSignEquiv, the principal ray class of an element prime to 𝔪 depends only on its residue and its signs, so principalRayClass 𝔪 descends to A 𝔪.

The left-hand part is the unit obstruction. An element prime to 𝔪 has trivial principal ray class exactly when it becomes congruent to one after multiplication by a global unit (principalRayClass_eq_one_iff), so the kernel of A 𝔪 → RayClassGroup 𝔪 is the image of the integer units, and the kernel of (𝓞 K)ˣ → A 𝔪 is the group of units congruent to one. That image is what glues the residue units, the signs and the ordinary class group together inside the ray class group; in general RayClassGroup 𝔪 is not the product of the three.

At the narrow modulus the residue factor is trivial and the formula becomes #(RayClassGroup (narrowModulus K)) * [(𝓞 K)ˣ : (𝓞 K)ˣ⁺] = #(ClassGroup (𝓞 K)) * 2 ^ r₁, with (𝓞 K)ˣ⁺ the totally positive units and r₁ the number of real places.

Main results

• TauCeti.GlobalNumberFields.card_ker_rayClassToClassGroup_mul_index: the order of the kernel of RayClassGroup 𝔪 → ClassGroup (𝓞 K).
• TauCeti.GlobalNumberFields.card_rayClassGroup_mul_index and TauCeti.GlobalNumberFields.card_rayClassGroup: the ray class number formula.
• TauCeti.GlobalNumberFields.card_rayClassGroup_narrowModulus_mul_index: its narrow case.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, (1.10) and (1.11).
• S. Lang, Algebraic Number Theory, Chapter VI, §1, Theorem 1.

The ray class number formula

theorem TauCeti.GlobalNumberFields.card_ker_rayClassToClassGroup_mul_index {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Nat.card ↥(rayClassToClassGroup 𝔪).ker * (unitsCongruenceSubgroup 𝔪).index = Nat.card (NumberField.RingOfIntegers K ⧸ 𝔪.finitePart)ˣ * 2 ^ 𝔪.infinitePart.card

The order of the kernel of RayClassGroup 𝔪 → ClassGroup (𝓞 K). The kernel is the group of residue units and sign patterns modulo the image of the integer units, and that image has order the index of the units congruent to one.

theorem TauCeti.GlobalNumberFields.card_rayClassGroup_mul_index {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Nat.card (RayClassGroup 𝔪) * (unitsCongruenceSubgroup 𝔪).index = Nat.card (ClassGroup (NumberField.RingOfIntegers K)) * (Nat.card (NumberField.RingOfIntegers K ⧸ 𝔪.finitePart)ˣ * 2 ^ 𝔪.infinitePart.card)

The ray class number formula. The order of the ray class group, times the index of the units congruent to one modulo 𝔪, is the class number times the number of residue units modulo the finite part times two for each real place of the infinite part.

theorem TauCeti.GlobalNumberFields.card_rayClassGroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Nat.card (RayClassGroup 𝔪) = Nat.card (ClassGroup (NumberField.RingOfIntegers K)) * (Nat.card (NumberField.RingOfIntegers K ⧸ 𝔪.finitePart)ˣ * 2 ^ 𝔪.infinitePart.card) / (unitsCongruenceSubgroup 𝔪).index

The ray class number formula, solved for the ray class number: h_𝔪 = h · #(𝓞 K ⧸ 𝔪₀)ˣ · 2 ^ #𝔪∞ / [(𝓞 K)ˣ : unitsCongruenceSubgroup 𝔪].

theorem TauCeti.GlobalNumberFields.card_rayClassGroup_narrowModulus_mul_index {K : Type u_1} [Field K] [NumberField K] : Nat.card (RayClassGroup (narrowModulus K)) * NumberField.totallyPositiveIntegerUnits.index = Nat.card (ClassGroup (NumberField.RingOfIntegers K)) * 2 ^ NumberField.InfinitePlace.nrRealPlaces K

The narrow class number formula. At the narrow modulus there are no residue units to count, and the units congruent to one are the totally positive units, so h⁺ · [(𝓞 K)ˣ : (𝓞 K)ˣ⁺] = h · 2 ^ r₁.