Reduction modulo the finite part of a modulus #
For a modulus ๐ช of a number field K, this file constructs the reduction homomorphism from
the elements of Kหฃ that are units at the primes dividing ๐ช.finitePart to the units of
๐ K โงธ ๐ช.finitePart.
An element x in primeToSubgroup ๐ช can be written as x = a / b with the denominator
congruent to one modulo the finite part. The class of a modulo ๐ช.finitePart is independent
of this presentation and defines residueHom ๐ช. Its kernel records exactly the finite-place
conditions in IsCongrOne, and every residue unit is attained: a nonzero integral representative
of a unit class is already prime to the finite part, so it is itself a field unit reducing to that
class.
Main definitions #
TauCeti.GlobalNumberFields.residue,TauCeti.GlobalNumberFields.residueHom: reduction of an element that is a unit at the finite part of๐ชto the residue units modulo that finite part.TauCeti.GlobalNumberFields.finiteUnitsMap: the transition map on residue units when the modulus grows.
Main results #
TauCeti.GlobalNumberFields.exists_algebraMap_eq_mul_of_mem_primeToSubgroup: a prime-to element has a denominator congruent to one modulo the finite part.TauCeti.GlobalNumberFields.residue_eq_one_iff: reduction to one is equivalent to the finite-place conditions inIsCongrOne.TauCeti.GlobalNumberFields.residueHom_eq_one_of_mem_congruenceSubgroup: an element congruent to one maps to one under reduction.TauCeti.GlobalNumberFields.isCongrOne_iff_residueHom_eq_one_of_finitePart_eq: for two moduli with the same finite part, congruence to one modulo one of them is reduction to one modulo the other together with positivity at its real places.TauCeti.GlobalNumberFields.IsCongrOne.exists_sub_one_mem_and_algebraMap_eq_mul: an element congruent to one is a quotient of two algebraic integers congruent to one.TauCeti.GlobalNumberFields.residueHom_surjective: every residue unit modulo the finite part is the reduction of an element ofKหฃthat is a unit at that finite part.TauCeti.GlobalNumberFields.finiteUnitsMap_reflandTauCeti.GlobalNumberFields.finiteUnitsMap_comp_finiteUnitsMap: the transition maps are functorial in finite-part divisibility.TauCeti.GlobalNumberFields.finiteUnitsMap_residueHom: reduction commutes with changing the modulus.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VI, ยง1.
- S. Lang, Algebraic Number Theory, Chapter VI, ยง1.
TauCetiRoadmap/GlobalNumberFields/Suggested.lean(GlobalNumberFields.finiteUnitsMap).
Denominators prime to the finite part #
An element that is a unit at the finite part has a denominator congruent to one. If x is
a unit at every prime dividing ๐ช.finitePart, then x = a / b with a b : ๐ K and
b โก 1 mod ๐ช.finitePart. Such a presentation is what makes the reduction residue of x
modulo the finite part available.
Reduction modulo the finite part #
The reduction of an element that is a unit at the finite part of ๐ช: the class modulo
๐ช.finitePart of a numerator in any presentation x = a / b with b โก 1 mod ๐ช.finitePart. The
class does not depend on the presentation (residue_eq).
Equations
- TauCeti.GlobalNumberFields.residue ๐ช x = (Ideal.Quotient.mk ๐ช.finitePart) โฏ.choose
Instances For
The reduction is computed by any presentation with denominator congruent to one.
Reduction modulo the finite part of a modulus, as a homomorphism from the elements that are
units at the primes dividing ๐ช.finitePart to the residue units. This is the carrier of the
residue-unit factor in the ray class number formula.
Equations
- TauCeti.GlobalNumberFields.residueHom ๐ช = { toFun := TauCeti.GlobalNumberFields.residue ๐ช, map_one' := โฏ, map_mul' := โฏ }.toHomUnits
Instances For
Reduction to one is exactly congruence to one at the primes dividing the finite part. The
reduction carries the finite conditions of IsCongrOne and nothing else, so the archimedean
conditions are independent of it and have to be supplied separately.
An element reducing to one and positive at the real places of ๐ช is congruent to one.
Congruence to one sees the finite part only through the reduction. For two moduli with the
same finite part, an element that is a unit at that finite part is congruent to one modulo ๐ช
exactly when it reduces to one modulo ๐ซ and is positive at the real places of ๐ช. This is how
the finite conditions of one modulus are read off the reduction attached to another.
An element congruent to one modulo ๐ช reduces to one: the congruence subgroup lies in the
kernel of residueHom ๐ช.
An element congruent to one is a quotient of integers congruent to one. If
IsCongrOne ๐ช x, then x = a / b with a b : ๐ K both congruent to one modulo
๐ช.finitePart.
Surjectivity of the reduction #
Every residue unit modulo the finite part is the reduction of a field unit prime to it.
This is what makes the residue-unit factor of the ray class number formula the whole of
(๐ K โงธ ๐ช.finitePart)หฃ rather than the image of the algebraic integers prime to ๐ช.
A nonzero integral representative of the class does the job by itself: being a unit residue it
avoids every prime dividing the finite part, so its image in Kหฃ lies in primeToSubgroup ๐ช and
reduces back to the class.
Transition maps for residue units #
The reduction map on residue units from a larger finite part to a divisor of it. It is induced by the canonical quotient map between the two ideal quotients; in particular, it does not choose a ring-level inverse.
Equations
Instances For
The value of the transition map is the image under the canonical quotient map of the underlying residue-unit value.
Changing the finite part along reflexivity gives the identity map.
Transition maps compose along a chain of finite-part divisibility.
Reduction of a prime-to element commutes with passing to a modulus with smaller finite part.