Elements of an ideal congruent to one, in the ray fundamental domain #
For a modulus πͺ with finite part πͺβ and a nonzero integral ideal π, this file names the set
of points of the ray fundamental domain of πͺ that are images of elements of π congruent to
one modulo πͺβ, and records two descriptions of it.
Only the finite part appears in the set-builder: the conditions the infinite part imposes are
already carried by the ray fundamental domain, which lies in posRegion πͺ
(mem_posRegion_of_mem_rayFundamentalDomain).
Nothing here asks that π represent a given ray class, nor divides out the congruence roots of
unity acting on the domain; a ray-class ideal count imposes both itself.
Main definitions #
TauCeti.GlobalNumberFields.rayIdealSet: the set described above;TauCeti.GlobalNumberFields.rayIdealSetEquiv: a bijection from it onto the points ofrayIntegerSet πͺwhose underlying algebraic integer lies inπand is congruent to one moduloπͺβ, withrayIdealSetEquiv_applyandrayIdealSetEquiv_symm_applyfor the two directions.
Main results #
TauCeti.GlobalNumberFields.mem_rayIdealSet: its points, unfolded;TauCeti.GlobalNumberFields.rayIdealSet_one: the trivial modulus recovers Mathlib'sNumberField.mixedEmbedding.fundamentalCone.idealSet;TauCeti.GlobalNumberFields.rayIdealSet_eq_inter_vadd: the same set as a translate of the congruence lattice, intersected with the domain;TauCeti.GlobalNumberFields.rayIdealSet_subset_rayIntegerSetandTauCeti.GlobalNumberFields.preimageOfMemRayIntegerSet_mem_and_sub_one_mem_of_mem_rayIdealSet: its points lie inrayIntegerSet πͺ, and the algebraic integer each of them is the image of lies inπand is congruent to one moduloπͺβ.
Implementation notes #
The set takes no base point, while its description as a translate does, which is why
rayIdealSet_eq_inter_vadd takes a witness ΞΎ. Taking ΞΎ = 0 would describe a different set
instead of dispensing with the witness: coe_congruenceLattice_mk0_eq_image
identifies congruenceLattice πͺ (FractionalIdeal.mk0 K π) with the image of π * πͺβ, and an
element of π * πͺβ congruent to one modulo πͺβ forces 1 β πͺβ, so the two agree only for a
trivial finite part.
References #
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean: theidealSetandidealSetEquivlayer there is the model for this file, with the fundamental cone replaced by the ray fundamental domain and the congruence condition added.
The images, inside the ray fundamental domain of πͺ, of the elements of π that are
congruent to one modulo the finite part of πͺ. This is the ray analogue of
NumberField.mixedEmbedding.fundamentalCone.idealSet.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The points of rayIdealSet. A point lies in it exactly when it lies in the ray
fundamental domain and is the image of an element of π congruent to one modulo πͺβ.
The trivial modulus recovers Mathlib's ideal set. Its finite part is the whole ring, so
the congruence condition holds vacuously, and its ray fundamental domain is the fundamental cone
(rayFundamentalDomain_one); what is left is
NumberField.mixedEmbedding.fundamentalCone.idealSet.
rayIdealSet as the domain met with a translate of the congruence lattice. For any
element ΞΎ of π congruent to one modulo πͺβ, the set is the ray fundamental domain
intersected with the translate of congruenceLattice πͺ (FractionalIdeal.mk0 K π) by the image
of ΞΎ.
The lattice on the right does not involve ΞΎ, so a different witness only renames the translate;
and such a ΞΎ exists exactly when π and πͺβ are coprime
(Ideal.isCoprime_iff_exists_mem_and_sub_one_mem). Without one, rayIdealSet πͺ π is empty.
Every point of rayIdealSet πͺ π lies in rayIntegerSet πͺ: it lies in the ray fundamental
domain and is the image of an algebraic integer. Both the membership in π and the congruence
condition are forgotten.
This inclusion is what lets rayIdealSetEquiv land in a subtype of rayIntegerSet πͺ; Mathlib
packages the corresponding map as a definition,
NumberField.mixedEmbedding.fundamentalCone.idealSetMap.
The algebraic integer underlying a point of rayIdealSet πͺ π lies in π and is congruent to
one modulo πͺβ.
With rayIdealSet_subset_rayIntegerSet, this is what makes rayIdealSetEquiv well defined. The
conjunction is stated bundled because it is the predicate defining the set rayIdealSet is built
from, and is verbatim the subtype predicate of that equivalence's codomain.
rayIdealSet as a subtype of the ray integer set. A point of rayIntegerSet πͺ comes
from a point of rayIdealSet πͺ π exactly when the algebraic integer it is the image of lies in
π and is congruent to one modulo πͺβ, so the two carriers are in bijection.
This is the ray analogue of NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv, with the
forward map applied inline rather than named separately.
Equations
- TauCeti.GlobalNumberFields.rayIdealSetEquiv πͺ π = Equiv.ofBijective (fun (x : β(TauCeti.GlobalNumberFields.rayIdealSet πͺ π)) => β¨β¨βx, β―β©, β―β©) β―
Instances For
rayIdealSetEquiv leaves the underlying point of the mixed space unchanged; this is the ray
analogue of NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply.
The inverse of rayIdealSetEquiv also leaves the underlying point of the mixed space
unchanged; this is the ray analogue of
NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply.