The ray class group of a modulus #
Let ๐ช be a modulus of a number field K. The ray of ๐ช is the subgroup of principal
fractional ideals generated by the elements of Kหฃ congruent to one modulo ๐ช, and the ray
class group RayClassGroup ๐ช is the quotient of the group idealsPrimeTo ๐ช of invertible
fractional ideals prime to the finite part of ๐ช by that ray.
The ray really is a subgroup of idealsPrimeTo ๐ช, and not merely of all invertible fractional
ideals: an element congruent to one is a unit at every prime dividing the finite part of ๐ช
(IsCongrOne.valuation_eq_one), so its principal ideal has vanishing multiplicity there. That is
the content of TauCeti.GlobalNumberFields.rayHom, from which the ray is obtained as a range.
The class of an ideal is defined on the monoid integralIdealsPrimeTo ๐ช of nonzero integral ideals
prime to the finite part, never on all of Ideal (๐ K): an ideal sharing a prime with the finite
part has no ray class, and carrying the coprimality proof in the argument makes multiplicativity
literally map_mul.
For the trivial modulus the congruence condition is empty, and the ray class group is the ordinary
class group (oneEquivClassGroup).
Main definitions #
TauCeti.GlobalNumberFields.principalIdealPrimeTo: the principal fractional ideals whose generators are units at the finite part.TauCeti.GlobalNumberFields.rayHom,TauCeti.GlobalNumberFields.ray: the principal ideals of the elements congruent to one, and the subgroup they form.TauCeti.GlobalNumberFields.idealsPrimeToClassGroup: the ordinary ideal class of an invertible fractional ideal prime to a modulus.TauCeti.GlobalNumberFields.RayClassGroup: the quotient ofidealsPrimeTo ๐ชby the ray, withTauCeti.GlobalNumberFields.rayClassMkand the universal propertyTauCeti.GlobalNumberFields.rayClassLift.TauCeti.GlobalNumberFields.idealClass: the ray class of an integral ideal prime to๐ช, as a monoid homomorphism out ofintegralIdealsPrimeTo ๐ช.TauCeti.GlobalNumberFields.classMap: the transition map, running from the ray class group of a larger modulus to that of a divisor of it.
Main results #
TauCeti.GlobalNumberFields.toPrincipalIdeal_mem_idealsPrimeTo_iff: a principal fractional ideal is prime to the modulus exactly when its generator is a unit at every prime dividing the finite part, withTauCeti.GlobalNumberFields.IsCongrOne.toPrincipalIdeal_mem_idealsPrimeTothe consequence for an element congruent to one.TauCeti.GlobalNumberFields.idealsPrimeTo_eq_top: every invertible fractional ideal is prime to a modulus whose support is empty, soTauCeti.GlobalNumberFields.idealsPrimeToEquividentifies the two carriers there.TauCeti.GlobalNumberFields.idealClass_apply: the ray class of an integral ideal is the ray class of the fractional ideal it generates.TauCeti.GlobalNumberFields.idealClass_mul: taking the ray class of an integral ideal respects multiplication.TauCeti.GlobalNumberFields.idealClass_eq_one_iff: an ideal has trivial ray class exactly when it is generated, as a fractional ideal, by an element ofKหฃcongruent to one modulo๐ช.TauCeti.GlobalNumberFields.classMap_comp_classMapandTauCeti.GlobalNumberFields.classMap_comp_idealClass: the transition maps compose along a tower of moduli, and carry the class of an integral ideal to the class of the same ideal. Both are equalities of homomorphisms, with the pointwise formsclassMap_classMapandclassMap_idealClassderived from them. The transition map from a modulus to itself is the identity (TauCeti.GlobalNumberFields.classMap_refl).TauCeti.GlobalNumberFields.oneEquivClassGroup: at the trivial modulus the ray class group is the class group of๐ K, carrying a ray class to the class of the same fractional ideal (TauCeti.GlobalNumberFields.oneEquivClassGroup_rayClassMk).
References #
- J. Neukirch, Algebraic Number Theory, Chapter VI, ยง1.
- S. Lang, Algebraic Number Theory, Chapter VI, ยง1.
A principal fractional ideal is prime to the modulus exactly when its generator is a unit at every prime dividing the finite part.
The principal ideal of an element congruent to one is prime to the modulus. At a prime dividing the finite part such an element is a unit, so the multiplicity of its principal ideal vanishes there.
The principal fractional ideal of an element that is a unit at every prime dividing the
finite part of m, viewed as an element of idealsPrimeTo m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
principalIdealPrimeTo does not change the underlying principal fractional ideal.
The homomorphism sending an element of Kหฃ congruent to one modulo ๐ช to its principal
fractional ideal, viewed inside the ideals prime to ๐ช.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ray of a modulus: the subgroup of idealsPrimeTo ๐ช consisting of the principal
fractional ideals of the elements of Kหฃ congruent to one modulo ๐ช.
Equations
Instances For
The ordinary ideal class of an invertible fractional ideal prime to a modulus. This is the
canonical map from idealsPrimeTo ๐ช to the ordinary class group; it descends to the right-hand
transition in the ray-class exact sequence.
Equations
Instances For
The principal fractional ideals prime to a modulus are exactly the kernel of the map to the ordinary ideal class group.
The ray class group of a modulus: the invertible fractional ideals prime to the finite part
of ๐ช, modulo the principal ideals of the elements congruent to one modulo ๐ช.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- TauCeti.GlobalNumberFields.instInhabitedRayClassGroup ๐ช = { default := 1 }
The ray class of an invertible fractional ideal prime to the modulus.
Equations
Instances For
The universal property of the ray class group. A homomorphism out of the invertible
fractional ideals prime to ๐ช which is trivial on the ray factors, uniquely, through the ray
class group.
Equations
Instances For
The factorization through the ray class group is unique: a homomorphism out of
RayClassGroup ๐ช is determined by its composition with rayClassMk.
The kernel of rayClassLift ฯ h is the image under rayClassMk ๐ช of ฯ.ker. This exposes
QuotientGroup.ker_lift through the module-opaque RayClassGroup representation.
The ray class of an integral ideal prime to the modulus. The domain is the monoid of
nonzero integral ideals prime to the finite part of ๐ช, never Ideal (๐ K): an ideal sharing a
prime with the finite part, or the zero ideal, has no ray class, and a version totalized over
arbitrary ideals would hand back a junk class there. Carrying the coprimality proof in the
argument also makes multiplicativity map_mul rather than a law with side conditions.
Equations
Instances For
The ray class of a product is the product of the ray classes.
The ray class of an integral ideal is the ray class of the fractional ideal it generates.
The intrinsic triviality criterion for a ray class. An integral ideal prime to ๐ช has
trivial ray class exactly when it is generated as a fractional ideal by an element of Kหฃ that
is congruent to one modulo ๐ช; the congruence already carries both the finite conditions and the
positivity at the real places of ๐ช.
The transition map between ray class groups #
The transition map between ray class groups. For ๐ช โฃ ๐ซ it runs from the larger modulus
to the smaller one: an invertible fractional ideal prime to ๐ซ is prime to ๐ช, and an element
congruent to one modulo ๐ซ is congruent to one modulo ๐ช, so the ray of ๐ซ lands in the ray
of ๐ช.
Equations
Instances For
The transition map at a modulus and itself is the identity, as an equality of homomorphisms.
The transition map at a modulus and itself is the identity.
The transition maps compose along a tower of moduli, as an equality of homomorphisms.
The transition maps compose along a tower of moduli.
The ray class of an integral ideal is compatible with the transition maps, as an equality
of homomorphisms out of integralIdealsPrimeTo ๐ซ.
The ray class of an integral ideal is compatible with the transition maps.
Moduli with unit finite part #
Every invertible fractional ideal is prime to a modulus with empty support: no prime divides the finite part, so no multiplicity is required to vanish. The trivial modulus and the narrow modulus are the two moduli of this kind.
The ideals prime to a modulus with empty support are all the invertible fractional ideals.
Equations
Instances For
Under the identification with all invertible fractional ideals, a fractional ideal prime to a modulus with empty support keeps its underlying ideal.
The trivial modulus #
The ray of the trivial modulus is the group of all principal fractional ideals.
At the trivial modulus the ray class group is the ordinary class group. This is a named equivalence, not a definitional equality: the ray class group is a quotient of the ideals prime to the empty set of primes, and the class group is a quotient of all invertible fractional ideals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence at the trivial modulus carries a ray class to the class of the same fractional ideal.