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, ie. 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_mem
andtorsion_unit_smul_mem_of_mem
.NumberField.mixedEmbedding.fundamentalCone.idealSet
: forJ
an integral ideal, the intersection between the fundamental cone and theidealLattice
defined by the image ofJ
.NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm
: forJ
an integral ideal andn
a natural integer, the equivalence between the elements ofidealSet K
of normn
and the product of the set of nonzero principal ideals ofK
divisible byJ
of normn
and 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
.
Equations
- One or more equations did not get rendered due to their size.
The map from the mixed space to {w : InfinitePlace K // w โ wโ} โ โ
(with wโ
the fixed
place from the proof of Dirichlet Unit Theorem) 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
.
Equations
- NumberField.mixedEmbedding.logMap x w = โ(โw).mult * (Real.log ((NumberField.mixedEmbedding.normAtPlace โw) x) - Real.log (NumberField.mixedEmbedding.norm x) * (โ(Module.finrank โ K))โปยน)
Instances For
The fundamental cone is a cone in the mixed space, ie. 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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The intersection between the fundamental cone and the integerLattice
.
Equations
Instances For
If a
is in integerSet
, then there is a unique algebraic integer in ๐ K
such
that mixedEmbedding K x = a
.
Alias of NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet
.
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
.
Equations
- NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a = โจโฏ.choose, โฏโฉ
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
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet = MulAction.mk โฏ โฏ
The mixedEmbedding.norm
of a : integerSet K
as a natural number, see also
intNorm_coe
.
Equations
Instances For
The norm intNorm
lifts to a function on integerSet K
modulo torsion K
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
Instances For
The equivalence between integerSet K
modulo torsion K
and Associates (๐ K)โฐ
.
Equations
Instances For
The equivalence between integerSet K
and the product of the set of nonzero principal
ideals of K
and the torsion of K
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
Instances For
The map that sends a : idealSet
to an element of integerSet
. This map exists because
J
is an integral ideal.
Equations
- NumberField.mixedEmbedding.fundamentalCone.idealSetMap K J โจa, haโฉ = โจa, โฏโฉ
Instances For
The map idealSetMap
is actually an equiv between idealSet K J
and the elements of
integerSet K
whose preimage lies in J
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.