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.integralPoint
: the subset of elements of the fundamental cone that are images of algebraic integers ofK
.NumberField.mixedEmbedding.fundamentalCone.integralPointEquiv
: the equivalence betweenfundamentalCone.integralPoint K
and the principal nonzero ideals ofπ K
times the torsion ofK
.NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion
: the number of principal nonzero ideals inπ K
of normn
multiplied by the order of the torsion ofK
is equal to the number offundamentalCone.integralPoint K
of normn
.
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 set of images by mixedEmbedding
of algebraic integers of K
contained in the
fundamental cone.
Equations
Instances For
If a
is an integral point, then there is a unique algebraic integer in π K
such
that mixedEmbedding K x = a
.
For a : fundamentalCone 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 integralPointEquiv
.
Equations
- NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint 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 β integralPoint K
.
The set integralPoint K
is stable under the action of the torsion.
The action of torsion K
on integralPoint K
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegralPoint = MulAction.mk β― β―
The mixedEmbedding.norm
of a : integralPoint K
as a natural number, see also
intNorm_coe
.
Equations
Instances For
The norm intNorm
lifts to a function on integralPoint 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 : integralPoint 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 integralPointQuotEquivAssociates
.
Equations
Instances For
The equivalence between integralPoint K
modulo torsion K
and Associates (π K)β°
.
Equations
Instances For
The equivalence between integralPoint 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 integralPoint 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 integralPoint K
of norm n
.
For s : β
, the number of principal nonzero ideals in π K
of norm β€ s
multiplied by the
order of the torsion of K
is equal to the number of integralPoint K
of norm β€ s
.