Documentation

TauCeti.NumberTheory.NumberField.Global.Adeles.Norm.Basic

The norm map of adeles #

Let L / K be an extension of number fields. The norm of L / K extends to a multiplicative map N_{L/K} : ๐”ธ_L โ†’ ๐”ธ_K of adele rings, defined place by place: the component of N_{L/K}(x) at a place v of K is the product, over the finitely many places w โˆฃ v of L, of the local norms N_{L_w/K_v}(x_w). At an infinite place this includes the norm z โ†ฆ |z|ยฒ of โ„‚ over โ„ when a complex place lies over a real one.

The finite component is again a finite adele because the local norm carries the completed integer ring ๐’ช_w into ๐’ช_v (IsDedekindDomain.HeightOneSpectrum.norm_mem_adicCompletionIntegers), and only finitely many places of K lie below the finitely many places of L at which a given finite adele of L is not integral.

The norm map is multiplicative but not additive. It extends the global norm along the diagonal embeddings: placewise, this is the semilocal factorization N_{L/K}(x) = โˆ_{w โˆฃ v} N_{L_w/K_v}(x). On adeles extended from K it is the [L : K]-th power, since the local degrees [L_w : K_v] over a fixed place v add up to [L : K]. The induced maps on ideles and idele classes are in TauCeti.NumberTheory.NumberField.Global.Ideles.Norm.Relative.

Main definitions #

Main results #

References #

Finite adeles #

source
theorem TauCeti.GlobalNumberFields.finprod_norm_mem_adicCompletionIntegers (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) โ†’ IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hx : โˆ€ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w = v โ†’ x w โˆˆ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w) :
โˆแถ  (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (x โ†‘w) โˆˆ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

The product of local norms above v is integral if every source coordinate above v is integral.

source
noncomputable def TauCeti.GlobalNumberFields.finiteAdeleNorm (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] :
IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L โ†’* IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K

The norm map of finite adeles. For an extension L / K of number fields, the component of the norm of a finite adele x of L at a finite place v of K is โˆ_{w โˆฃ v} N_{L_w/K_v}(x_w). It is multiplicative but not additive.

Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.finiteAdeleNorm_apply {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    ((finiteAdeleNorm K L) x) v = โˆแถ  (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (x โ†‘w)

    The component of the finite adele norm at v is the product of the local norms at the places above v.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.finiteAdeleNorm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : L) :
    (finiteAdeleNorm K L) ((algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)) ((Algebra.norm K) x)

    The finite adele norm extends the norm of L / K along the diagonal embeddings.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.finiteAdeleNorm_finiteAdeleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) :
    (finiteAdeleNorm K L) ((IsDedekindDomain.finiteAdeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a) = a ^ Module.finrank K L

    The norm of a finite adele extended from K is its [L : K]-th power.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.finiteAdeleNorm_comp (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] :
    (finiteAdeleNorm K L).comp (finiteAdeleNorm L M) = finiteAdeleNorm K M

    Norm maps of finite adeles compose in a tower K โŠ† L โŠ† M.

    Infinite adeles #

    source
    noncomputable def TauCeti.GlobalNumberFields.infiniteAdeleNorm (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] :
    NumberField.InfiniteAdeleRing L โ†’* NumberField.InfiniteAdeleRing K

    The norm map of infinite adeles. For an extension L / K of number fields, the component of the norm of an infinite adele x of L at an infinite place v of K is โˆ_{w โˆฃ v} N_{L_w/K_v}(x_w). At a complex place above a real place the local norm is z โ†ฆ |z|ยฒ.

    Instances For
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.infiniteAdeleNorm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.InfiniteAdeleRing L) (v : NumberField.InfinitePlace K) :
      (infiniteAdeleNorm K L) x v = โˆแถ  (w : { w : NumberField.InfinitePlace L // w.LiesOver v }), (Algebra.norm v.Completion) (x โ†‘w)

      The component of the infinite adele norm at v is the product of the local norms at the places above v.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.infiniteAdeleNorm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : L) :
      (infiniteAdeleNorm K L) ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = (algebraMap K (NumberField.InfiniteAdeleRing K)) ((Algebra.norm K) x)

      The infinite adele norm extends the norm of L / K along the diagonal embeddings.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.infiniteAdeleNorm_infiniteAdeleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (a : NumberField.InfiniteAdeleRing K) :
      (infiniteAdeleNorm K L) ((NumberField.infiniteAdeleExtension K L) a) = a ^ Module.finrank K L

      The norm of an infinite adele extended from K is its [L : K]-th power.

      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.infiniteAdeleNorm_comp (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] :
      (infiniteAdeleNorm K L).comp (infiniteAdeleNorm L M) = infiniteAdeleNorm K M

      Norm maps of infinite adeles compose when L and M are number fields over a field K.

      Adeles #

      source
      noncomputable def TauCeti.GlobalNumberFields.adeleNorm (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] :
      NumberField.AdeleRing (NumberField.RingOfIntegers L) L โ†’* NumberField.AdeleRing (NumberField.RingOfIntegers K) K

      The norm map of adeles N_{L/K} : ๐”ธ_L โ†’* ๐”ธ_K: infiniteAdeleNorm on the infinite component and finiteAdeleNorm on the finite component.

      Instances For
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.adeleNorm_fst {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.AdeleRing (NumberField.RingOfIntegers L) L) :
        ((adeleNorm K L) x).1 = (infiniteAdeleNorm K L) x.1

        The infinite component of the adele norm is the infinite adele norm.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.adeleNorm_snd {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : NumberField.AdeleRing (NumberField.RingOfIntegers L) L) :
        ((adeleNorm K L) x).2 = (finiteAdeleNorm K L) x.2

        The finite component of the adele norm is the finite adele norm.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.adeleNorm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : L) :
        (adeleNorm K L) ((algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) ((Algebra.norm K) x)

        The adele norm extends the norm of L / K along the diagonal embeddings: the norm of a principal adele is the principal adele of the norm.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.adeleNorm_adeleExtension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) :
        (adeleNorm K L) ((NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a) = a ^ Module.finrank K L

        The norm of an adele extended from K is its [L : K]-th power.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.adeleNorm_comp (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (M : Type u_3) [Field M] [NumberField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] :
        (adeleNorm K L).comp (adeleNorm L M) = adeleNorm K M

        Norm maps of adeles compose in a tower of number fields.