The residue-and-sign presentation of the congruence quotient #
Let ๐ช be a modulus of a number field K. Congruence to one modulo ๐ช is two independent
conditions on an element of primeToSubgroup ๐ช: reduction to one in (๐ K โงธ ๐ช.finitePart)หฃ, and
positivity at each real place selected by ๐ช.infinitePart. This file packages the two conditions
into one homomorphism
residueSignHom ๐ช :
primeToSubgroup ๐ช โ* (๐ K โงธ ๐ช.finitePart)หฃ ร (๐ช.infinitePart โ โคหฃ)
and proves that it is surjective with kernel exactly congruenceSubgroup ๐ช. The resulting
isomorphism residueSignEquiv computes the relative index
(congruenceSubgroup ๐ช).relIndex (primeToSubgroup ๐ช)
= Nat.card (๐ K โงธ ๐ช.finitePart)หฃ * 2 ^ ๐ช.infinitePart.card,
which is the residue-and-sign factor of the ray class number formula โ the factor before the
image of the global units is divided out โ and strengthens the bare finiteness recorded by
congruenceSubgroup_finiteIndex.
Surjectivity is the arithmetic content and is not a chinese-remainder statement: the residue
class and the signs have to be realized by one and the same element of Kหฃ, so the proof runs
through weak approximation at the mixed set of places consisting of the primes dividing
๐ช.finitePart together with all real places
(exists_fieldUnit_valuation_sub_lt_and_signHom_eq). An approximation to a chosen integral
representative of the residue class, closely enough that v.valuation K of their difference stays
below exp (-๐ช.exponent v) at each prime of the support, has the same reduction as that
representative: the quotient of the two then differs from one by at most that much, which is the
congruence condition recorded by residue_eq_one_iff.
The global units of K are nowhere quotiented out here. Their image in this quotient is the
obstruction that glues the residue-unit and sign factors to the ordinary class group inside the
ray class group, and it is why the ray class group is not the product of the three.
Main definitions #
TauCeti.GlobalNumberFields.residueSignHom: the reduction-and-signs homomorphism.TauCeti.GlobalNumberFields.residueSignEquiv: the induced isomorphism from the congruence quotient.
Main results #
TauCeti.GlobalNumberFields.residueSignHom_eq_one_iffandTauCeti.GlobalNumberFields.ker_residueSignHom: the kernel is the congruence subgroup.TauCeti.GlobalNumberFields.residueSignHom_surjective: every residue unit and sign pattern is realized simultaneously, together with its archimedean halfTauCeti.GlobalNumberFields.modulusSignHom_comp_primeToSubgroup_surjective.TauCeti.GlobalNumberFields.relIndex_congruenceSubgroup: the exact relative index.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VI, ยง1.
- S. Lang, Algebraic Number Theory, Chapter VI, ยง1.
The signs prescribed by a modulus #
The signs of a field unit at the real places selected by a modulus. This is signHom
restricted to ๐ช.infinitePart; the real places outside the modulus are unconstrained and are
forgotten.
Equations
- TauCeti.GlobalNumberFields.modulusSignHom ๐ช = { toFun := fun (x : Kหฃ) (w : โฅ๐ช.infinitePart) => TauCeti.GlobalNumberFields.signHom x โw, map_one' := โฏ, map_mul' := โฏ }
Instances For
The prescribed signs are trivial exactly at an element positive on the infinite part.
The reduction-and-signs homomorphism #
The residue-and-sign presentation of a modulus. An element of Kหฃ that is a unit at every
prime dividing ๐ช.finitePart has both a reduction in (๐ K โงธ ๐ช.finitePart)หฃ and a sign at each
real place selected by ๐ช; congruence to one modulo ๐ช is exactly the vanishing of both.
The two factors are the finite and the archimedean halves of the ray class number formula.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Congruence to one is exactly trivial reduction together with trivial signs.
The kernel of the residue-and-sign presentation is the congruence subgroup.
Surjectivity #
The residue-and-sign presentation is surjective. Every residue unit modulo the finite part
and every pattern of signs at the real places of the modulus are realized simultaneously by one
element of Kหฃ that is a unit at the finite part.
The two prescriptions are independent: no compatibility between a residue class and a sign pattern is required, which is what makes the congruence quotient a direct product.
Every pattern of signs at the real places of a modulus is realized by a field unit prime to
its finite part. This is the archimedean half of residueSignHom_surjective, the finite half
being residueHom_surjective. Unlike signHom_surjective, the realizing element is also
constrained at the finite places: it is a unit at every prime dividing ๐ช.finitePart.
The congruence quotient and its order #
The congruence quotient of a modulus is the residue units times the prescribed signs. This
is the presentation of primeToSubgroup ๐ช โงธ congruenceSubgroup ๐ช that the ray class number formula
is read off, and it is where the finite and the archimedean data of a modulus become independent
coordinates.
Equations
Instances For
The exact relative index of the congruence subgroup. The elements that are units at the
finite part of ๐ช, modulo those congruent to one, are counted by the residue units modulo the
finite part times two for each real place of the infinite part.
This refines the finiteness statement congruenceSubgroup_finiteIndex to an equality. It is the
residue-and-sign factor entering the ray class number formula, which multiplies the class number
only after the image of the global units in this quotient is divided out; that image is the
obstruction described in the module docstring.