Module

Conductor.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Conductor

10 declarations indexed from sourceView source ↗

Module documentation

Conductors of finite abelian local extensions

For a finite abelian extension L / K, define its conductor exponent as the least n ≥ 0 for which the n-th principal-unit group of K lies in the norm subgroup. The conductor itself is the corresponding power of the maximal ideal of the valuation ring of K.

The existence of this least exponent is not an extra hypothesis here. It follows from openness of the norm subgroup of the actual finite extension and the principal-unit neighbourhood basis.

Imports3

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.TopologicalReciprocity
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.StandardOpenSubgroups
Mathlib.FieldTheory.Galois.Abelian

Imported by3

theorem

fieldPrincipalUnits_antitone

L34 ↗

LocalClassFieldTheory.fieldPrincipalUnits_antitone

Documentation

The field-level principal-unit filtration is antitone in its exponent.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem fieldPrincipalUnits_antitone
    (K : Type) [Field K] [ValuativeRel K]
    {m n : ℕ} (hmn : m ≤ n) :
    LocalFieldTheory.fieldPrincipalUnits K n ≤ LocalFieldTheory.fieldPrincipalUnits K m

theorem

exists_fieldPrincipalUnits_le_normSubgroup

L43 ↗

LocalClassFieldTheory.exists_fieldPrincipalUnits_le_normSubgroup

Documentation

For an actual finite abelian local extension, some principal-unit group is contained in its norm subgroup. This supplies the least conductor exponent.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem exists_fieldPrincipalUnits_le_normSubgroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ n : ℕ, LocalFieldTheory.fieldPrincipalUnits K n ≤ localNormSubgroup K L

def

localConductorExponent

L56 ↗

LocalClassFieldTheory.localConductorExponent

Documentation

The least principal-unit depth contained in the norm subgroup of the finite abelian extension L / K.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

def localConductorExponent
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : ℕ

theorem

localConductorExponent_spec

L66 ↗

LocalClassFieldTheory.localConductorExponent_spec

Documentation

The principal-unit group at the conductor exponent is contained in the norm subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_spec
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    LocalFieldTheory.fieldPrincipalUnits K (localConductorExponent K L) ≤
      localNormSubgroup K L

theorem

localConductorExponent_min

L77 ↗

LocalClassFieldTheory.localConductorExponent_min

Documentation

Minimality of the conductor exponent.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_min
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {n : ℕ} (hn : LocalFieldTheory.fieldPrincipalUnits K n ≤ localNormSubgroup K L) :
    localConductorExponent K L ≤ n

theorem

localConductorExponent_le_iff

L89 ↗

LocalClassFieldTheory.localConductorExponent_le_iff

Documentation

A depth contains the conductor depth exactly when its principal units are already norms. This records both the defining property and its minimality.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_le_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) :
    localConductorExponent K L ≤ n ↔
      LocalFieldTheory.fieldPrincipalUnits K n ≤ localNormSubgroup K L

def

localConductorIdeal

L105 ↗

LocalClassFieldTheory.localConductorIdeal

Documentation

The conductor ideal p_K ^ n, where n is the least principal-unit depth contained in the norm subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

def localConductorIdeal
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Ideal 𝒪[K]

theorem

localConductorExponent_eq_zero_iff

L114 ↗

LocalClassFieldTheory.localConductorExponent_eq_zero_iff

Documentation

The conductor exponent is zero exactly when the whole unit group U_K = U_K^(0) is contained in the norm subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_eq_zero_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    localConductorExponent K L = 0 ↔
      LocalFieldTheory.fieldPrincipalUnits K 0 ≤ localNormSubgroup K L

theorem

localConductorIdeal_eq_one_iff_exponent_eq_zero

L124 ↗

LocalClassFieldTheory.localConductorIdeal_eq_one_iff_exponent_eq_zero

Documentation

The conductor ideal is 1 exactly when its exponent is zero.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem localConductorIdeal_eq_one_iff_exponent_eq_zero
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    localConductorIdeal K L = 1 ↔ localConductorExponent K L = 0

theorem

localConductorIdeal_eq_one_iff

L135 ↗

LocalClassFieldTheory.localConductorIdeal_eq_one_iff

Documentation

The conductor-one criterion stated directly in terms of the norm subgroup and U_K = U_K^(0).

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory

Lean source · statement

theorem localConductorIdeal_eq_one_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    localConductorIdeal K L = 1 ↔
      LocalFieldTheory.fieldPrincipalUnits K 0 ≤ localNormSubgroup K L

Module documentation

Conductors of finite abelian local extensions

Declarations