The volume of the norm-one section of the ray fundamental domain

On the section of norm at most one, the ray fundamental domain of a modulus 𝔪 is the part of the union of the unit translates of Mathlib's fundamentalCone.normLeOne K that carries the signs prescribed by the infinite part of 𝔪. The translates are indexed by the cosets of unitsCongruenceSubgroupSupTorsion 𝔪; they are pairwise disjoint and each has the volume of normLeOne K, and their union is stable under reflection at every real place. Prescribing the sign at the s real places of the infinite part therefore divides the volume of the union by 2 ^ s.

Main results

• TauCeti.GlobalNumberFields.two_pow_mul_volume_rayFundamentalDomain_inter_normLeOne: 2 ^ s times the volume of the norm-one section of rayFundamentalDomain 𝔪 is the index of unitsCongruenceSubgroupSupTorsion 𝔪 times the volume of normLeOne K.
• TauCeti.GlobalNumberFields.measureReal_rayFundamentalDomain_inter_normLeOne: the same volume as an explicit real number, the index times 2 ^ r₁ · π ^ r₂ · Reg_K / 2 ^ s.

References

• S. Lang, Algebraic Number Theory, Chapter VI, §2.

theorem TauCeti.GlobalNumberFields.two_pow_mul_volume_rayFundamentalDomain_inter_normLeOne {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : 2 ^ 𝔪.infinitePart.card * MeasureTheory.volume (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) = ↑(unitsCongruenceSubgroupSupTorsion 𝔪).index * MeasureTheory.volume (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)

The volume of the norm-≤-one section of the ray fundamental domain. With s real places in the infinite part of 𝔪, the section of rayFundamentalDomain 𝔪 of norm at most one has 1 / 2 ^ s of the volume of Mathlib's normLeOne K for each coset of unitsCongruenceSubgroupSupTorsion 𝔪; the statement clears the denominator 2 ^ s. For the trivial modulus both factors are one, and the section has the volume of normLeOne K.

theorem TauCeti.GlobalNumberFields.measureReal_rayFundamentalDomain_inter_normLeOne {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : MeasureTheory.volume.real (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) = ↑(unitsCongruenceSubgroupSupTorsion 𝔪).index * (2 ^ NumberField.InfinitePlace.nrRealPlaces K * Real.pi ^ NumberField.InfinitePlace.nrComplexPlaces K * NumberField.Units.regulator K) / 2 ^ 𝔪.infinitePart.card

The real volume of the norm-≤-one section of the ray fundamental domain. With s real places in the infinite part of 𝔪, the section of rayFundamentalDomain 𝔪 of norm at most one has real volume i · 2 ^ r₁ · π ^ r₂ · Reg_K / 2 ^ s, where i is the index of unitsCongruenceSubgroupSupTorsion 𝔪, r₁ and r₂ are the numbers of real and complex places of K, and Reg_K is its regulator.