Documentation

TauCeti.NumberTheory.ClassFieldTheory.Global.AdmissibleModulus.Basic

Admissible moduli, the conductor, and the real places #

Let L/K be an extension of number fields. A modulus π”ͺ of K is admissible for L/K (IsAdmissibleModulus K L π”ͺ) when its ray subgroup lies in the idele-class norm group N_{L/K}(C_L). For an abelian extension this is the condition under which the global Artin map factors through the ray class group of π”ͺ, which is why ray-class reciprocity is stated for admissible moduli. Admissibility is inherited by multiples (IsAdmissibleModulus.of_dvd), because ray subgroups shrink as the modulus grows, and by subextensions (IsAdmissibleModulus.tower_bot), because norms compose in towers.

The norm group N_{L/K}(C_L) is open, so it has a conductor in the sense of OpenSubgroup.ideleClassConductor: the conductor abelianConductor K L of L/K is the least admissible modulus, and a modulus is admissible exactly when the conductor divides it (isAdmissibleModulus_iff_abelianConductor_dvd). The conductor of a subextension divides that of the extension (abelianConductor_dvd_abelianConductor). None of this uses a reciprocity law.

This file shows that the real places cannot be left out of an admissible modulus when L contains enough roots of unity. Let w be a real place of K and suppose that L contains a primitive pⁿ-th root of unity with pⁿ > 2. Then the idele class that is -1 at w and 1 everywhere else is not a norm from L (ofCompletion_neg_one_notMem_range_ideleClassNormMap). Suppose that (-1)_w Β· Ξ± is the norm of an idele of L for some Ξ± ∈ KΛ£. Then Ξ± is a local norm from K_v βŠ—[K] L at every place v β‰  w and -Ξ± is one at w, so, by abelianizedLocalCyclotomicCharacter_artinMap_mem_unitsPrincipal and its archimedean counterpart, the p-adic cyclotomic characters Ο‡_p(Art_v(Ξ±)) are ≑ 1 mod pⁿ for v β‰  w, while Ο‡_p(Art_w(Ξ±)) ≑ -1, since Ο‡_p(Art_w(-1)) = -1 at a real place. Their product is 1 by the cyclotomic product formula (finprod_mul_prod_abelianizedLocalCyclotomicCharacter_artinMap_eq_one), which forces -1 ≑ 1 mod pⁿ. No global reciprocity law is used.

That idele class lies in the ray subgroup of every modulus whose infinite part omits w (TauCeti.GlobalNumberFields.ofCompletion_mem_raySubgroup), so no such modulus is admissible (not_isAdmissibleModulus_of_forall_ne). For β„š(i)/β„š this rejects the trivial modulus (not_isAdmissibleModulus_one_Qi), whose ray class group is trivial although the unramified prime 3 does not split in β„š(i). It also rejects the modulus (4), which contains the only ramified prime: the conductor of β„š(i)/β„š is (4) Β· ∞. In terms of the conductor, every real place of K lies in the infinite part of the conductor of L/K (mem_abelianConductor_infinitePart), and the real place of β„š in that of β„š(i)/β„š (mem_abelianConductor_infinitePart_Qi).

Main definitions #

Main results #

References #

The class of -1 at a real place #

source
theorem TauCeti.ClassFieldTheory.ofCompletion_neg_one_notMem_range_ideleClassNormMap (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : β„•) [Fact (Nat.Prime p)] {w : NumberField.InfinitePlace K} (hw : w.IsReal) {n : β„•} {ΞΆ : L} (hΞΆ : IsPrimitiveRoot ΞΆ (p ^ n)) (hpn : 2 < p ^ n) :
(NumberField.IdeleClassGroup.ofCompletion (NumberField.RingOfIntegers K) K w) (-1) βˆ‰ (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The class of -1 at a real place is not a norm from an extension containing μ_{pⁿ}. Let w be a real place of K and let L/K contain a primitive pⁿ-th root of unity with pⁿ > 2. Then the idele class that is -1 at w and 1 at every other place is not the norm of an idele class of L.

Admissible moduli #

source
def TauCeti.ClassFieldTheory.IsAdmissibleModulus (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (π”ͺ : GlobalNumberFields.Modulus K) :
Prop

A modulus π”ͺ of K is admissible for the extension L/K when the ray subgroup of π”ͺ lies in the idele-class norm group N_{L/K}(C_L): every idele class satisfying the congruence and sign conditions of π”ͺ is a norm from L.

Instances For
    source
    theorem TauCeti.ClassFieldTheory.isAdmissibleModulus_iff {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {π”ͺ : GlobalNumberFields.Modulus K} :
    IsAdmissibleModulus K L π”ͺ ↔ GlobalNumberFields.raySubgroup π”ͺ ≀ (↑(GlobalNumberFields.ideleClassNormMap K L)).range

    The defining condition of an admissible modulus.

    source
    theorem TauCeti.ClassFieldTheory.IsAdmissibleModulus.of_dvd {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {π”ͺ 𝔫 : GlobalNumberFields.Modulus K} (hπ”ͺ : IsAdmissibleModulus K L π”ͺ) (h : π”ͺ ∣ 𝔫) :
    IsAdmissibleModulus K L 𝔫

    Admissibility passes to multiples: the ray subgroup shrinks as the modulus grows.

    source
    theorem TauCeti.ClassFieldTheory.IsAdmissibleModulus.tower_bot {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {M : Type} [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] {π”ͺ : GlobalNumberFields.Modulus K} (h : IsAdmissibleModulus K M π”ͺ) :
    IsAdmissibleModulus K L π”ͺ

    Admissibility passes to subextensions: a norm from M is a norm from every intermediate field L.

    The conductor #

    source
    noncomputable def TauCeti.ClassFieldTheory.abelianConductor (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] :
    GlobalNumberFields.Modulus K

    The conductor of an extension of number fields: the least admissible modulus of L/K, that is, the conductor of the idele-class norm group N_{L/K}(C_L), which is open. The admissible moduli are exactly its multiples (isAdmissibleModulus_iff_abelianConductor_dvd). For an abelian extension this is the conductor of class field theory; the definition itself uses only that the norm group is open, so it needs no hypothesis on L/K.

    Instances For
      source
      theorem TauCeti.ClassFieldTheory.isAdmissibleModulus_iff_abelianConductor_dvd {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (π”ͺ : GlobalNumberFields.Modulus K) :
      IsAdmissibleModulus K L π”ͺ ↔ abelianConductor K L ∣ π”ͺ

      The characterization of admissibility: a modulus is admissible for L/K exactly when the conductor of L/K divides it.

      source
      theorem TauCeti.ClassFieldTheory.exponent_abelianConductor_le_iff {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {n : β„•} :
      (abelianConductor K L).exponent v ≀ n ↔ βˆ€ u ∈ unitFiltration (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) n, ↑((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) u) ∈ (↑(GlobalNumberFields.ideleClassNormMap K L)).range

      The exponents of the conductor are local. The exponent of a finite place v of K in the conductor of L/K is at most n exactly when the class of every idele concentrated at v with component in U(K_v, n) is a norm from L.

      source
      theorem TauCeti.ClassFieldTheory.isAdmissibleModulus_abelianConductor (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] :
      IsAdmissibleModulus K L (abelianConductor K L)

      The conductor of L/K is admissible for L/K.

      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.abelianConductor_self (K : Type) [Field K] [NumberField K] :
      abelianConductor K K = GlobalNumberFields.Modulus.one K

      The trivial extension has the trivial conductor.

      source
      theorem TauCeti.ClassFieldTheory.abelianConductor_dvd_abelianConductor {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] :
      abelianConductor K L ∣ abelianConductor K M

      The conductor of a subextension divides the conductor of the extension: for a tower K βŠ† L βŠ† M, the conductor of L/K divides that of M/K.

      source
      theorem TauCeti.ClassFieldTheory.not_isAdmissibleModulus_of_forall_ne {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : β„•) [Fact (Nat.Prime p)] {π”ͺ : GlobalNumberFields.Modulus K} {w : NumberField.InfinitePlace K} (hw : w.IsReal) (hwπ”ͺ : βˆ€ w' ∈ π”ͺ.infinitePart, ↑w' β‰  w) {n : β„•} {ΞΆ : L} (hΞΆ : IsPrimitiveRoot ΞΆ (p ^ n)) (hpn : 2 < p ^ n) :
      Β¬IsAdmissibleModulus K L π”ͺ

      A modulus omitting a real place is not admissible for an extension containing ΞΌ_{pⁿ}. If L contains a primitive pⁿ-th root of unity with pⁿ > 2 and the real place w of K is not in the infinite part of π”ͺ, then π”ͺ is not admissible for L/K.

      source
      theorem TauCeti.ClassFieldTheory.not_isAdmissibleModulus_one_Qi (E : Type) [Field E] [NumberField E] [Algebra β„š E] [IsCyclotomicExtension {4} β„š E] :
      Β¬IsAdmissibleModulus β„š E (GlobalNumberFields.Modulus.one β„š)

      The trivial modulus is not admissible for β„š(i)/β„š, although the ray class group of β„š for the trivial modulus is trivial.

      source
      theorem TauCeti.ClassFieldTheory.mem_abelianConductor_infinitePart {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : β„•) [Fact (Nat.Prime p)] (w : { w : NumberField.InfinitePlace K // w.IsReal }) {n : β„•} {ΞΆ : L} (hΞΆ : IsPrimitiveRoot ΞΆ (p ^ n)) (hpn : 2 < p ^ n) :
      w ∈ (abelianConductor K L).infinitePart

      The conductor of an extension containing μ_{pⁿ} contains every real place. If L contains a primitive pⁿ-th root of unity with pⁿ > 2, every real place of K lies in the infinite part of the conductor of L/K.

      source
      theorem TauCeti.ClassFieldTheory.mem_abelianConductor_infinitePart_Qi (E : Type) [Field E] [NumberField E] [Algebra β„š E] [IsCyclotomicExtension {4} β„š E] :
      ⟨Rat.infinitePlace, Rat.isReal_infinitePlace⟩ ∈ (abelianConductor β„š E).infinitePart

      The conductor of β„š(i)/β„š contains the real place of β„š.