Documentation

TauCeti.NumberTheory.NumberField.Global.Ideles.Norm.One

The norm-one idele class group #

The idele norm ‖·‖ : 𝕀_K → ℝ>0 of a number field K is trivial on the principal ideles by the product formula, so it descends to a continuous surjective homomorphism ideleClassNorm : C_K → ℝ>0 on the idele class group C_K = 𝕀_K / Kˣ. Its kernel is the norm-one idele class group C_K¹, a closed subgroup of C_K.

The full idele class group is not compact, since it surjects continuously onto the positive reals, and C_K¹ is a proper subgroup. The norm-one subgroup is the carrier of the compactness theorem for C_K¹, the adelic form of the finiteness of the class group and Dirichlet's unit theorem.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.GlobalNumberFields.ideleClassNorm {K : Type u_1} [Field K] [NumberField K] :
NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K →* NNRealˣ

The idele norm on the idele class group of a number field: the idele norm descends along the quotient by the principal ideles, on which it is trivial by the product formula.

Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.ideleClassNorm_mk {K : Type u_1} [Field K] [NumberField K] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) :
    ideleClassNorm ↑x = ideleNorm x

    The idele class norm of the class of an idele is its idele norm.

    source
    theorem TauCeti.GlobalNumberFields.coe_ideleClassNorm_pos {K : Type u_1} [Field K] [NumberField K] (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) :
    0 < ↑↑(ideleClassNorm c)

    The idele class norm of an idele class is a positive real number.

    source
    theorem TauCeti.GlobalNumberFields.continuous_ideleClassNorm {K : Type u_1} [Field K] [NumberField K] :
    Continuous ⇑ideleClassNorm

    The idele class norm is continuous.

    source
    theorem TauCeti.GlobalNumberFields.ideleClassNorm_surjective {K : Type u_1} [Field K] [NumberField K] :
    Function.Surjective ⇑ideleClassNorm

    The idele class norm is surjective.

    source
    noncomputable def TauCeti.GlobalNumberFields.IdeleClassGroup.normOne (K : Type u_1) [Field K] [NumberField K] :
    Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)

    The norm-one idele class group C_K¹ of a number field: the classes of ideles of idele norm one.

    Instances For
      source
      instance TauCeti.GlobalNumberFields.IdeleClassGroup.normal_normOne {K : Type u_1} [Field K] [NumberField K] :
      (normOne K).Normal

      The norm-one idele class group is normal, being a kernel.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.IdeleClassGroup.mem_normOne_iff {K : Type u_1} [Field K] [NumberField K] {x : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K} :
      x ∈ normOne K ↔ ideleClassNorm x = 1

      An idele class lies in the norm-one subgroup exactly when its idele class norm is 1.

      source
      theorem TauCeti.GlobalNumberFields.IdeleClassGroup.mk_mem_normOne_iff {K : Type u_1} [Field K] [NumberField K] {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} :
      ↑x ∈ normOne K ↔ ideleNorm x = 1

      The class of an idele lies in the norm-one subgroup exactly when the idele has norm 1.

      source
      theorem TauCeti.GlobalNumberFields.IdeleClassGroup.comap_normOne (K : Type u_1) [Field K] [NumberField K] :
      Subgroup.comap (QuotientGroup.mk' (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K)) (normOne K) = ideleNorm.ker

      The preimage of the norm-one idele class group in the idele group is the kernel of the idele norm.

      source
      theorem TauCeti.GlobalNumberFields.IdeleClassGroup.isClosed_normOne (K : Type u_1) [Field K] [NumberField K] :
      IsClosed ↑(normOne K)

      The norm-one idele class group is closed in the idele class group.

      source
      theorem TauCeti.GlobalNumberFields.IdeleClassGroup.normOne_ne_top (K : Type u_1) [Field K] [NumberField K] :
      normOne K ≠ ⊤

      The norm-one idele class group is a proper subgroup: the idele class norm is surjective onto the nontrivial group ℝ>0.

      source
      instance TauCeti.GlobalNumberFields.IdeleClassGroup.noncompactSpace (K : Type u_1) [Field K] [NumberField K] :
      NoncompactSpace (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)

      The idele class group of a number field is not compact: it surjects continuously onto the noncompact group ℝ>0. This is in contrast to the norm-one subgroup C_K¹, which is compact.