Module

FinitePlaceRayArtinNormKernel.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceRayArtinNormKernel

1 declaration indexed from sourceView source ↗

Module documentation

The local kernel of a ray-class Artin map

The local-to-ray map is constructed from a one-place idèle class. This statement compares the kernel of the resulting ray-class Artin map with the determinant norm of the entire local tensor algebra, at every finite place, including places in the modulus. It is a kernel comparison; the stronger equality of the Artin values is a separate normalization question.

Imports5

Imported by1

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.All

theorem

exists_finitePlaceRayArtin_normKernel

L33 ↗

ClassFieldTheory.exists_finitePlaceRayArtin_normKernel

Documentation

At every finite place, including a ramified place, the ray-class Artin map has the local tensor-norm subgroup as its kernel after the canonical one-place map into the ray class group.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem exists_finitePlaceRayArtin_normKernel
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L)
    (v : HeightOneSpectrum (𝓞 K)) :
    ∃ ι : (v.adicCompletion K)ˣ →* RayClassGroup D.modulus,
      (D.artin.comp ι).ker = finitePlaceTensorNormSubgroup K L v

Module documentation

The local kernel of a ray-class Artin map

Declarations

exists_finitePlaceRayArtin_normKernel