Documentation

TauCeti.NumberTheory.NumberField.Global.Counting.RayFundamentalDomain.IntegerSet

Algebraic integers in the ray fundamental domain #

Counting the integral ideals of a ray class goes through the points of the ray fundamental domain that are images of algebraic integers. This file introduces that carrier, rayIntegerSet π”ͺ, and the map recovering the integer a point comes from.

An element of rayIntegerSet π”ͺ has a unique preimage in π“ž K, because mixedEmbedding is injective, and that preimage is nonzero, since the ray fundamental domain has no point of vanishing norm (norm_pos_of_mem_rayFundamentalDomain). The preimage is therefore recorded in (π“ž K)⁰, so that its nonzero-ness travels with the value.

For the trivial modulus this is Mathlib's NumberField.mixedEmbedding.fundamentalCone.integerSet.

The carrier also carries an action: a congruence unit sends a point of the domain back into the domain exactly when it is a root of unity, so the roots of unity congruent to one modulo π”ͺ act on rayIntegerSet π”ͺ, and that action is free. Counting a ray class will divide by the size of its orbits, which is what makes freeness the fact worth isolating here.

Main definitions #

Main results #

References #

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

The points of the ray fundamental domain of π”ͺ that are images of algebraic integers.

Equations
Instances For
    source
    theorem TauCeti.GlobalNumberFields.mem_rayIntegerSet {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {a : NumberField.mixedEmbedding.mixedSpace K} :
    a ∈ rayIntegerSet π”ͺ ↔ a ∈ rayFundamentalDomain π”ͺ ∧ βˆƒ (x : NumberField.RingOfIntegers K), (NumberField.mixedEmbedding K) ↑x = a

    Membership in rayIntegerSet: a point of the ray fundamental domain that is the image of an algebraic integer.

    source
    theorem TauCeti.GlobalNumberFields.existsUnique_preimage_of_mem_rayIntegerSet {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {a : NumberField.mixedEmbedding.mixedSpace K} (ha : a ∈ rayIntegerSet π”ͺ) :
    βˆƒ! x : NumberField.RingOfIntegers K, (NumberField.mixedEmbedding K) ↑x = a

    A point of the ray fundamental domain that is the image of an algebraic integer is the image of exactly one, since mixedEmbedding is injective.

    source
    theorem TauCeti.GlobalNumberFields.ne_zero_of_mem_rayIntegerSet {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (a : ↑(rayIntegerSet π”ͺ)) :
    ↑a β‰  0

    A point of rayIntegerSet is nonzero, since the ray fundamental domain has no point of vanishing norm.

    source
    noncomputable def TauCeti.GlobalNumberFields.preimageOfMemRayIntegerSet {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (a : ↑(rayIntegerSet π”ͺ)) :
    β†₯(nonZeroDivisors (NumberField.RingOfIntegers K))

    The unique algebraic integer a point of rayIntegerSet π”ͺ is the image of, recorded as an element of the nonzero divisors (π“ž K)⁰.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.mixedEmbedding_preimageOfMemRayIntegerSet {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (a : ↑(rayIntegerSet π”ͺ)) :
      (NumberField.mixedEmbedding K) ↑↑(preimageOfMemRayIntegerSet a) = ↑a

      The preimage map is a section of mixedEmbedding: embedding the integer it returns recovers the point.

      source
      theorem TauCeti.GlobalNumberFields.preimageOfMemRayIntegerSet_mixedEmbedding {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.RingOfIntegers K} (hx : (NumberField.mixedEmbedding K) ↑x ∈ rayIntegerSet π”ͺ) :
      ↑(preimageOfMemRayIntegerSet ⟨(NumberField.mixedEmbedding K) ↑x, hx⟩) = x

      The preimage map is a retraction of mixedEmbedding: an integer whose image lies in the carrier is returned unchanged.

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

      Agreement with Mathlib at the trivial modulus. The trivial modulus recovers NumberField.mixedEmbedding.fundamentalCone.integerSet, since its ray fundamental domain is the fundamental cone.

      The free action of the congruence roots of unity #

      source
      theorem TauCeti.GlobalNumberFields.unitsCongruenceTorsion_smul_mem_rayIntegerSet {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {ΞΆ : (NumberField.RingOfIntegers K)Λ£} (hΞΆ : ΞΆ ∈ unitsCongruenceTorsion π”ͺ) {a : NumberField.mixedEmbedding.mixedSpace K} (ha : a ∈ rayIntegerSet π”ͺ) :
      ΞΆ β€’ a ∈ rayIntegerSet π”ͺ

      rayIntegerSet π”ͺ is stable under the congruence roots of unity.

      source
      @[instance_reducible]
      noncomputable instance TauCeti.GlobalNumberFields.rayIntegerSetUnitsCongruenceTorsionSMul {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      SMul β†₯(unitsCongruenceTorsion π”ͺ) ↑(rayIntegerSet π”ͺ)

      The action of the congruence roots of unity on rayIntegerSet π”ͺ.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.rayIntegerSetUnitsCongruenceTorsionSMul_smul_coe {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) (x✝ : β†₯(unitsCongruenceTorsion π”ͺ)) (x✝¹ : ↑(rayIntegerSet π”ͺ)) :
      ↑(x✝ β€’ x✝¹) = ↑x✝ β€’ ↑x✝¹
      source
      @[instance_reducible]
      noncomputable instance TauCeti.GlobalNumberFields.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupUnitsCongruenceTorsionElemMixedSpaceRayIntegerSet {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      MulAction β†₯(unitsCongruenceTorsion π”ͺ) ↑(rayIntegerSet π”ͺ)

      The scalar action of the congruence roots of unity is a group action, which is what stabilizer_rayIntegerSet_eq_bot below speaks about. It is transported along the injection into the mixed space, where the action laws are Mathlib's.

      Equations
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.preimageOfMemRayIntegerSet_smul {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (ΞΆ : β†₯(unitsCongruenceTorsion π”ͺ)) (a : ↑(rayIntegerSet π”ͺ)) :
      ↑(preimageOfMemRayIntegerSet (ΞΆ β€’ a)) = ↑↑΢ * ↑(preimageOfMemRayIntegerSet a)

      A congruence root of unity acts on rayIntegerSet π”ͺ by multiplying the underlying algebraic integer.

      source
      theorem TauCeti.GlobalNumberFields.stabilizer_rayIntegerSet_eq_bot {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} (a : ↑(rayIntegerSet π”ͺ)) :
      MulAction.stabilizer (β†₯(unitsCongruenceTorsion π”ͺ)) a = βŠ₯

      The action is free. A congruence root of unity fixing a point of rayIntegerSet π”ͺ is the identity, because the point is the image of a nonzero algebraic integer.

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

      Freeness as a typeclass. Exposing stabilizer_rayIntegerSet_eq_bot as IsCancelSMul lets the generic free-action and orbit-cardinality results apply to this action by instance resolution, which is how the ray class count consumes it.