The ray class exact sequence #
For a modulus m of a number field K, forgetting its congruence and sign conditions sends a ray
class to an ordinary ideal class. This file constructs the full exact sequence
1 โ unitsCongruenceSubgroup m โ (๐ K)หฃ โ A m โ RayClassGroup m โ ClassGroup (๐ K) โ 1,
where A m = (๐ K โงธ m.finitePart)หฃ ร (m.infinitePart โ โคหฃ) records residues and prescribed
signs. It also retains the useful coarser exact tail
primeToSubgroup m โ RayClassGroup m โ ClassGroup (๐ K) โ 1.
In the coarser tail, the first map sends an element of Kหฃ that is a unit at the finite part to
the ray class of its principal ideal. The second map is surjective, and its kernel is exactly the
range of the first. Surjectivity of the transition maps follows by weak approximation, and
surjectivity onto the ordinary class group follows by transition to the trivial modulus.
The kernel of A m โ RayClassGroup m is the image of the integer units, while the kernel of the
map from integer units to A m is unitsCongruenceSubgroup m. The resulting exact sequence is
the input to the ray class number formula.
Main definitions #
TauCeti.GlobalNumberFields.principalRayClass: the ray class of a principal fractional ideal whose generator is a unit at the finite part.TauCeti.GlobalNumberFields.rayClassToClassGroup: the ordinary ideal class underlying a ray class.TauCeti.GlobalNumberFields.unitsResidueSignHom: the residues and signs of the integer units.TauCeti.GlobalNumberFields.residueSignRayClass: the principal ray class of a residue unit and sign pattern.
Main results #
TauCeti.GlobalNumberFields.rayClassToClassGroup_surjective: every ordinary ideal class lifts to a ray class.TauCeti.GlobalNumberFields.ker_rayClassToClassGroup: the kernel consists exactly of ray classes of principal ideals generated by elements inprimeToSubgroup m.TauCeti.GlobalNumberFields.mulExact_principalRayClass_rayClassToClassGroup: the corresponding multiplicative exactness statement.TauCeti.GlobalNumberFields.classMap_surjective: every transition between ray class groups is surjective.TauCeti.GlobalNumberFields.ker_unitsResidueSignHom,TauCeti.GlobalNumberFields.ker_residueSignRayClassandTauCeti.GlobalNumberFields.range_residueSignRayClass: the three nontrivial exactness statements in the full sequence.TauCeti.GlobalNumberFields.mulExact_unitsCongruenceSubgroup_unitsResidueSignHom,TauCeti.GlobalNumberFields.mulExact_unitsResidueSignHom_residueSignRayClassandTauCeti.GlobalNumberFields.mulExact_residueSignRayClass_rayClassToClassGroup: their multiplicative exactness forms.TauCeti.GlobalNumberFields.classMap_eq_one_iff_of_finitePart_eq: the kernel of a transition map between moduli with the same finite part consists of the classes of sign patterns trivial at the real places of the smaller modulus.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VI, ยง1.
- S. Lang, Algebraic Number Theory, Chapter VI, ยง1.
The ray class of the principal ideal generated by an element that is a unit at every prime
dividing the finite part of m.
Equations
Instances For
The principal ray class is represented by the corresponding principal fractional ideal.
A generator congruent to one modulo m has trivial principal ray class.
The map from a ray class to its underlying ordinary ideal class.
Equations
Instances For
The ordinary class underlying the ray class of a fractional ideal is its usual ideal class.
Forgetting the modulus agrees with transition to the trivial modulus followed by the canonical identification of its ray class group with the ordinary class group.
Transition from a larger modulus to any divisor is surjective.
Every ordinary ideal class is represented by a ray class.
The ray classes with trivial ordinary ideal class are exactly the principal ray classes. This
is exactness at RayClassGroup m in the ray-class exact sequence.
The principal-ray-class map followed by forgetting the modulus is exact.
The residue-and-sign presentation of the exact sequence #
A principal ray class is trivial exactly when a unit multiple of the generator is congruent
to one. Two generators of the same principal fractional ideal differ by a unit of ๐ K, so the
ray only sees an element of primeToSubgroup ๐ช up to the integer units.
The residues and signs of the integer units. This is the left-hand map of the ray class exact sequence; its image is the obstruction that is divided out of the residue units and signs before they embed into the ray class group.
Equations
Instances For
Exactness at the integer units: a unit has trivial residue and trivial signs exactly when
it is congruent to one modulo ๐ช.
Exactness at the integer units, as a Function.MulExact statement.
The principal ray class of a residue unit and a sign pattern. The principal ray class of
an element prime to ๐ช depends only on its residue modulo the finite part and its signs at the
real places of ๐ช, and every residue unit and sign pattern arises (residueSignEquiv); this is
the induced homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class attached to the residue and signs of an element is its principal ray class.
residueSignRayClass ๐ช is the factorization of principalRayClass ๐ช through the surjection
residueSignHom ๐ช.
Exactness at the residue units and signs: a residue unit and sign pattern has trivial ray class exactly when it is the residue and sign pattern of an integer unit.
Exactness at the ray class group: the ray classes with trivial ordinary ideal class are exactly the classes of residue units and sign patterns.
Exactness at the residue units and signs, as a Function.MulExact statement.
Exactness at the ray class group, as a Function.MulExact statement.
The residue and signs of the unit -1: residue -1 and sign -1 at every real place of the
modulus.
Transition maps that only forget real places #
The kernel of a transition map between moduli with the same finite part consists of sign
classes. When ๐ช โฃ ๐ซ have the same finite part, a ray class of ๐ซ is killed by
classMap : Cl_๐ซ โ Cl_๐ช exactly when it is the class residueSignRayClass ๐ซ (1, s) of the trivial
residue together with a pattern of signs s that is trivial at the real places of ๐ช.