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.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.
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.
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.