Module

UnramifiedNormSubgroup.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.UnramifiedNormSubgroup

26 declarations indexed from sourceView source ↗

Module documentation

Unramified norm subgroups

For a nonarchimedean local field, the norm subgroup of an unramified extension of degree n is characterized by divisibility of the normalized valuation by n. This file packages that subgroup, its quotient map, and the canonical identification of the quotient with ZMod n.

Imports4

Imported by10

def

valuationModDegree

L30 ↗

LocalClassFieldTheory.valuationModDegree

Documentation

The normalized valuation map reduced modulo a positive or zero degree n.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

def valuationModDegree (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    Additive Kˣ →+ ZMod n

theorem

valuationModDegree_apply

L37 ↗

LocalClassFieldTheory.valuationModDegree_apply

Documentation

Evaluates the normalized valuation map after reduction modulo n.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegree_apply (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) (x : Additive Kˣ) :
    valuationModDegree K n x =
      (LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K x : ZMod n)

theorem

valuationModDegree_surjective

L44 ↗

LocalClassFieldTheory.valuationModDegree_surjective

Documentation

The normalized valuation remains surjective after reduction modulo n.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegree_surjective (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    Function.Surjective (valuationModDegree K n)

theorem

valuationModDegree_eq_zero_iff_dvd

L53 ↗

LocalClassFieldTheory.valuationModDegree_eq_zero_iff_dvd

Documentation

A reduced valuation vanishes exactly when n divides the original valuation.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegree_eq_zero_iff_dvd (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) (x : Additive Kˣ) :
    valuationModDegree K n x = 0 ↔
      (n : Int) ∣ LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K x

theorem

valuationModDegree_eq_iff_dvd_sub

L62 ↗

LocalClassFieldTheory.valuationModDegree_eq_iff_dvd_sub

Documentation

Two reduced valuations agree exactly when n divides their difference.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegree_eq_iff_dvd_sub (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) (x y : Additive Kˣ) :
    valuationModDegree K n x = valuationModDegree K n y ↔
      (n : Int) ∣
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K x -
          LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K y

def

valuationModDegreeMulHom

L71 ↗

LocalClassFieldTheory.valuationModDegreeMulHom

Documentation

Multiplicative form of the normalized valuation map modulo a degree.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

def valuationModDegreeMulHom (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    Kˣ →* Multiplicative (ZMod n)

theorem

valuationModDegreeMulHom_apply

L78 ↗

LocalClassFieldTheory.valuationModDegreeMulHom_apply

Documentation

Evaluates the multiplicative form of the valuation-modulo-degree map.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegreeMulHom_apply (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) (x : Kˣ) :
    valuationModDegreeMulHom K n x =
      Multiplicative.ofAdd
        (LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x) : ZMod n)

theorem

valuationModDegreeMulHom_surjective

L86 ↗

LocalClassFieldTheory.valuationModDegreeMulHom_surjective

Documentation

The multiplicative valuation-modulo-degree map is surjective.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegreeMulHom_surjective (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    Function.Surjective (valuationModDegreeMulHom K n)

theorem

valuationModDegreeMulHom_eq_one_iff_dvd

L96 ↗

LocalClassFieldTheory.valuationModDegreeMulHom_eq_one_iff_dvd

Documentation

A unit maps to one exactly when its valuation is divisible by n.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegreeMulHom_eq_one_iff_dvd (K : Type u) [Field K]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x : Kˣ) :
    valuationModDegreeMulHom K n x = 1 ↔
      (n : Int) ∣
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x)

theorem

valuationModDegreeMulHom_eq_iff_dvd_sub

L106 ↗

LocalClassFieldTheory.valuationModDegreeMulHom_eq_iff_dvd_sub

Documentation

Two units have the same image exactly when n divides their valuation difference.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem valuationModDegreeMulHom_eq_iff_dvd_sub (K : Type u) [Field K]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x y : Kˣ) :
    valuationModDegreeMulHom K n x = valuationModDegreeMulHom K n y ↔
      (n : Int) ∣
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x) -
          LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul y)

def

unramifiedNormSubgroup

L119 ↗

LocalClassFieldTheory.unramifiedNormSubgroup

Documentation

The unramified norm subgroup of degree n: field units whose normalized valuation lies in nℤ.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · full declaration

def unramifiedNormSubgroup (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) : Subgroup Kˣ where
  carrier := {x | (n : Int) ∣
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x)}
  one_mem' := by
    change (n : Int) ∣
      LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul (1 : Kˣ))
    rw [show Additive.ofMul (1 : Kˣ) = 0 by rfl, map_zero]
    exact dvd_zero (n : Int)
  mul_mem' := by
    intro x y hx hy
    change (n : Int) ∣
      LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul (x * y))
    rw [show Additive.ofMul (x * y) = Additive.ofMul x + Additive.ofMul y by rfl,
      map_add]
    exact dvd_add hx hy
  inv_mem' := by
    intro x hx
    change (n : Int) ∣
      LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x⁻¹)
    rw [show Additive.ofMul x⁻¹ = -Additive.ofMul x by rfl, map_neg]
    exact dvd_neg.mpr hx

theorem

mem_unramifiedNormSubgroup_iff

L143 ↗

LocalClassFieldTheory.mem_unramifiedNormSubgroup_iff

Documentation

Characterizes the unramified norm subgroup by divisibility of the normalized valuation.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem mem_unramifiedNormSubgroup_iff (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) (x : Kˣ) :
    x ∈ unramifiedNormSubgroup K n ↔
      (n : Int) ∣ LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x)

def

unramifiedNormClass

L150 ↗

LocalClassFieldTheory.unramifiedNormClass

Documentation

The quotient map from field units to degree-n unramified norm classes.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

def unramifiedNormClass (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    Kˣ →* Kˣ ⧸ unramifiedNormSubgroup K n

theorem

unramifiedNormClass_surjective

L156 ↗

LocalClassFieldTheory.unramifiedNormClass_surjective

Documentation

Every unramified norm class is represented by a field unit.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormClass_surjective (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    Function.Surjective (unramifiedNormClass K n)

theorem

unramifiedNormClass_ker

L162 ↗

LocalClassFieldTheory.unramifiedNormClass_ker

Documentation

The kernel of the quotient map is the unramified norm subgroup.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormClass_ker (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Nat) :
    MonoidHom.ker (unramifiedNormClass K n) =
      unramifiedNormSubgroup K n

theorem

unramifiedNormClass_eq_one_iff

L169 ↗

LocalClassFieldTheory.unramifiedNormClass_eq_one_iff

Documentation

A unit has trivial norm class exactly when its valuation is divisible by the degree.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormClass_eq_one_iff (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x : Kˣ) :
    unramifiedNormClass K n x = 1 ↔
      (n : Int) ∣ LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul
        x)

theorem

unramifiedNormClass_eq_one_iff_mem

L179 ↗

LocalClassFieldTheory.unramifiedNormClass_eq_one_iff_mem

Documentation

A unit has trivial norm class exactly when it belongs to the unramified norm subgroup.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormClass_eq_one_iff_mem (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x : Kˣ) :
    unramifiedNormClass K n x = 1 ↔ x ∈ unramifiedNormSubgroup K n

theorem

unramifiedNormSubgroup_eq_ker_valuationModDegreeMulHom

L186 ↗

LocalClassFieldTheory.unramifiedNormSubgroup_eq_ker_valuationModDegreeMulHom

Documentation

The unramified norm subgroup is the kernel of the multiplicative reduced valuation.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormSubgroup_eq_ker_valuationModDegreeMulHom (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) :
    MonoidHom.ker (valuationModDegreeMulHom K n) = unramifiedNormSubgroup K n

theorem

mem_unramifiedNormSubgroup_iff_valuationModDegreeMulHom_eq_one

L195 ↗

LocalClassFieldTheory.mem_unramifiedNormSubgroup_iff_valuationModDegreeMulHom_eq_one

Documentation

Membership in the unramified norm subgroup is detected by the reduced valuation.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem mem_unramifiedNormSubgroup_iff_valuationModDegreeMulHom_eq_one
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) (x : Kˣ) :
    x ∈ unramifiedNormSubgroup K n ↔ valuationModDegreeMulHom K n x = 1

def

unramifiedNormQuotientEquivZMod

L203 ↗

LocalClassFieldTheory.unramifiedNormQuotientEquivZMod

Documentation

The valuation quotient model Kˣ / {x | n ∣ v(x)} ≃ Z/nZ, in multiplicative notation.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

def unramifiedNormQuotientEquivZMod (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) :
    Kˣ ⧸ unramifiedNormSubgroup K n ≃* Multiplicative (ZMod n)

theorem

unramifiedNormQuotientEquivZMod_mk

L214 ↗

LocalClassFieldTheory.unramifiedNormQuotientEquivZMod_mk

Documentation

The quotient equivalence sends a unit class to its valuation modulo the degree.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormQuotientEquivZMod_mk (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x : Kˣ) :
    unramifiedNormQuotientEquivZMod K n (QuotientGroup.mk x) =
      valuationModDegreeMulHom K n x

theorem

unramifiedNormQuotient_cardinal_eq_zmod

L227 ↗

LocalClassFieldTheory.unramifiedNormQuotient_cardinal_eq_zmod

Documentation

Cardinality of the valuation quotient for arbitrary n. This statement remains meaningful at n = 0, when ZMod 0 and the quotient are infinite.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormQuotient_cardinal_eq_zmod (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) :
    Cardinal.mk (Kˣ ⧸ unramifiedNormSubgroup K n) =
      Cardinal.lift (Cardinal.mk (ZMod n))

instance

finiteUnramifiedNormQuotient

L237 ↗

LocalClassFieldTheory.finiteUnramifiedNormQuotient

Documentation

A nonzero valuation modulus gives a finite norm quotient.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

instance finiteUnramifiedNormQuotient (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) [NeZero n] : Finite (Kˣ ⧸ unramifiedNormSubgroup K n)

theorem

unramifiedNormQuotient_card_eq_degree

L244 ↗

LocalClassFieldTheory.unramifiedNormQuotient_card_eq_degree

Documentation

For nonzero degree, the unramified norm quotient has cardinality equal to that degree.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormQuotient_card_eq_degree (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) [NeZero n] :
    Nat.card (Kˣ ⧸ unramifiedNormSubgroup K n) = n

theorem

unramifiedNormClass_eq_iff

L257 ↗

LocalClassFieldTheory.unramifiedNormClass_eq_iff

Documentation

Two units define the same norm class exactly when the degree divides their valuation difference.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormClass_eq_iff (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x y : Kˣ) :
    unramifiedNormClass K n x =
        unramifiedNormClass K n y ↔
      (n : Int) ∣
        LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x) -
          LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul y)

theorem

unramifiedNormQuotientEquivZMod_eq_iff_valuation_sub_eq_zero

L280 ↗

LocalClassFieldTheory.unramifiedNormQuotientEquivZMod_eq_iff_valuation_sub_eq_zero

Documentation

The quotient images agree exactly when the reduced valuation difference vanishes.

Source context 3 commands

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

noncomputable section
universe u
namespace LocalClassFieldTheory

Lean source · statement

theorem unramifiedNormQuotientEquivZMod_eq_iff_valuation_sub_eq_zero (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (n : Nat) (x y : Kˣ) :
    unramifiedNormQuotientEquivZMod K n
        (unramifiedNormClass K n x) =
        unramifiedNormQuotientEquivZMod K n
          (unramifiedNormClass K n y) ↔
      ((LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul x) -
          LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul y) : Int) :
        ZMod n) = 0

Module documentation

Unramified norm subgroups

Declarations