Documentation

TauCeti.NumberTheory.NumberField.Global.Counting.RayFundamentalDomain.Basic

Fundamental domains for congruence subgroups of number-field units #

A unit congruent to one modulo a modulus π”ͺ is constrained in two ways: it lies in a finite-index subgroup of (π“ž K)Λ£, and it is positive at every real place selected by the infinite part of π”ͺ. The set rayFundamentalDomain π”ͺ built here is cut out by the matching two conditions on the mixed space: the sign conditions prescribed by π”ͺ, recorded by posRegion π”ͺ, together with membership in one of finitely many translates of Mathlib's NumberField.mixedEmbedding.fundamentalCone.

The translates are indexed by the cosets of unitsCongruenceSubgroupSupTorsion π”ͺ, the congruence units joined with the roots of unity, and not by the cosets of the congruence units alone. Mathlib's cone is stable under the torsion, so translating it by two units differing by a root of unity gives the same set; only with the larger index group do the translates meet each congruence-unit orbit the same number of times, independently of the point and of the arbitrary choice of representatives.

Consequently the domain is fundamental modulo torsion, in exactly the sense in which Mathlib's cone is fundamental for the full unit group. It is measurable and stable under positive real scalars β€” negative ones may violate nonempty prescribed sign conditions β€” every point of posRegion π”ͺ of nonzero mixed norm is carried into it by a unit congruent to one modulo π”ͺ, and a congruence unit carries a point of the domain back into the domain exactly when that unit is a root of unity. So the domain meets each congruence-unit orbit of nonzero mixed norm inside posRegion π”ͺ in one point, modulo the congruence units that are roots of unity. For the trivial modulus, whose infinite part is empty and whose congruence units are all of (π“ž K)Λ£, the domain is Mathlib's fundamental cone.

Boundary regularity β€” Lipschitz parametrizability of the frontier of the norm-one section β€” is developed separately; it is what upgrades the orbit description below to a count of the algebraic integers in a fixed ray class.

Main definitions #

Main results #

References #

The finite-union construction is the standard ray-class refinement of the fundamental cone; see S. Lang, Algebraic Number Theory, Chapter VI, Section 2.

smul_rayFundamentalDomain_inter_normLeOne is adapted from github.com/CBirkbeck/aintlib @ 2622c61d2502159c62865a1b59fc1de473519113 (Apache-2.0), projects/Chebotarev/CebotarevDensity/ForMathlib/IdealCongruenceCount.lean, where cone_normLe_eq_smul_normLeOne states it privately for the fundamental cone and the trivial modulus under the stronger hypothesis 1 ≀ t.

The congruence units and the roots of unity #

source
def TauCeti.GlobalNumberFields.unitsCongruenceSubgroupSupTorsion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
Subgroup (NumberField.RingOfIntegers K)Λ£

The subgroup of (π“ž K)Λ£ generated by the units congruent to one modulo π”ͺ and the roots of unity.

Mathlib's fundamental cone is a fundamental domain for the unit action only modulo torsion, so this join, rather than unitsCongruenceSubgroup π”ͺ itself, is the subgroup whose cosets index the translates of the cone below.

Equations
Instances For
    source
    theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroupSupTorsion_def {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
    unitsCongruenceSubgroupSupTorsion π”ͺ = unitsCongruenceSubgroup π”ͺ βŠ” NumberField.Units.torsion K

    unitsCongruenceSubgroupSupTorsion π”ͺ is the join of unitsCongruenceSubgroup π”ͺ and the roots of unity.

    source
    theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroupSupTorsion_le_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {H : Subgroup (NumberField.RingOfIntegers K)Λ£} :
    unitsCongruenceSubgroupSupTorsion π”ͺ ≀ H ↔ unitsCongruenceSubgroup π”ͺ ≀ H ∧ NumberField.Units.torsion K ≀ H

    The universal property of the join: a subgroup contains unitsCongruenceSubgroupSupTorsion π”ͺ if and only if it contains the units congruent to one modulo π”ͺ and the roots of unity.

    source
    theorem TauCeti.GlobalNumberFields.torsion_le_unitsCongruenceSubgroupSupTorsion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
    NumberField.Units.torsion K ≀ unitsCongruenceSubgroupSupTorsion π”ͺ

    The roots of unity lie in unitsCongruenceSubgroupSupTorsion π”ͺ.

    source
    theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_le_unitsCongruenceSubgroupSupTorsion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
    unitsCongruenceSubgroup π”ͺ ≀ unitsCongruenceSubgroupSupTorsion π”ͺ

    The units congruent to one modulo π”ͺ lie in unitsCongruenceSubgroupSupTorsion π”ͺ.

    source
    theorem TauCeti.GlobalNumberFields.mem_unitsCongruenceSubgroupSupTorsion {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {u : (NumberField.RingOfIntegers K)Λ£} :
    u ∈ unitsCongruenceSubgroupSupTorsion π”ͺ ↔ βˆƒ v ∈ unitsCongruenceSubgroup π”ͺ, βˆƒ ΞΆ ∈ NumberField.Units.torsion K, v * ΞΆ = u

    A unit lies in unitsCongruenceSubgroupSupTorsion π”ͺ exactly when it is the product of a unit congruent to one modulo π”ͺ and a root of unity.

    source
    instance TauCeti.GlobalNumberFields.unitsCongruenceSubgroupSupTorsion_finiteIndex {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
    (unitsCongruenceSubgroupSupTorsion π”ͺ).FiniteIndex
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroupSupTorsion_one {K : Type u_1} [Field K] [NumberField K] :
    unitsCongruenceSubgroupSupTorsion (Modulus.one K) = ⊀

    For the trivial modulus the congruence units are already all of (π“ž K)Λ£, so adjoining the roots of unity changes nothing and there is a single coset.

    The sign conditions prescribed by the infinite part #

    source
    def TauCeti.GlobalNumberFields.posRegion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
    Set (NumberField.mixedEmbedding.mixedSpace K)

    The positivity region of a modulus: the points of the mixed space whose coordinate at every real place in π”ͺ.infinitePart is positive.

    These are the sign conditions defining congruence to one modulo π”ͺ: the mixed embedding of an element congruent to one lies in this region, and the region is stable under the action of a unit congruent to one.

    Equations
    Instances For
      source
      theorem TauCeti.GlobalNumberFields.posRegion_def {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      posRegion π”ͺ = {x : NumberField.mixedEmbedding.mixedSpace K | βˆ€ w ∈ π”ͺ.infinitePart, 0 < x.1 w}

      posRegion π”ͺ is the set of points positive at every real place of the infinite part of π”ͺ.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.mem_posRegion {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} :
      x ∈ posRegion π”ͺ ↔ βˆ€ w ∈ π”ͺ.infinitePart, 0 < x.1 w
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.posRegion_one {K : Type u_1} [Field K] [NumberField K] :
      posRegion (Modulus.one K) = Set.univ

      The trivial modulus prescribes no sign at all: its infinite part is empty.

      source
      theorem TauCeti.GlobalNumberFields.isOpen_posRegion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      IsOpen (posRegion π”ͺ)

      The positivity region is open: it is a finite intersection of open half spaces.

      source
      theorem TauCeti.GlobalNumberFields.measurableSet_posRegion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      MeasurableSet (posRegion π”ͺ)
      source
      theorem TauCeti.GlobalNumberFields.smul_mem_posRegion {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ posRegion π”ͺ) {c : ℝ} (hc : 0 < c) :
      c β€’ x ∈ posRegion π”ͺ

      The positivity region is stable under multiplication by a positive real scalar.

      source
      theorem TauCeti.GlobalNumberFields.unitSMul_mem_posRegion {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ posRegion π”ͺ) {u : (NumberField.RingOfIntegers K)Λ£} (hu : u ∈ unitsCongruenceSubgroup π”ͺ) :
      u β€’ x ∈ posRegion π”ͺ

      The positivity region is stable under the action of a unit congruent to one modulo π”ͺ: such a unit is positive at every real place prescribed by π”ͺ.

      source
      theorem TauCeti.GlobalNumberFields.unitSMul_mem_posRegion_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} {u : (NumberField.RingOfIntegers K)Λ£} (hu : u ∈ unitsCongruenceSubgroup π”ͺ) :
      u β€’ x ∈ posRegion π”ͺ ↔ x ∈ posRegion π”ͺ

      The positivity region is invariant under the action of a unit congruent to one modulo π”ͺ.

      The fundamental domain #

      source
      noncomputable def TauCeti.GlobalNumberFields.rayUnitRepresentative {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) (q : (NumberField.RingOfIntegers K)Λ£ β§Έ unitsCongruenceSubgroupSupTorsion π”ͺ) :
      (NumberField.RingOfIntegers K)Λ£

      A representative of a coset of unitsCongruenceSubgroupSupTorsion π”ͺ.

      The identity coset is normalized to have representative 1. This normalization makes the fundamental domain for the trivial modulus agree literally with Mathlib's fundamental cone, rather than with an unspecified unit translate of it.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.rayUnitRepresentative_one {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
        rayUnitRepresentative π”ͺ 1 = 1

        The representative of the identity coset is the identity unit.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.rayUnitRepresentative_mk {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) (q : (NumberField.RingOfIntegers K)Λ£ β§Έ unitsCongruenceSubgroupSupTorsion π”ͺ) :
        ↑(rayUnitRepresentative π”ͺ q) = q

        The chosen representative maps back to the coset it represents.

        source
        def TauCeti.GlobalNumberFields.rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
        Set (NumberField.mixedEmbedding.mixedSpace K)

        The ray fundamental domain associated to a modulus: the points of the mixed space that carry the signs prescribed by the infinite part of π”ͺ and that one chosen unit-coset representative moves into Mathlib's fundamental cone.

        Equivalently, this is the intersection of posRegion π”ͺ with the union of the translates rayUnitRepresentative π”ͺ q β€’ fundamentalCone K over the finite quotient of the unit group by unitsCongruenceSubgroupSupTorsion π”ͺ; see rayFundamentalDomain_eq_iUnion.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem TauCeti.GlobalNumberFields.mem_rayFundamentalDomain_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} :
          x ∈ rayFundamentalDomain π”ͺ ↔ x ∈ posRegion π”ͺ ∧ βˆƒ (q : (NumberField.RingOfIntegers K)Λ£ β§Έ unitsCongruenceSubgroupSupTorsion π”ͺ), (rayUnitRepresentative π”ͺ q)⁻¹ β€’ x ∈ NumberField.mixedEmbedding.fundamentalCone K

          Membership in the ray fundamental domain, unfolded to the sign conditions and a chosen unit coset.

          source
          theorem TauCeti.GlobalNumberFields.mem_posRegion_of_mem_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ rayFundamentalDomain π”ͺ) :
          x ∈ posRegion π”ͺ

          A point of the ray fundamental domain carries the signs prescribed by π”ͺ.

          source
          theorem TauCeti.GlobalNumberFields.rayFundamentalDomain_eq_iUnion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
          rayFundamentalDomain π”ͺ = posRegion π”ͺ ∩ ⋃ (q : (NumberField.RingOfIntegers K)Λ£ β§Έ unitsCongruenceSubgroupSupTorsion π”ͺ), rayUnitRepresentative π”ͺ q β€’ NumberField.mixedEmbedding.fundamentalCone K

          The ray fundamental domain is the positivity region intersected with the finite union of the translates of Mathlib's fundamental cone by the chosen coset representatives.

          source
          theorem TauCeti.GlobalNumberFields.measurableSet_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
          MeasurableSet (rayFundamentalDomain π”ͺ)

          The ray fundamental domain is measurable: it is the intersection of an open region with a finite union of unit translates of Mathlib's measurable fundamental cone.

          source
          theorem TauCeti.GlobalNumberFields.norm_pos_of_mem_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ rayFundamentalDomain π”ͺ) :
          0 < NumberField.mixedEmbedding.norm x

          Every point of the ray fundamental domain has positive mixed norm.

          source
          theorem TauCeti.GlobalNumberFields.smul_mem_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ rayFundamentalDomain π”ͺ) {c : ℝ} (hc : 0 < c) :
          c β€’ x ∈ rayFundamentalDomain π”ͺ

          The ray fundamental domain is stable under multiplication by a positive real scalar. Negative scalars are excluded because they may violate nonempty sign conditions prescribed by the infinite part of π”ͺ.

          source
          @[simp]
          theorem TauCeti.GlobalNumberFields.smul_mem_rayFundamentalDomain_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} {c : ℝ} (hc : 0 < c) :
          c β€’ x ∈ rayFundamentalDomain π”ͺ ↔ x ∈ rayFundamentalDomain π”ͺ

          Multiplication by a positive real scalar preserves membership in the ray fundamental domain.

          source
          @[simp]
          theorem TauCeti.GlobalNumberFields.smul_rayFundamentalDomain_inter_normLeOne {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) {c : ℝ} (hc : 0 < c) :
          c β€’ (rayFundamentalDomain π”ͺ ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≀ 1}) = rayFundamentalDomain π”ͺ ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≀ c ^ Module.finrank β„š K}

          The norm grading is a dilation. Scaling by c > 0 preserves the ray fundamental domain and multiplies mixedEmbedding.norm by c ^ [K:β„š], so the dilate by c of the norm-≀-one section is the norm-≀-c ^ [K:β„š] section.

          It converts between the two gradings: the lattice-point estimate is stated for dilates of a fixed region, while ideals are counted by their absolute norm.

          source
          theorem TauCeti.GlobalNumberFields.torsion_smul_mem_rayFundamentalDomain_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} {ΞΆ : (NumberField.RingOfIntegers K)Λ£} (hΞΆ : ΞΆ ∈ NumberField.Units.torsion K) (hΞΆ' : ΞΆ ∈ unitsCongruenceSubgroup π”ͺ) :
          ΞΆ β€’ x ∈ rayFundamentalDomain π”ͺ ↔ x ∈ rayFundamentalDomain π”ͺ

          Multiplication by a root of unity congruent to one modulo π”ͺ preserves membership in the ray fundamental domain: the cone translates are stable under the torsion, and the prescribed signs are preserved because the unit is a congruence unit.

          This is not a simp lemma: Mathlib's NumberField.mixedEmbedding.unitSMul_smul is itself simp and rewrites the left-hand side to a product, so the statement is not in simp normal form.

          source
          def TauCeti.GlobalNumberFields.unitsCongruenceTorsion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
          Subgroup (NumberField.RingOfIntegers K)Λ£

          The roots of unity congruent to one modulo π”ͺ. By unitsCongruenceSubgroup_smul_mem_rayFundamentalDomain_iff_mem_torsion these are exactly the congruence units carrying a point of the ray fundamental domain back into it.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.GlobalNumberFields.mem_unitsCongruenceTorsion {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {u : (NumberField.RingOfIntegers K)Λ£} :
            u ∈ unitsCongruenceTorsion π”ͺ ↔ u ∈ unitsCongruenceSubgroup π”ͺ ∧ u ∈ NumberField.Units.torsion K

            Membership in unitsCongruenceTorsion, unfolded to the two defining conditions. The definition is not exposed, so Subgroup.mem_inf cannot see through it from another module.

            source
            instance TauCeti.GlobalNumberFields.instFiniteSubtypeUnitsRingOfIntegersMemSubgroupUnitsCongruenceTorsion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
            Finite β†₯(unitsCongruenceTorsion π”ͺ)

            unitsCongruenceTorsion π”ͺ is finite, being a subgroup of the roots of unity.

            source
            theorem TauCeti.GlobalNumberFields.index_unitsCongruenceSubgroup_mul_card_unitsCongruenceTorsion {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
            (unitsCongruenceSubgroup π”ͺ).index * Nat.card β†₯(unitsCongruenceTorsion π”ͺ) = (unitsCongruenceSubgroupSupTorsion π”ͺ).index * NumberField.Units.torsionOrder K

            The index of the congruence units, corrected by torsion. Adjoining the roots of unity to the units congruent to one modulo π”ͺ divides their index by the index of unitsCongruenceTorsion π”ͺ in the roots of unity: [E : E_π”ͺ] Β· #(E_π”ͺ ∩ ΞΌ_K) = [E : E_π”ͺ Β· ΞΌ_K] Β· #ΞΌ_K.

            The identity is stated multiplicatively, so it holds in β„• with no divisibility side condition.

            source
            theorem TauCeti.GlobalNumberFields.exists_unitsCongruenceSubgroup_smul_mem_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) {x : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x β‰  0) (hpos : x ∈ posRegion π”ͺ) :
            βˆƒ u ∈ unitsCongruenceSubgroup π”ͺ, u β€’ x ∈ rayFundamentalDomain π”ͺ

            Existence of a representative. Every point carrying the signs prescribed by π”ͺ and of nonzero mixed norm is moved into the ray fundamental domain by a unit congruent to one modulo π”ͺ.

            source
            @[simp]
            theorem TauCeti.GlobalNumberFields.rayFundamentalDomain_one {K : Type u_1} [Field K] [NumberField K] :
            rayFundamentalDomain (Modulus.one K) = NumberField.mixedEmbedding.fundamentalCone K

            The ray fundamental domain for the trivial modulus is Mathlib's fundamental cone.

            source
            theorem TauCeti.GlobalNumberFields.unitsCongruenceSubgroup_smul_mem_rayFundamentalDomain_iff_mem_torsion {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ rayFundamentalDomain π”ͺ) {u : (NumberField.RingOfIntegers K)Λ£} (hu : u ∈ unitsCongruenceSubgroup π”ͺ) :
            u β€’ x ∈ rayFundamentalDomain π”ͺ ↔ u ∈ NumberField.Units.torsion K

            Uniqueness of the representative, modulo roots of unity. A unit congruent to one modulo π”ͺ carries a point of the ray fundamental domain back into the ray fundamental domain exactly when it is a root of unity.

            Together with exists_unitsCongruenceSubgroup_smul_mem_rayFundamentalDomain this says that the domain meets each orbit of nonzero mixed norm of the congruence units inside posRegion π”ͺ in one point, modulo the congruence units that are roots of unity: the sense in which Mathlib's fundamental cone is fundamental for the full unit group.

            source
            theorem TauCeti.GlobalNumberFields.mul_inv_mem_torsion_of_smul_mem_rayFundamentalDomain {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.mixedEmbedding.mixedSpace K} {u v : (NumberField.RingOfIntegers K)Λ£} (huv : v * u⁻¹ ∈ unitsCongruenceSubgroup π”ͺ) (hux : u β€’ x ∈ rayFundamentalDomain π”ͺ) (hvx : v β€’ x ∈ rayFundamentalDomain π”ͺ) :
            v * u⁻¹ ∈ NumberField.Units.torsion K

            Two units carrying the same point into the ray fundamental domain and differing by a unit congruent to one modulo π”ͺ differ by a root of unity.