Module

OnePlaceNormKernel.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.OnePlaceNormKernel

11 declarations indexed from sourceView source ↗

Module documentation

The one-place norm kernel

At the source level, the key calculation is that an idele supported at one finite place is a global relative-idele norm exactly when its local component is a norm from the corresponding local tensor algebra. The determinant-norm comparison then identifies this image with the norm group of any chosen completion above the place.

Imports4

Imported by6

def

ideleNormSubgroup

L40 ↗

GlobalClassFieldTheory.Reciprocity.ideleNormSubgroup

Documentation

The image of the global norm on relative ideles.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def ideleNormSubgroup :
    Subgroup (IdeleGroup K)

abbrev

IdeleNormQuotient

L46 ↗

GlobalClassFieldTheory.Reciprocity.IdeleNormQuotient

Documentation

The raw idele norm quotient. Passing further to principal-idèle classes gives the class quotient used in the global reciprocity theorem.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev IdeleNormQuotient

def

ideleNormClass

L50 ↗

GlobalClassFieldTheory.Reciprocity.ideleNormClass

Documentation

The projection to the raw global norm quotient.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def ideleNormClass :
    IdeleGroup K →* IdeleNormQuotient (K := K) (L := L)

theorem

norm_relativeInfinitePlaceIdele

L57 ↗

GlobalClassFieldTheory.Reciprocity.norm_relativeInfinitePlaceIdele

Documentation

A relative idele supported at an archimedean place has norm equal to the one-place idele of its local determinant norm.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem norm_relativeInfinitePlaceIdele
    (v : InfinitePlace K)
    (z : (v.Completion ⊗[K] L)ˣ) :
    RelativeIdeleGroup.norm K L
        (relativeInfinitePlaceIdele
          (K := K) (L := L) v z) =
      infinitePlaceIdele v
        (infiniteTensorDetNorm
          (K := K) (L := L) v z)

theorem

infinitePlaceIdele_mem_ideleNormSubgroup_iff

L114 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceIdele_mem_ideleNormSubgroup_iff

Documentation

Exact archimedean one-place intersection before quotienting by principal ideles:

N(I_L) ∩ K_vˣ = N((K_v ⊗_K L)ˣ).

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem infinitePlaceIdele_mem_ideleNormSubgroup_iff
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    infinitePlaceIdele v x ∈
        ideleNormSubgroup (K := K) (L := L) ↔
      x ∈ infiniteTensorNormSubgroup
        (K := K) (L := L) v

theorem

ideleNormClass_comp_infinitePlaceIdele_ker

L140 ↗

GlobalClassFieldTheory.Reciprocity.ideleNormClass_comp_infinitePlaceIdele_ker

Documentation

Kernel-exact form of the archimedean one-place norm statement.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem ideleNormClass_comp_infinitePlaceIdele_ker
    (v : InfinitePlace K) :
    ((ideleNormClass (K := K) (L := L)).comp
        (infinitePlaceIdele v)).ker =
      infiniteTensorNormSubgroup
        (K := K) (L := L) v

theorem

norm_relativeFinitePlaceIdele

L162 ↗

GlobalClassFieldTheory.Reciprocity.norm_relativeFinitePlaceIdele

Documentation

A relative idele supported at v has norm equal to the one-place idele of its local determinant norm.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem norm_relativeFinitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K))
    (z : (v.adicCompletion K ⊗[K] L)ˣ) :
    RelativeIdeleGroup.norm K L
        (relativeFinitePlaceIdele (K := K) (L := L) v z) =
      finitePlaceIdele v
        (localTensorNorm (K := K) (L := L) v z)

theorem

finitePlaceIdele_mem_ideleNormSubgroup_iff

L209 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceIdele_mem_ideleNormSubgroup_iff

Documentation

Exact one-place intersection before quotienting by principal ideles:

N(I_L) ∩ K_vˣ = N((K_v ⊗_K L)ˣ).

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem finitePlaceIdele_mem_ideleNormSubgroup_iff
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    finitePlaceIdele v x ∈
        ideleNormSubgroup (K := K) (L := L) ↔
      x ∈ (localTensorNorm (K := K) (L := L) v).range

theorem

finitePlaceIdele_mem_ideleNormSubgroup_iff_chosenLocalNorm

L235 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceIdele_mem_ideleNormSubgroup_iff_chosenLocalNorm

Documentation

The finite-place tensor form with the actual chosen completion norm group.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in

Lean source · statement

theorem finitePlaceIdele_mem_ideleNormSubgroup_iff_chosenLocalNorm
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    finitePlaceIdele v x ∈
        ideleNormSubgroup (K := K) (L := L) ↔
      x ∈ chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

finitePlaceIdeleClass_mem_ideleClassNorm_range_of_mem_chosenLocalNorm

L251 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceIdeleClass_mem_ideleClassNorm_range_of_mem_chosenLocalNorm

Documentation

A chosen local norm at one finite place gives an actual global idele-class norm. The witness is the relative idele supported at that place, transported to an ordinary idele of the extension field.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceIdeleClass_mem_ideleClassNorm_range_of_mem_chosenLocalNorm
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (hx :
      x ∈ chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v) :
    IdeleGroup.finitePlaceIdeleClass v x ∈
      (_root_.ideleClassNorm K L).range

theorem

ideleNormClass_comp_finitePlaceIdele_ker

L283 ↗

GlobalClassFieldTheory.Reciprocity.ideleNormClass_comp_finitePlaceIdele_ker

Documentation

Kernel-exact form of the one-place norm statement.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in

Lean source · statement

theorem ideleNormClass_comp_finitePlaceIdele_ker
    (v : HeightOneSpectrum (𝓞 K)) :
    ((ideleNormClass (K := K) (L := L)).comp
        (finitePlaceIdele v)).ker =
      chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

Module documentation

The one-place norm kernel

Declarations