Module

Norm.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Unramified.Norm

8 declarations indexed from sourceView source ↗

Module documentation

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.Norm Lean module.

Imports2

Imported by4

theorem

normIntegerUnits_surjective_unramified_of_isIntegralClosure

L28 ↗

LocalClassFieldTheory.normIntegerUnits_surjective_unramified_of_isIntegralClosure

Documentation

For a finite unramified extension, actual integral-closure integer-unit norm surjectivity: combine the quotient norm on 𝒪[L]ˣ/U_L¹ with the actual U_L¹ -> U_K¹ lifting.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem normIntegerUnits_surjective_unramified_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [LocalFieldTheory.ValuativeExtension K L] [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    Function.Surjective (normIntegerUnits K L)

theorem

v_normUnits_integerUnitsToFieldUnits

L81 ↗

LocalClassFieldTheory.v_normUnits_integerUnitsToFieldUnits

Documentation

For a finite unramified extension: the norm of an integer unit is again an integer unit, so its normalized valuation is zero.

This is the unit part of the standard decomposition x = u * π^m; it uses the actual integer-unit norm, not a norm-valuation certificate.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem v_normUnits_integerUnitsToFieldUnits
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [Algebra K L] [LocalFieldTheory.ValuativeExtension K L]
    (u : 𝒪[L]ˣ) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K
      (Additive.ofMul (LocalFieldTheory.normUnits K L
        (integerUnitsToFieldUnits L u))) = 0

theorem

v_normUnits_mapBase_inverseIntegerRingUniformizerFieldUnit_zpow

L100 ↗

LocalClassFieldTheory.v_normUnits_mapBase_inverseIntegerRingUniformizerFieldUnit_zpow

Documentation

The norm of a base-field inverse uniformizer power has the expected valuation. This is the N(π_K^m) = π_K^{m[L:K]} part of the unramified norm calculation, proved from the algebra norm of a base element.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem v_normUnits_mapBase_inverseIntegerRingUniformizerFieldUnit_zpow
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [Algebra K L] (m : Int) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K
      (Additive.ofMul
        (LocalFieldTheory.normUnits K L
          ((mapBaseUnitsToExtensionUnits K L
            (inverseIntegerRingUniformizerFieldUnit K)) ^ m))) =
      (Module.finrank K L : Int) * m

theorem

v_normUnits_integerUnit_mul_mapBase_inverseIntegerRingUniformizer_zpow

L129 ↗

LocalClassFieldTheory.v_normUnits_integerUnit_mul_mapBase_inverseIntegerRingUniformizer_zpow

Documentation

For a finite unramified extension: after decomposing an element into an integer-unit part and a power of the chosen inverse uniformizer, the valuation of its norm is determined by the exponent.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem v_normUnits_integerUnit_mul_mapBase_inverseIntegerRingUniformizer_zpow
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [Algebra K L] [LocalFieldTheory.ValuativeExtension K L]
    (u : 𝒪[L]ˣ) (m : Int) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K
      (Additive.ofMul
        (LocalFieldTheory.normUnits K L
          (integerUnitsToFieldUnits L u *
            (mapBaseUnitsToExtensionUnits K L
              (inverseIntegerRingUniformizerFieldUnit K)) ^ m))) =
      (Module.finrank K L : Int) * m

theorem

v_normUnits_unramifiedValuation

L155 ↗

LocalClassFieldTheory.v_normUnits_unramifiedValuation

Documentation

For a finite unramified extension, norm-valuation calculation in the actual unramified valuation case.

The proof uses the standard decomposition: choose the base inverse uniformizer, use unramifiedness to know that it is also an upstairs normalized generator, decompose x = u * π^{v_L(x)}, then combine the integer-unit norm with N(π^m) = π_K^{m[L:K]}. No common-uniformizer value, norm-valuation formula, or residue-degree equality is assumed as an extra input.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem v_normUnits_unramifiedValuation
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [LocalFieldTheory.ValuativeExtension K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (x : Lˣ) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K
      (Additive.ofMul (LocalFieldTheory.normUnits K L x)) =
      (Module.finrank K L : Int) *
        LocalFieldTheory.IsNonarchimedeanLocalField.v L (Additive.ofMul x)

theorem

finrank_dvd_valuation_of_mem_normSubgroup_unramified

L195 ↗

LocalClassFieldTheory.finrank_dvd_valuation_of_mem_normSubgroup_unramified

Documentation

For a finite unramified extension, reverse containment source: every field norm has valuation divisible by [L : K] in the actual unramified valuation case.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem finrank_dvd_valuation_of_mem_normSubgroup_unramified
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [LocalFieldTheory.ValuativeExtension K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    {x : Kˣ} (hx : x ∈ localNormSubgroup K L) :
    (Module.finrank K L : Int) ∣ valuationMap K (Additive.ofMul x)

theorem

mem_normSubgroup_of_finrank_dvd_valuation_unramified_of_isIntegralClosure

L218 ↗

LocalClassFieldTheory.mem_normSubgroup_of_finrank_dvd_valuation_unramified_of_isIntegralClosure

Documentation

For a finite unramified extension, constructive reverse containment for the unramified norm calculation, actual integral-closure source-producing half: if the valuation of a base-field unit is divisible by [L : K], then it is already a field norm.

This is the standard argument a = u * π_K^(m[L:K]), with u = N(ε) by the actual integer-unit norm theorem and π_K^(m[L:K]) = N(π_K^m). It uses the integral-closure version of the integer-unit lifting, with no auxiliary invariant package.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem mem_normSubgroup_of_finrank_dvd_valuation_unramified_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [LocalFieldTheory.ValuativeExtension K L] [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    {x : Kˣ}
    (hdiv : (Module.finrank K L : Int) ∣ valuationMap K (Additive.ofMul x)) :
    x ∈ localNormSubgroup K L

theorem

mem_normSubgroup_unramifiedValuation_iff_finrank_dvd_valuation_of_isIntegralClosure

L283 ↗

LocalClassFieldTheory.mem_normSubgroup_unramifiedValuation_iff_finrank_dvd_valuation_of_isIntegralClosure

Documentation

For a finite unramified extension, actual unramified norm image membership: the norm subgroup consists exactly of elements whose normalized valuation is divisible by [L : K].

This combines the actual norm-valuation calculation with the actual integral-closure unit lifting.

Source context 6 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem mem_normSubgroup_unramifiedValuation_iff_finrank_dvd_valuation_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [LocalFieldTheory.ValuativeExtension K L] [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (x : Kˣ) :
    x ∈ localNormSubgroup K L ↔
      (Module.finrank K L : Int) ∣ valuationMap K (Additive.ofMul x)

Module documentation

Declarations