Fundamental Cone #
Let K be a number field of signature (rโ, rโ). We define an action of the units (๐ K)หฃ on
the mixed space โ^rโ ร โ^rโ via the mixedEmbedding. The fundamental cone is a cone in the
mixed space that is a fundamental domain for the action of (๐ K)หฃ modulo torsion.
Main definitions and results #
NumberField.mixedEmbedding.unitSMul: the action of(๐ K)หฃon the mixed space defined, foru : (๐ K)หฃ, by multiplication component by component withmixedEmbedding K u.NumberField.mixedEmbedding.fundamentalCone: a cone in the mixed space, i.e. a subset stable by multiplication by a nonzero real number, seesmul_mem_of_mem, that is also a fundamental domain for the action of(๐ K)หฃmodulo torsion, seeexists_unit_smul_memandtorsion_unit_smul_mem_of_mem.NumberField.mixedEmbedding.fundamentalCone.idealSet: forJan integral ideal, the intersection between the fundamental cone and theidealLatticedefined by the image ofJ.NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm: forJan integral ideal andna natural integer, the equivalence between the elements ofidealSet Kof normnand the product of the set of nonzero principal ideals ofKdivisible byJof normnand the torsion ofK.
Tags #
number field, canonical embedding, units, principal ideals
The action of (๐ K)หฃ on the mixed space โ^rโ ร โ^rโ defined, for u : (๐ K)หฃ, by
multiplication component by component with mixedEmbedding K u.
The map from the mixed space to logSpace K defined in such way that: 1) it factors the map
logEmbedding, see logMap_eq_logEmbedding; 2) it is constant on the sets
{c โข x | c โ โ, c โ 0} if norm x โ 0, see logMap_real_smul.
Instances For
Alias of NumberField.mixedEmbedding.logMap_apply_of_norm_eq_one.
The fundamental cone is a cone in the mixed space, i.e. a subset fixed by multiplication by
a nonzero real number, see smul_mem_of_mem, that is also a fundamental domain for the action
of (๐ K)หฃ modulo torsion, see exists_unit_smul_mem and torsion_smul_mem_of_mem.
Instances For
The intersection between the fundamental cone and the integerLattice.
Instances For
If a is in integerSet, then there is a unique algebraic integer in ๐ K such
that mixedEmbedding K x = a.
For a : integerSet K, the unique nonzero algebraic integer x such that its image by
mixedEmbedding is equal to a. Note that we state the fact that x โ 0 by saying that x is
a nonzero divisors since we will use later on the isomorphism
Ideal.associatesNonZeroDivisorsEquivIsPrincipal, see integerSetEquiv.
Instances For
If x : mixedSpace K is nonzero and the image of an algebraic integer, then there exists a
unit such that u โข x โ integerSet K.
The set integerSet K is stable under the action of the torsion.
The action of torsion K on integerSet K.
The mixedEmbedding.norm of a : integerSet K as a natural number, see also
intNorm_coe.
Instances For
The norm intNorm lifts to a function on integerSet K modulo torsion K.
Instances For
The map that sends an element of a : integerSet K to the associates class
of its preimage in (๐ K)โฐ. By quotienting by the kernel of the map, which is equal to the
subgroup of torsion, we get the equivalence integerSetQuotEquivAssociates.
Instances For
The equivalence between integerSet K modulo torsion K and Associates (๐ K)โฐ.
Instances For
The equivalence between integerSet K and the product of the set of nonzero principal
ideals of K and the torsion of K.
Instances For
For an integer n, The equivalence between the elements of integerSet K of norm n
and the product of the set of nonzero principal ideals of K of norm n and the torsion of K.
Instances For
For n positive, the number of principal ideals in ๐ K of norm n multiplied by the order
of the torsion of K is equal to the number of elements in integerSet K of norm n.
The intersection between the fundamental cone and the idealLattice defined by the image of
the integral ideal J.
Instances For
The map that sends a : idealSet to an element of integerSet. This map exists because
J is an integral ideal.
Instances For
The map idealSetMap is actually an equiv between idealSet K J and the elements of
integerSet K whose preimage lies in J.
Instances For
For an integer n, The equivalence between the elements of idealSet K of norm n and
the product of the set of nonzero principal ideals of K divisible by J of norm n and the
torsion of K.
Instances For
For s : โ, the number of principal nonzero ideals in ๐ K divisible par J of norm โค s
multiplied by the order of the torsion of K is equal to the number of elements in idealSet K J
of norm โค s.