Module

AbelianNormConductor.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.AbelianNormConductor

2 declarations indexed from sourceView source ↗

Module documentation

Unramified finite places and abelian norm conductors

For a finite abelian extension of number fields, the selected local higher-unit exponent of the actual idèle-class norm subgroup vanishes exactly at the finite places where the chosen completed extension is unramified.

The converse to the general unramifiedness implication uses finite local reciprocity. Integral units are transported from the adic completion used by the idèle library to the absolute-value completion used by local class field theory, and the local conductor-zero criterion then detects unramifiedness.

Imports3

Imported by3

theorem

ideleClassNormLocalHigherUnitExponent_eq_zero_iff_chosenFinitePlaceIsUnramified

L50 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormLocalHigherUnitExponent_eq_zero_iff_chosenFinitePlaceIsUnramified

Documentation

For a finite abelian extension, the chosen finite-place norm conductor has exponent zero exactly when the chosen completed extension is unramified.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField L] in

Lean source · statement

theorem
    ideleClassNormLocalHigherUnitExponent_eq_zero_iff_chosenFinitePlaceIsUnramified
    (v : HeightOneSpectrum (𝓞 K)) :
    ideleClassNormLocalHigherUnitExponent
        (K := K) (L := L) v = 0 ↔
      _root_.ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v

theorem

mem_ideleClassNormDefiningModulus_support_iff_not_chosenFinitePlaceIsUnramified

L255 ↗

GlobalClassFieldTheory.GlobalClassFields.mem_ideleClassNormDefiningModulus_support_iff_not_chosenFinitePlaceIsUnramified