Module

FinitePlaceRayArtinDecomposition.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FinitePlaceRayArtinDecomposition

1 declaration indexed from sourceView source ↗

Module documentation

Ray Artin values at a finite place

The canonical one-place map into an ideal-theoretic ray class group has the actual local norm subgroup as its Artin kernel. Its Artin values preserve the absolute-value class of one extension of that place to the top field, including when the place divides the ray modulus.

Imports10

Imported by1

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.All

theorem

exists_finitePlaceRayArtin_decomposition

L38 ↗

ClassFieldTheory.exists_finitePlaceRayArtin_decomposition

Documentation

A Frobenius-normalized ray Artin map restricts at every finite place to the local norm quotient and lands in a decomposition group. The extension absolute value and the local-to-ray map are chosen independently of D's Artin values.

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_decomposition
    (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)) :
    ∃ (w : ExtendingAbsoluteValue
        (NumberField.HeightOneSpectrum.adicAbv K v) L)
      (ι : (v.adicCompletion K)ˣ →* RayClassGroup D.modulus),
      (D.artin.comp ι).ker = finitePlaceTensorNormSubgroup K L v ∧
      ∀ (x : (v.adicCompletion K)ˣ) (y : L),
        w.1 ((D.artin (ι x)) y) < 1 ↔ w.1 y < 1

Module documentation

Ray Artin values at a finite place

Declarations

exists_finitePlaceRayArtin_decomposition