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_memandtorsion_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 Kand the principal nonzero ideals ofπ Ktimes the torsion ofK.NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion: the number of principal nonzero ideals inπ Kof normnmultiplied by the order of the torsion ofKis equal to the number offundamentalCone.integralPoint Kof 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.