Documentation

TauCeti.NumberTheory.NumberField.Global.Ideles.Congruence

The idele congruence subgroup of a modulus #

Let K be a number field and π”ͺ a modulus of K. The idele congruence subgroup ideleCongruenceSubgroup π”ͺ is the subgroup of the idele group cut out placewise by the conditions that π”ͺ prescribes:

A principal unit of positive level is a unit of the valuation ring, so an idele of the congruence subgroup is a unit at every finite place: the fractional ideal it defines is trivial. This is ideleCongruenceSubgroup.valued_ideleFiniteCoord_eq_one, and it is what makes the principal ideles of the congruence subgroup exactly the units of π“ž K congruent to one modulo π”ͺ (unitEmbedding_mem_ideleCongruenceSubgroup_iff).

Dropping the unit conditions away from π”ͺ gives the larger subgroup ideleCongrOneSubgroup π”ͺ of ideles congruent to one modulo π”ͺ, which imposes conditions only at the places of π”ͺ. It is the idelic counterpart of congruenceSubgroup π”ͺ: a principal idele is congruent to one exactly when its generator is (unitEmbedding_mem_ideleCongrOneSubgroup_iff). Such an idele is still a unit at every finite divisor of π”ͺ, so the fractional ideal it defines is prime to π”ͺ; this is what lets it be sent to the ray class group.

The two structural facts about the family π”ͺ ↦ ideleCongruenceSubgroup π”ͺ are that each member is open in the idele topology β€” the conditions at the finitely many places of π”ͺ are open, and away from them the condition is membership in the open subgroup of everywhere-integral ideles β€” and that the family is antitone: a larger modulus imposes stronger conditions. Moreover the congruence subgroup of the greatest common divisor of two moduli is generated by the two congruence subgroups, since an idele can be split placewise into two factors.

Main definitions #

Main results #

References #

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

The ideles congruent to one modulo a modulus: the ideles that are principal units of the prescribed level at the finite divisors of π”ͺ and positive at the real places selected by π”ͺ. No condition is imposed at any other place. This is the idelic counterpart of congruenceSubgroup π”ͺ (unitEmbedding_mem_ideleCongrOneSubgroup_iff).

Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.mem_ideleCongrOneSubgroup_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} :
    x ∈ ideleCongrOneSubgroup π”ͺ ↔ (βˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v.asIdeal ∣ π”ͺ.finitePart β†’ Valued.v (↑(v.ideleFiniteCoord x) - 1) ≀ WithZero.exp (-↑(π”ͺ.exponent v))) ∧ βˆ€ w ∈ π”ͺ.infinitePart, 0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal β‹―) ↑((↑w).ideleInfiniteCoord x)

    The placewise conditions defining the ideles congruent to one.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.ideleCongrOneSubgroup_one {K : Type u_1} [Field K] [NumberField K] :
    ideleCongrOneSubgroup (Modulus.one K) = ⊀

    The trivial modulus imposes no congruence conditions on an idele.

    source
    theorem TauCeti.GlobalNumberFields.ideleCongrOneSubgroup.valued_ideleFiniteCoord_eq_one {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongrOneSubgroup π”ͺ) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v.asIdeal ∣ π”ͺ.finitePart) :
    Valued.v ↑(v.ideleFiniteCoord x) = 1

    An idele congruent to one is a unit at every finite divisor of the modulus, because the prescribed exponent there is positive.

    source
    theorem TauCeti.GlobalNumberFields.ideleCongrOneSubgroup_antitone {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} (h : π”ͺ ∣ 𝔫) :
    ideleCongrOneSubgroup 𝔫 ≀ ideleCongrOneSubgroup π”ͺ

    The ideles congruent to one decrease as the modulus grows.

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

    The idele congruence subgroup of a modulus: the ideles congruent to one modulo π”ͺ that are moreover units of the valuation ring at the finite places not dividing π”ͺ. Explicitly, they are principal units of the prescribed level at the finite divisors of π”ͺ, units of the valuation ring at the remaining finite places, and positive at the real places selected by π”ͺ. No condition is imposed at the infinite places outside π”ͺ.

    Instances For
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.mem_ideleCongruenceSubgroup_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} :
      x ∈ ideleCongruenceSubgroup π”ͺ ↔ (βˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Β¬v.asIdeal ∣ π”ͺ.finitePart β†’ Valued.v ↑(v.ideleFiniteCoord x) = 1) ∧ (βˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v.asIdeal ∣ π”ͺ.finitePart β†’ Valued.v (↑(v.ideleFiniteCoord x) - 1) ≀ WithZero.exp (-↑(π”ͺ.exponent v))) ∧ βˆ€ w ∈ π”ͺ.infinitePart, 0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal β‹―) ↑((↑w).ideleInfiniteCoord x)

      The placewise conditions defining the idele congruence subgroup.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.valued_ideleFiniteCoord_sub_one_le {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup π”ͺ) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v.asIdeal ∣ π”ͺ.finitePart) :
      Valued.v (↑(v.ideleFiniteCoord x) - 1) ≀ WithZero.exp (-↑(π”ͺ.exponent v))
      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.extensionEmbeddingOfIsReal_pos {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup π”ͺ) {w : { w : NumberField.InfinitePlace K // w.IsReal }} (hw : w ∈ π”ͺ.infinitePart) :
      0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal β‹―) ↑((↑w).ideleInfiniteCoord x)
      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.valued_ideleFiniteCoord_eq_one {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup π”ͺ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
      Valued.v ↑(v.ideleFiniteCoord x) = 1

      An idele of the congruence subgroup is a unit at every finite place. Away from the finite part this is the defining condition, and at a divisor of the finite part it follows from the congruence, because the prescribed exponent there is positive.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.snd_mem_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup π”ͺ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
      (↑x).2 v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

      The finite components of a congruence idele are integral: at every finite place v, the v-component of the underlying adele lies in the valuation ring.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.valued_snd_sub_one_le_of_pow_dvd {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup π”ͺ) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {n : β„•} (hn : v.asIdeal ^ n ∣ π”ͺ.finitePart) :
      Valued.v ((↑x).2 v - 1) ≀ WithZero.exp (-↑n)

      The congruence condition on the underlying adele: if v ^ n divides the finite part of π”ͺ, then the v-component of a congruence idele is congruent to 1 to level n. For n = 0 this is the integrality of the component.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup_antitone {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} (h : π”ͺ ∣ 𝔫) :
      ideleCongruenceSubgroup 𝔫 ≀ ideleCongruenceSubgroup π”ͺ

      The idele congruence subgroups decrease as the modulus grows.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup_le_ideleCongrOneSubgroup {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      ideleCongruenceSubgroup π”ͺ ≀ ideleCongrOneSubgroup π”ͺ

      The idele congruence subgroup lies in the ideles congruent to one.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.ideleFiniteCoord_mem_unitFiltration {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup π”ͺ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
      v.ideleFiniteCoord x ∈ unitFiltration (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (π”ͺ.exponent v)

      The finite coordinates of a congruence idele lie in the prescribed steps of the unit filtration: at every finite place v, the coordinate of an idele of ideleCongruenceSubgroup π”ͺ lies in U(K_v, π”ͺ.exponent v).

      source
      theorem TauCeti.GlobalNumberFields.ofAdicCompletion_mem_ideleCongruenceSubgroup_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)Λ£} :
      (NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) u ∈ ideleCongruenceSubgroup π”ͺ ↔ u ∈ unitFiltration (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (π”ͺ.exponent v)

      An idele concentrated at one finite place lies in the congruence subgroup exactly when its component lies in the prescribed step of the unit filtration. For u ∈ K_vΛ£, the idele with component u at v and 1 elsewhere lies in ideleCongruenceSubgroup π”ͺ exactly when u ∈ U(K_v, π”ͺ.exponent v): a unit of π“ž_v when v does not divide π”ͺ, and a principal unit of level π”ͺ.exponent v when it does.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup.inv_ofAdicCompletion_mul_mem {K : Type u_1} [Field K] [NumberField K] {π”ͺ 𝔫 : Modulus K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hexp : βˆ€ (v' : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), v' β‰  v β†’ π”ͺ.exponent v' ≀ 𝔫.exponent v') (hinf : π”ͺ.infinitePart βŠ† 𝔫.infinitePart) {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongruenceSubgroup 𝔫) :
      ((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) (v.ideleFiniteCoord x))⁻¹ * x ∈ ideleCongruenceSubgroup π”ͺ

      Removing the component at one place from a congruence idele. Let v be a finite place and let the modulus π”ͺ impose, away from v, no condition that 𝔫 does not. Dividing an idele of the congruence subgroup of 𝔫 by the idele concentrated at v with the same v-component gives an idele of the congruence subgroup of π”ͺ.

      Openness #

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

      The idele congruence subgroup is open. Away from the modulus the condition is membership in the open subring of everywhere-integral adeles, at the finitely many finite divisors of π”ͺ it is a closed valuation ball, and at the finitely many selected real places it is a strict inequality; imposing the same conditions on x and on x⁻¹ turns the integrality conditions into the unit conditions.

      Principal ideles and the trivial modulus #

      source
      theorem TauCeti.GlobalNumberFields.unitEmbedding_mem_ideleCongrOneSubgroup_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : KΛ£} :
      (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) x ∈ ideleCongrOneSubgroup π”ͺ ↔ IsCongrOne π”ͺ x

      The principal ideles congruent to one are the elements congruent to one. At a finite divisor of π”ͺ the coordinate of a principal idele is the global element, whose valuation in the completion is its v-adic valuation, and at a real place its sign is that of the real embedding.

      source
      theorem TauCeti.GlobalNumberFields.unitEmbedding_mem_ideleCongruenceSubgroup_iff {K : Type u_1} [Field K] [NumberField K] {π”ͺ : Modulus K} {x : KΛ£} :
      (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) x ∈ ideleCongruenceSubgroup π”ͺ ↔ x ∈ Subgroup.map (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) (unitsCongruenceSubgroup π”ͺ)

      The principal ideles of the congruence subgroup are the congruence units. A principal idele lies in ideleCongruenceSubgroup π”ͺ exactly when its generator is the image of a unit of π“ž K congruent to one modulo π”ͺ: the local unit conditions force the generator to be integral together with its inverse, and what is left of the conditions is IsCongrOne π”ͺ.

      source
      theorem TauCeti.GlobalNumberFields.mem_ideleCongruenceSubgroup_one_iff {K : Type u_1} [Field K] [NumberField K] {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} :
      x ∈ ideleCongruenceSubgroup (Modulus.one K) ↔ βˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Valued.v ↑(v.ideleFiniteCoord x) = 1

      The trivial modulus gives the ideles that are units at every finite place. No prime divides the unit ideal and the infinite part is empty, so only the local unit conditions survive.

      source
      theorem TauCeti.GlobalNumberFields.ideleCongrOneSubgroup_inf_ideleCongruenceSubgroup_one {K : Type u_1} [Field K] [NumberField K] (π”ͺ : Modulus K) :
      ideleCongrOneSubgroup π”ͺ βŠ“ ideleCongruenceSubgroup (Modulus.one K) = ideleCongruenceSubgroup π”ͺ

      The idele congruence subgroup consists of the ideles congruent to one that are units at every finite place.

      The greatest common divisor of two moduli #

      source
      theorem TauCeti.GlobalNumberFields.ideleCongruenceSubgroup_gcd {K : Type u_1} [Field K] [NumberField K] (π”ͺ 𝔫 : Modulus K) :
      ideleCongruenceSubgroup (π”ͺ.gcd 𝔫) = ideleCongruenceSubgroup π”ͺ βŠ” ideleCongruenceSubgroup 𝔫

      The idele congruence subgroup of a greatest common divisor is generated by the two congruence subgroups. An idele satisfying the conditions of π”ͺ.gcd 𝔫 is split into two ideles by distributing its components: the components at the finite places where π”ͺ has the larger exponent and at the real places of π”ͺ outside 𝔫 form an idele of the congruence subgroup of 𝔫, and the remaining components form an idele of the congruence subgroup of π”ͺ.