The ray class group of a modulus is finite

Let 𝔪 be a modulus of a number field K. This file proves that RayClassGroup 𝔪 is finite.

The argument runs along the two steps of the ray class exact sequence. The transition map to the ordinary class group has finite image because the class group of a number field is finite, and its kernel is the group of principal ideals prime to 𝔪, modulo the ray. That kernel is a quotient of primeToSubgroup 𝔪 ⧸ congruenceSubgroup 𝔪, so everything rests on

TauCeti.GlobalNumberFields.congruenceSubgroup_finiteIndex: the elements congruent to one modulo 𝔪 have finite index among the elements that are units at the primes dividing the finite part.

That relative finite-index statement uses the reduction homomorphism residueHom 𝔪 constructed in TauCeti.NumberTheory.NumberField.Global.RayClass.Residue: an element that reduces to one and is totally positive is congruent to one modulo 𝔪.

The unit-group form unitsCongruenceSubgroup_finiteIndex — the units of 𝓞 K congruent to one modulo 𝔪 have finite index in (𝓞 K)ˣ — is the same statement pulled back along (𝓞 K)ˣ → Kˣ; it is the unit correction appearing in the ray class number formula, and the finite-index input to the geometry-of-numbers count of ideals in a ray class.

Main results

• TauCeti.GlobalNumberFields.congruenceSubgroup_finiteIndex and TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_finiteIndex: the two finite-index statements.
• TauCeti.GlobalNumberFields.finiteIndex_ray: the ray has finite index in the group of invertible fractional ideals prime to the modulus.
• TauCeti.GlobalNumberFields.finite_rayClassGroup: the ray class group of a modulus is finite.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• S. Lang, Algebraic Number Theory, Chapter VI, §1.

Finiteness of the index

instance TauCeti.GlobalNumberFields.congruenceSubgroup_finiteIndex {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : ((congruenceSubgroup 𝔪).subgroupOf (primeToSubgroup 𝔪)).FiniteIndex

The elements congruent to one modulo 𝔪 have finite index among the elements that are units at the primes dividing the finite part. This relative finite index is the arithmetic content behind the finiteness of the ray class group.

instance TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_finiteIndex {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (unitsCongruenceSubgroup 𝔪).FiniteIndex

The units congruent to one modulo 𝔪 have finite index in (𝓞 K)ˣ. This is the unit correction in the ray class number formula, and the input that makes the implied constants of the ray-class ideal count uniform in the class.

Finiteness of the ray class group

instance TauCeti.GlobalNumberFields.finiteIndex_ray {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (ray 𝔪).FiniteIndex

The ray has finite index in the invertible fractional ideals prime to 𝔪. This index is the ray class number, and its finiteness is what makes RayClassGroup 𝔪 a finite group.

instance TauCeti.GlobalNumberFields.finite_rayClassGroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Finite (RayClassGroup 𝔪)

The ray class group of a modulus is finite. This is the finiteness underlying the ray class number, and what makes a ray class character a character of a finite abelian group.