Module

UniformizerPrincipalQuotient.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.UniformizerPrincipalQuotient

8 declarations indexed from sourceView source ↗

Module documentation

Quotients by a uniformizer and principal units

For a nonarchimedean local field, quotienting the field-unit group by the standard subgroup generated by a normalized uniformizer and U^n is canonically equivalent to quotienting the integer-unit group by U^n.

Imports2

Imported by4

theorem

integerUnitsToFieldUnits_injective

L27 ↗

LocalFieldTheory.integerUnitsToFieldUnits_injective

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem integerUnitsToFieldUnits_injective
    (L : Type*) [Field L] [ValuativeRel L] :
    Function.Injective (integerUnitsToFieldUnits L)

theorem

uniformizerUnitFactor_one

L36 ↗

LocalFieldTheory.uniformizerUnitFactor_one

Documentation

The unit factor associated with a normalized uniformizer sends one to the trivial integer unit.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem uniformizerUnitFactor_one
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1) :
    LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor K pi hpi 1 = 1

theorem

uniformizerUnitFactor_mul

L49 ↗

LocalFieldTheory.uniformizerUnitFactor_mul

Documentation

The unit factor associated with a normalized uniformizer is multiplicative.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem uniformizerUnitFactor_mul
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1)
    (x y : Kˣ) :
    LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor K pi hpi (x * y) =
      LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor K pi hpi x *
        LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor K pi hpi y

theorem

uniformizerUnitFactor_integerUnit

L67 ↗

LocalFieldTheory.uniformizerUnitFactor_integerUnit

Documentation

Extracting the unit factor of an embedded integer unit recovers the original integer unit.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem uniformizerUnitFactor_integerUnit
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1)
    (u : 𝒪[K]ˣ) :
    LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor K pi hpi
        (integerUnitsToFieldUnits K u) = u

def

fieldUnitsToIntegerUnitsPrincipalQuotientHom

L86 ↗

LocalFieldTheory.fieldUnitsToIntegerUnitsPrincipalQuotientHom

Documentation

Extract the unit factor and reduce it modulo the n-th principal-unit subgroup.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

def fieldUnitsToIntegerUnitsPrincipalQuotientHom
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1)
    (n : ℕ) : Kˣ →* IntegerUnitsPrincipalQuot K n where
  toFun x := integerUnitsPrincipalQuotMk K n
    (LocalFieldTheory.IsNonarchimedeanLocalField.uniformizerUnitFactor K pi hpi x)
  map_one' := by rw [uniformizerUnitFactor_one]; exact map_one _
  map_mul' x y := by
    rw [uniformizerUnitFactor_mul]
    exact map_mul _ _ _

theorem

fieldUnitsToIntegerUnitsPrincipalQuotientHom_surjective

L101 ↗

LocalFieldTheory.fieldUnitsToIntegerUnitsPrincipalQuotientHom_surjective

Documentation

Reduction of normalized unit factors modulo principal units is surjective.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem fieldUnitsToIntegerUnitsPrincipalQuotientHom_surjective
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1)
    (n : ℕ) :
    Function.Surjective (fieldUnitsToIntegerUnitsPrincipalQuotientHom K pi hpi n)

theorem

fieldUnitsToIntegerUnitsPrincipalQuotientHom_ker

L118 ↗

LocalFieldTheory.fieldUnitsToIntegerUnitsPrincipalQuotientHom_ker

Documentation

The kernel is generated by the normalized uniformizer together with the n-th field principal-unit subgroup.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem fieldUnitsToIntegerUnitsPrincipalQuotientHom_ker
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1)
    (n : ℕ) :
    MonoidHom.ker (fieldUnitsToIntegerUnitsPrincipalQuotientHom K pi hpi n) =
      uniformizerPrincipalSubgroup K pi 1 n

def

uniformizerPrincipalQuotientEquivIntegerUnitsPrincipalQuotient

L168 ↗

LocalFieldTheory.uniformizerPrincipalQuotientEquivIntegerUnitsPrincipalQuotient

Documentation

Quotienting field units by a normalized uniformizer and U^n is canonically equivalent to quotienting integer units by U^n.

Source context 4 commands

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

open scoped ValuativeRel
namespace LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def uniformizerPrincipalQuotientEquivIntegerUnitsPrincipalQuotient
    (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (pi : Kˣ)
    (hpi : LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K (Additive.ofMul pi) = 1)
    (n : ℕ) :
    Kˣ ⧸ uniformizerPrincipalSubgroup K pi 1 n ≃*
      IntegerUnitsPrincipalQuot K n

Module documentation

Quotients by a uniformizer and principal units

Declarations