Module

AbelianConductorFiniteNormCriterion.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.AbelianConductorFiniteNormCriterion

1 declaration indexed from sourceView source ↗

Module documentation

Finite conductor exponents and local norms

The finite exponent of the conductor is characterized by the determinant norm from K_v ⊗[K] L. This formulation does not choose a place of L above v; the implementation proves that the tensor norm image agrees with the norm group of a chosen local field extension.

Imports8

Imported by2

theorem

finiteExponent_le_iff_higherUnit_le_tensorNorm

L34 ↗

ClassFieldTheory.IsAbelianConductor.finiteExponent_le_iff_higherUnit_le_tensorNorm

Documentation

The conductor exponent at v is at most n exactly when the n-th higher-unit group lies in the finite-place tensor norm image.

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 IsAbelianConductor.finiteExponent_le_iff_higherUnit_le_tensorNorm
    {K : Type} [Field K] [NumberField K]
    {L : Type} [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    {c : RayClassModulus K}
    (hc : IsAbelianConductor K L c)
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    c.finitePart v ≤ n ↔
      rayLocalHigherUnitGroup v n ≤
        (Units.map (Algebra.norm (v.adicCompletion K)) :
          (v.adicCompletion K ⊗[K] L)ˣ →*
            (v.adicCompletion K)ˣ).range

Module documentation

Finite conductor exponents and local norms

Declarations

finiteExponent_le_iff_higherUnit_le_tensorNorm