NYLL
Module

FinitePlaceLocalGlobalNormKernel.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceLocalGlobalNormKernel
1 declaration indexed from sourceView source ↗

Module documentation

Finite-place norm kernels of a global Artin map

This is a Mathlib-typed local--global compatibility statement. Restricting one global Artin map along Mathlib's one-place idèle-class homomorphism has the local tensor-norm group as its kernel. It specifies the kernel at each finite place, not yet the value normalization against a separately chosen local Artin map or the real-place comparison.

The proof transports the established restricted-product reciprocity map through the algebraic comparison with Mathlib's idèle class group.

Imports9
Imported by1

Declarations

theorem

exists_finiteAbelianGlobalArtin_finitePlaceNormKernel

L39 ↗
ClassFieldTheory.exists_finiteAbelianGlobalArtin_finitePlaceNormKernel
Documentation

A finite abelian extension has one global Artin homomorphism whose restriction to each finite completion has precisely the tensor-norm kernel.

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_finiteAbelianGlobalArtin_finitePlaceNormKernel
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    ∃ artin : NumberField.IdeleClassGroup (𝓞 K) K →*
        (L ≃ₐ[K] L),
      Function.Surjective artin ∧
      ∀ (v : HeightOneSpectrum (𝓞 K))
        (x : (v.adicCompletion K)ˣ),
        artin (NumberField.IdeleClassGroup.ofAdicCompletion (𝓞 K) K v x) = 1 ↔
          x ∈ finitePlaceTensorNormSubgroup K L v

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.