Module

IdealQuotients.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.IdealQuotients

58 declarations indexed from sourceView source ↗

Module documentation

Residue and maximal-ideal successive quotients

Imports2

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.PrincipalUnitQuotients

Imported by13

def

integerRingModMaximalIdealAddEquivResidue

L27 ↗

LocalFieldTheory.integerRingModMaximalIdealAddEquivResidue

Documentation

Additive identification of the residue field with 𝒪[K]/𝓂[K].

This is definitional for mathlib's local-ring residue field, but we expose it as part of the local CFT boundary so later files do not depend on unfolding the residue-field definition.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerRingModMaximalIdealAddEquivResidue
    (K : Type u) [Field K] [ValuativeRel K] :
    (𝒪[K] ⧸ (𝓂[K] : Ideal 𝒪[K])) ≃+ 𝓀[K]

theorem

integerRingModMaximalIdealAddEquivResidue_mk

L35 ↗

LocalFieldTheory.integerRingModMaximalIdealAddEquivResidue_mk

Documentation

The additive equivalence from the integer ring modulo its maximal ideal sends a representative to its residue class.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingModMaximalIdealAddEquivResidue_mk
    (K : Type u) [Field K] [ValuativeRel K] (x : 𝒪[K]) :
    integerRingModMaximalIdealAddEquivResidue K
        (Ideal.Quotient.mk (𝓂[K] : Ideal 𝒪[K]) x) =
      IsLocalRing.residue 𝒪[K] x

theorem

residue_eq_zero_iff_mem_maximalIdeal

L43 ↗

LocalFieldTheory.residue_eq_zero_iff_mem_maximalIdeal

Documentation

An integer-ring element has zero residue exactly when it belongs to the maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residue_eq_zero_iff_mem_maximalIdeal
    (K : Type u) [Field K] [ValuativeRel K] (x : 𝒪[K]) :
    IsLocalRing.residue 𝒪[K] x = 0 ↔ x ∈ (𝓂[K] : Ideal 𝒪[K])

def

chosenIntegerRingUniformizer

L50 ↗

LocalFieldTheory.chosenIntegerRingUniformizer

Documentation

A chosen DVR uniformizer of the valuation ring of a nonarchimedean local field, viewed as an irreducible element of 𝒪[K].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def chosenIntegerRingUniformizer
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : 𝒪[K]

theorem

chosenIntegerRingUniformizer_irreducible

L56 ↗

LocalFieldTheory.chosenIntegerRingUniformizer_irreducible

Documentation

The chosen integer-ring uniformizer is irreducible in the discrete valuation ring.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem chosenIntegerRingUniformizer_irreducible
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Irreducible (chosenIntegerRingUniformizer K)

theorem

chosenIntegerRingUniformizer_maximalIdeal_eq

L63 ↗

LocalFieldTheory.chosenIntegerRingUniformizer_maximalIdeal_eq

Documentation

The maximal ideal is the principal ideal generated by the chosen integer-ring uniformizer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem chosenIntegerRingUniformizer_maximalIdeal_eq
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (𝓂[K] : Ideal 𝒪[K]) = Ideal.span ({chosenIntegerRingUniformizer K} : Set 𝒪[K])

def

integerRingUniformizerFieldUnit

L74 ↗

LocalFieldTheory.integerRingUniformizerFieldUnit

Documentation

The chosen DVR uniformizer of 𝒪[K], viewed as a nonzero field unit.

This is the source object for the local class-field decomposition by powers of a prime element. Valuation normalization is proved separately; it is not an extra argument of this definition.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerRingUniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Kˣ

theorem

integerRingUniformizerFieldUnit_coe

L84 ↗

LocalFieldTheory.integerRingUniformizerFieldUnit_coe

Documentation

The field unit associated to the chosen integer-ring uniformizer has the same underlying field element.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingUniformizerFieldUnit_coe
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ((integerRingUniformizerFieldUnit K : Kˣ) : K) =
      (((chosenIntegerRingUniformizer K : 𝒪[K]) : K))

def

inverseIntegerRingUniformizerFieldUnit

L96 ↗

LocalFieldTheory.inverseIntegerRingUniformizerFieldUnit

Documentation

The inverse of the chosen DVR uniformizer, as a field unit.

With the normalized additive valuation used by valuationMap, this is the element expected to have value 1. The proof of that normalization is the next source-producing frontier.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def inverseIntegerRingUniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Kˣ

theorem

inverseIntegerRingUniformizerFieldUnit_coe

L103 ↗

LocalFieldTheory.inverseIntegerRingUniformizerFieldUnit_coe

Documentation

The inverse uniformizer field unit coerces to the inverse of the chosen uniformizer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem inverseIntegerRingUniformizerFieldUnit_coe
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ((inverseIntegerRingUniformizerFieldUnit K : Kˣ) : K) =
      (((chosenIntegerRingUniformizer K : 𝒪[K]) : K))⁻¹

lemma

withZeroMultiplicativeInt_le_of_lt_one

L110 ↗

LocalFieldTheory.withZeroMultiplicativeInt_le_of_lt_one

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

lemma withZeroMultiplicativeInt_le_of_lt_one
    (δ : WithZero (Multiplicative Int)) (hδ : δ < 1) :
    δ ≤ ((Multiplicative.ofAdd (-1 : Int) : Multiplicative Int) :
      WithZero (Multiplicative Int))

lemma

withZeroMultiplicativeInt_maximal_lt_one_eq_ofAdd_neg_one

L127 ↗

LocalFieldTheory.withZeroMultiplicativeInt_maximal_lt_one_eq_ofAdd_neg_one

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

lemma withZeroMultiplicativeInt_maximal_lt_one_eq_ofAdd_neg_one
    {a : WithZero (Multiplicative Int)} (ha : a < 1)
    (hmax : ∀ δ : WithZero (Multiplicative Int), δ < 1 → δ ≤ a) :
    a = ((Multiplicative.ofAdd (-1 : Int) : Multiplicative Int) :
      WithZero (Multiplicative Int))

theorem

valueGroupWithZeroIsoInt_eq_of_maximal_lt_one

L139 ↗

LocalFieldTheory.valueGroupWithZeroIsoInt_eq_of_maximal_lt_one

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem valueGroupWithZeroIsoInt_eq_of_maximal_lt_one
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {a : ValuativeRel.ValueGroupWithZero K} (ha : a < 1)
    (hmax : ∀ δ : ValuativeRel.ValueGroupWithZero K, δ < 1 → δ ≤ a) :
    IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K a =
      ((Multiplicative.ofAdd (-1 : Int) : Multiplicative Int) :
        WithZero (Multiplicative Int))

theorem

valueGroupWithZeroIsoInt_of_integerRing_irreducible

L166 ↗

LocalFieldTheory.valueGroupWithZeroIsoInt_of_integerRing_irreducible

Documentation

any prime element of the valuation ring has multiplicative value ofAdd (-1) under the local-field normalization.

The proof is the DVR argument used in this construction: 𝓂 = (ϖ), so every valuation value below 1 is bounded by the value of ϖ; in the normalized value group this maximal element below 1 is ofAdd (-1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem valueGroupWithZeroIsoInt_of_integerRing_irreducible
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ) :
    IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K
        (ValuativeRel.valuation K ((ϖ : 𝒪[K]) : K)) =
      ((Multiplicative.ofAdd (-1 : Int) : Multiplicative Int) :
        WithZero (Multiplicative Int))

theorem

v_integerRingIrreducibleFieldUnit

L212 ↗

LocalFieldTheory.v_integerRingIrreducibleFieldUnit

Documentation

A field unit whose value is represented by a valuation-ring prime element has normalized additive value -1.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem v_integerRingIrreducibleFieldUnit
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (u : Kˣ) (hu : (u : K) = ((ϖ : 𝒪[K]) : K)) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K (Additive.ofMul u) = -1

theorem

v_integerRingIrreducibleFieldUnit_inv

L237 ↗

LocalFieldTheory.v_integerRingIrreducibleFieldUnit_inv

Documentation

The inverse of a field unit represented by a valuation-ring prime element has normalized additive value 1.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem v_integerRingIrreducibleFieldUnit_inv
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (u : Kˣ) (hu : (u : K) = ((ϖ : 𝒪[K]) : K)) :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K (Additive.ofMul u⁻¹) = 1

theorem

valueGroupWithZeroIsoInt_chosenIntegerRingUniformizer

L252 ↗

LocalFieldTheory.valueGroupWithZeroIsoInt_chosenIntegerRingUniformizer

Documentation

The chosen prime element of the valuation ring has multiplicative value ofAdd (-1) under the local-field normalization.

This is the source-producing normalization for the later decomposition x = u * π^m; it is proved from the DVR fact 𝓂 = (π), not assumed as a separate uniformizer-value input.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem valueGroupWithZeroIsoInt_chosenIntegerRingUniformizer
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K
        (ValuativeRel.valuation K ((chosenIntegerRingUniformizer K : 𝒪[K]) : K)) =
      ((Multiplicative.ofAdd (-1 : Int) : Multiplicative Int) :
        WithZero (Multiplicative Int))

theorem

v_integerRingUniformizerFieldUnit

L265 ↗

LocalFieldTheory.v_integerRingUniformizerFieldUnit

Documentation

The chosen valuation-ring prime element has normalized additive value -1 as a field unit. We use the inverse convention for a positive uniformizer in the exact sequence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem v_integerRingUniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K
      (Additive.ofMul (integerRingUniformizerFieldUnit K)) = -1

theorem

v_inverseIntegerRingUniformizerFieldUnit

L277 ↗

LocalFieldTheory.v_inverseIntegerRingUniformizerFieldUnit

Documentation

The inverse of the chosen valuation-ring prime element has normalized additive value 1. This is the source object needed before using powers of a uniformizer in the local class-field calculation.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem v_inverseIntegerRingUniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    LocalFieldTheory.IsNonarchimedeanLocalField.v K
      (Additive.ofMul (inverseIntegerRingUniformizerFieldUnit K)) = 1

theorem

exists_chosenIntegerRingUniformizer_pow_mul_mem_integerRing

L294 ↗

LocalFieldTheory.exists_chosenIntegerRingUniformizer_pow_mul_mem_integerRing

Documentation

Denominator clearing in the valuation ring: every element of K becomes integral after multiplying by a sufficiently high power of the chosen prime element of 𝒪[K].

This local-DVR denominator-clearing theorem supports normal-basis lattice bounds; the proof uses the fraction representation over 𝒪[K] and the DVR factorization of the denominator into a unit times a power of the prime element.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem exists_chosenIntegerRingUniformizer_pow_mul_mem_integerRing
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : K) :
    ∃ n : Nat,
      (((chosenIntegerRingUniformizer K : 𝒪[K]) : K) ^ n) * x ∈ 𝒪[K]

theorem

maximalIdeal_pow_eq_span_uniformizer_pow_of_irreducible

L346 ↗

LocalFieldTheory.maximalIdeal_pow_eq_span_uniformizer_pow_of_irreducible

Documentation

If a uniformizer is irreducible, each maximal-ideal power is generated by the corresponding power of that uniformizer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdeal_pow_eq_span_uniformizer_pow_of_irreducible
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ) (n : Nat) :
    (𝓂[K] ^ n : Ideal 𝒪[K]) = Ideal.span ({ϖ ^ n} : Set 𝒪[K])

theorem

maximalIdeal_pow_eq_span_uniformizer_pow

L353 ↗

LocalFieldTheory.maximalIdeal_pow_eq_span_uniformizer_pow

Documentation

Each power of the maximal ideal is generated by the matching power of the chosen uniformizer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdeal_pow_eq_span_uniformizer_pow
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    (𝓂[K] ^ n : Ideal 𝒪[K]) =
      Ideal.span ({chosenIntegerRingUniformizer K ^ n} : Set 𝒪[K])

theorem

mul_uniformizer_pow_mem_maximalIdeal_pow

L363 ↗

LocalFieldTheory.mul_uniformizer_pow_mem_maximalIdeal_pow

Documentation

Multiplying an integer by the n-th uniformizer power places it in the n-th maximal-ideal power.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem mul_uniformizer_pow_mem_maximalIdeal_pow
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (r : 𝒪[K]) :
    r * ϖ ^ n ∈ (𝓂[K] ^ n : Ideal 𝒪[K])

theorem

mul_uniformizer_pow_mem_maximalIdeal_pow_succ_iff

L374 ↗

LocalFieldTheory.mul_uniformizer_pow_mem_maximalIdeal_pow_succ_iff

Documentation

A multiple of the n-th uniformizer power lies in the next ideal power exactly when its coefficient lies in the maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem mul_uniformizer_pow_mem_maximalIdeal_pow_succ_iff
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (r : 𝒪[K]) :
    r * ϖ ^ n ∈ (𝓂[K] ^ (n + 1) : Ideal 𝒪[K]) ↔
      r ∈ (𝓂[K] : Ideal 𝒪[K])

def

maximalIdealPowMulUniformizerPowMap

L400 ↗

LocalFieldTheory.maximalIdealPowMulUniformizerPowMap

Documentation

Multiplication by ϖ^n, landing in the ideal 𝓂^n.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def maximalIdealPowMulUniformizerPowMap
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) :
    𝒪[K] →ₗ[𝒪[K]] ((𝓂[K] ^ n : Ideal 𝒪[K]) : Type u) where
  toFun r := ⟨r * ϖ ^ n, mul_uniformizer_pow_mem_maximalIdeal_pow K ϖ hϖ n r⟩
  map_add' r s := by
    ext
    simp [add_mul]
  map_smul' a r := by
    ext
    simp [mul_assoc]

theorem

maximalIdealPowMulUniformizerPowMap_apply

L416 ↗

LocalFieldTheory.maximalIdealPowMulUniformizerPowMap_apply

Documentation

The map into a maximal-ideal power multiplies its input by the corresponding uniformizer power. The map into a maximal-ideal power multiplies its input by the corresponding uniformizer power.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowMulUniformizerPowMap_apply
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (r : 𝒪[K]) :
    (maximalIdealPowMulUniformizerPowMap K ϖ hϖ n r : 𝒪[K]) =
      r * ϖ ^ n

def

maximalIdealPowSuccQuotMulUniformizerPowMap

L425 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMulUniformizerPowMap

Documentation

The map 𝒪[K] → 𝓂^n/𝓂^(n+1) induced by multiplication by ϖ^n.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def maximalIdealPowSuccQuotMulUniformizerPowMap
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) :
    𝒪[K] →ₗ[𝒪[K]] MaximalIdealPowSuccQuot K n

theorem

maximalIdealPowSuccQuotMulUniformizerPowMap_apply

L436 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMulUniformizerPowMap_apply

Documentation

On successive ideal quotients, multiplication by a uniformizer power sends a residue representative to its ideal-quotient class.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMulUniformizerPowMap_apply
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (r : 𝒪[K]) :
    maximalIdealPowSuccQuotMulUniformizerPowMap K ϖ hϖ n r =
      maximalIdealPowSuccQuotMk K n
        (maximalIdealPowMulUniformizerPowMap K ϖ hϖ n r)

theorem

maximalIdealPowSuccQuotMulUniformizerPowMap_ker

L446 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMulUniformizerPowMap_ker

Documentation

The kernel of multiplication into a successive ideal quotient is the maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMulUniformizerPowMap_ker
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) :
    LinearMap.ker (maximalIdealPowSuccQuotMulUniformizerPowMap K ϖ hϖ n) =
      (𝓂[K] : Ideal 𝒪[K])

theorem

maximalIdealPowSuccQuotMulUniformizerPowMap_surjective

L464 ↗

LocalFieldTheory.maximalIdealPowSuccQuotMulUniformizerPowMap_surjective

Documentation

Every class in a successive maximal-ideal quotient is represented by a uniformizer power times an integer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuotMulUniformizerPowMap_surjective
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) :
    Function.Surjective (maximalIdealPowSuccQuotMulUniformizerPowMap K ϖ hϖ n)

def

residueLinearEquivMaximalIdealPowSuccQuotOfIrreducible

L489 ↗

LocalFieldTheory.residueLinearEquivMaximalIdealPowSuccQuotOfIrreducible

Documentation

The DVR comparison 𝒪[K]/𝓂[K] ≃ 𝓂^n/𝓂^(n+1) attached to an irreducible uniformizer ϖ.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def residueLinearEquivMaximalIdealPowSuccQuotOfIrreducible
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) :
    𝓀[K] ≃ₗ[𝒪[K]] MaximalIdealPowSuccQuot K n

def

residueAddEquivMaximalIdealPowSuccQuotOfIrreducible

L501 ↗

LocalFieldTheory.residueAddEquivMaximalIdealPowSuccQuotOfIrreducible

Documentation

Additive form of 𝒪[K]/𝓂[K] ≃ 𝓂^n/𝓂^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def residueAddEquivMaximalIdealPowSuccQuotOfIrreducible
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) :
    𝓀[K] ≃+ MaximalIdealPowSuccQuot K n

theorem

residueAddEquivMaximalIdealPowSuccQuotOfIrreducible_residue

L511 ↗

LocalFieldTheory.residueAddEquivMaximalIdealPowSuccQuotOfIrreducible_residue

Documentation

The residue-to-ideal-quotient equivalence sends a residue class to the class of its lift times the uniformizer power.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueAddEquivMaximalIdealPowSuccQuotOfIrreducible_residue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (r : 𝒪[K]) :
    residueAddEquivMaximalIdealPowSuccQuotOfIrreducible K ϖ hϖ n
        (IsLocalRing.residue 𝒪[K] r) =
    maximalIdealPowSuccQuotMulUniformizerPowMap K ϖ hϖ n r

def

chosenResidueLinearEquivMaximalIdealPowSuccQuot

L538 ↗

LocalFieldTheory.chosenResidueLinearEquivMaximalIdealPowSuccQuot

Documentation

The version of 𝒪[K]/𝓂[K] ≃ 𝓂^n/𝓂^(n+1) determined by the library's chosen integer-ring uniformizer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def chosenResidueLinearEquivMaximalIdealPowSuccQuot
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    𝓀[K] ≃ₗ[𝒪[K]] MaximalIdealPowSuccQuot K n

def

chosenResidueAddEquivMaximalIdealPowSuccQuot

L547 ↗

LocalFieldTheory.chosenResidueAddEquivMaximalIdealPowSuccQuot

Documentation

Additive equivalence determined by the library's chosen integer-ring uniformizer.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def chosenResidueAddEquivMaximalIdealPowSuccQuot
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    𝓀[K] ≃+ MaximalIdealPowSuccQuot K n

instance

maximalIdealPowSuccQuot_finite

L554 ↗

LocalFieldTheory.maximalIdealPowSuccQuot_finite

Documentation

A successive maximal-ideal quotient over a local field is finite.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

instance maximalIdealPowSuccQuot_finite
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    Finite (MaximalIdealPowSuccQuot K n)

theorem

maximalIdealPowSuccQuot_card_eq_residue

L561 ↗

LocalFieldTheory.maximalIdealPowSuccQuot_card_eq_residue

Documentation

Every successive maximal-ideal quotient has the same cardinality as the residue field.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdealPowSuccQuot_card_eq_residue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    Nat.card (MaximalIdealPowSuccQuot K n) = Nat.card 𝓀[K]

def

principalUnitsSuccQuotAddEquivResidue

L570 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivResidue

Documentation

The unit-quotient coordinate theorem in additive form: U^n/U^(n+1) ≃ 𝓀[K], for n ≥ 1.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def principalUnitsSuccQuotAddEquivResidue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) (hn : 1 ≤ n) :
    Additive (PrincipalUnitsSuccQuot K n) ≃+ 𝓀[K]

def

principalUnitsSuccQuotAddEquivResidueOfIrreducible

L581 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivResidueOfIrreducible

Documentation

The unit-quotient coordinate theorem in additive form, using a specified irreducible uniformizer. This avoids the independent canonical-uniformizer choice when comparing an unramified extension with the image of a base uniformizer upstairs.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def principalUnitsSuccQuotAddEquivResidueOfIrreducible
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) :
    Additive (PrincipalUnitsSuccQuot K n) ≃+ 𝓀[K]

theorem

principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_apply

L592 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_apply

Documentation

The inverse residue equivalence extracts the residue coordinate of a successive principal-unit class.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_apply
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (x : 𝓀[K]) :
    (principalUnitsSuccQuotAddEquivResidueOfIrreducible K ϖ hϖ n hn).symm x =
      principalUnitsSuccQuotOfMaximalIdealPowSuccQuotAdd K n hn
        (residueAddEquivMaximalIdealPowSuccQuotOfIrreducible K ϖ hϖ n x)

theorem

principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_residue

L604 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_residue

Documentation

Applying the inverse principal-unit quotient equivalence to a residue representative recovers that residue.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_residue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    (principalUnitsSuccQuotAddEquivResidueOfIrreducible K ϖ hϖ n hn).symm
        (IsLocalRing.residue 𝒪[K] r) =
      Additive.ofMul
        (principalUnitsSuccQuotMk K n
          (principalUnitOneAddOfMemPowSubgroup K hn
            ((maximalIdealPowMulUniformizerPowMap K ϖ hϖ n r :
              (𝓂[K] ^ n : Ideal 𝒪[K])) : 𝒪[K])
            (maximalIdealPowMulUniformizerPowMap K ϖ hϖ n r).2))

def

principalUnitsSuccQuotUniformizerCoord

L627 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord

Documentation

The class of 1 + rϖ^n in U^n/U^(n+1), for a DVR uniformizer ϖ.

This is the concrete coordinate used in the unit-quotient coordinate theorem: successive principal-unit quotients are residue-field additive quotients.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def principalUnitsSuccQuotUniformizerCoord
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    PrincipalUnitsSuccQuot K n

theorem

principalUnitsSuccQuotUniformizerCoord_zero

L640 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord_zero

Documentation

The zero coordinate gives the trivial class in U^n/U^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoord_zero
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) :
    principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn 0 = 1

theorem

principalUnitsSuccQuotUniformizerCoord_add

L653 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord_add

Documentation

Uniformizer coordinates add as expected in the successive principal-unit quotient: 1 + (r+s)ϖ^n and (1+rϖ^n)(1+sϖ^n) have the same class modulo U^(n+1).

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoord_add
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r s : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn (r + s) =
      principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r *
        principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn s

def

principalUnitsSuccQuotUniformizerCoordAddHom

L673 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoordAddHom

Documentation

Additive homomorphism form of the uniformizer coordinate r ↦ [1 + rϖ^n] into the successive principal-unit quotient.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def principalUnitsSuccQuotUniformizerCoordAddHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) :
    𝒪[K] →+ Additive (PrincipalUnitsSuccQuot K n) where
  toFun r := Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r)
  map_zero' := by
    change Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn 0) = 0
    rw [principalUnitsSuccQuotUniformizerCoord_zero]
    rfl
  map_add' r s := by
    change Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn (r + s)) =
      Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r) +
        Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn s)
    rw [principalUnitsSuccQuotUniformizerCoord_add]
    rfl

theorem

principalUnitsSuccQuotUniformizerCoordAddHom_apply

L693 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoordAddHom_apply

Documentation

The uniformizer-coordinate homomorphism sends a principal-unit class to its residue-field coordinate.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoordAddHom_apply
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoordAddHom K ϖ hϖ n hn r =
      Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r)

theorem

principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_residue_coord

L703 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_residue_coord

Documentation

The inverse of the additive equivalence U^n/U^(n+1) ≃ 𝓀[K] sends the residue of r to the uniformizer coordinate class [1 + rϖ^n].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotAddEquivResidueOfIrreducible_symm_residue_coord
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    (principalUnitsSuccQuotAddEquivResidueOfIrreducible K ϖ hϖ n hn).symm
        (IsLocalRing.residue 𝒪[K] r) =
      Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r)

theorem

principalUnitsSuccQuotAddEquivResidueOfIrreducible_coord

L715 ↗

LocalFieldTheory.principalUnitsSuccQuotAddEquivResidueOfIrreducible_coord

Documentation

The additive equivalence U^n/U^(n+1) ≃ 𝓀[K] sends the uniformizer coordinate class [1 + rϖ^n] to the residue of r.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotAddEquivResidueOfIrreducible_coord
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    principalUnitsSuccQuotAddEquivResidueOfIrreducible K ϖ hϖ n hn
        (Additive.ofMul (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r)) =
      IsLocalRing.residue 𝒪[K] r

theorem

principalUnitsSuccQuotUniformizerCoordAddHom_eq_symm_residue

L736 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoordAddHom_eq_symm_residue

Documentation

The coordinate homomorphism factors through reduction to the residue field, pointwise.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoordAddHom_eq_symm_residue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoordAddHom K ϖ hϖ n hn r =
      (principalUnitsSuccQuotAddEquivResidueOfIrreducible K ϖ hϖ n hn).symm
        (IsLocalRing.residue 𝒪[K] r)

theorem

principalUnitsSuccQuotUniformizerCoordAddHom_eq_symm_comp_residue

L749 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoordAddHom_eq_symm_comp_residue

Documentation

The coordinate homomorphism is the composite of residue reduction and the inverse of the additive equivalence U^n/U^(n+1) ≃ 𝓀[K].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoordAddHom_eq_symm_comp_residue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) :
    principalUnitsSuccQuotUniformizerCoordAddHom K ϖ hϖ n hn =
      (principalUnitsSuccQuotAddEquivResidueOfIrreducible K ϖ hϖ n hn).symm.toAddMonoidHom.comp
        (IsLocalRing.residue 𝒪[K]).toAddMonoidHom

theorem

principalUnitsSuccQuotUniformizerCoordAddHom_surjective

L761 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoordAddHom_surjective

Documentation

Every class in U^n/U^(n+1) has a uniformizer-coordinate representative [1 + rϖ^n], in additive homomorphism form.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoordAddHom_surjective
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) :
    Function.Surjective (principalUnitsSuccQuotUniformizerCoordAddHom K ϖ hϖ n hn)

theorem

principalUnitsSuccQuotUniformizerCoord_surjective

L778 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord_surjective

Documentation

Every class in U^n/U^(n+1) has a uniformizer-coordinate representative [1 + rϖ^n].

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoord_surjective
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) :
    Function.Surjective (principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn)

theorem

principalUnitsSuccQuotUniformizerCoord_eq_iff_residue_eq

L794 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord_eq_iff_residue_eq

Documentation

In uniformizer coordinates, equality in U^n/U^(n+1) is exactly equality of residues of the coefficients.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoord_eq_iff_residue_eq
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r s : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r =
        principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn s ↔
      IsLocalRing.residue 𝒪[K] r = IsLocalRing.residue 𝒪[K] s

theorem

principalUnitsSuccQuotUniformizerCoord_eq_one_iff_residue_eq_zero

L845 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord_eq_one_iff_residue_eq_zero

Documentation

In uniformizer coordinates, the class of 1 + rϖ^n is trivial exactly when the coefficient has zero residue.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoord_eq_one_iff_residue_eq_zero
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r = 1 ↔
      IsLocalRing.residue 𝒪[K] r = 0

theorem

principalUnitsSuccQuotUniformizerCoord_eq_one_iff_mem_maximalIdeal

L862 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoord_eq_one_iff_mem_maximalIdeal

Documentation

In uniformizer coordinates, the class [1 + rϖ^n] is trivial exactly when the coefficient lies in the maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoord_eq_one_iff_mem_maximalIdeal
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoord K ϖ hϖ n hn r = 1 ↔
      r ∈ (𝓂[K] : Ideal 𝒪[K])

theorem

principalUnitsSuccQuotUniformizerCoordAddHom_eq_zero_iff_mem_maximalIdeal

L873 ↗

LocalFieldTheory.principalUnitsSuccQuotUniformizerCoordAddHom_eq_zero_iff_mem_maximalIdeal

Documentation

Kernel criterion for the additive uniformizer-coordinate homomorphism: r ↦ [1 + rϖ^n] kills exactly the maximal ideal.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotUniformizerCoordAddHom_eq_zero_iff_mem_maximalIdeal
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (ϖ : 𝒪[K]) (hϖ : Irreducible ϖ)
    (n : Nat) (hn : 1 ≤ n) (r : 𝒪[K]) :
    principalUnitsSuccQuotUniformizerCoordAddHom K ϖ hϖ n hn r = 0 ↔
      r ∈ (𝓂[K] : Ideal 𝒪[K])

theorem

principalUnitsSuccQuot_card_eq_residue

L898 ↗

LocalFieldTheory.principalUnitsSuccQuot_card_eq_residue

Documentation

Every successive principal-unit quotient has cardinality equal to that of the residue field.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuot_card_eq_residue
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) (hn : 1 ≤ n)
    [Finite (PrincipalUnitsSuccQuot K n)] :
    Nat.card (PrincipalUnitsSuccQuot K n) = Nat.card 𝓀[K]

theorem

finite_principalUnitsSuccQuot

L907 ↗

LocalFieldTheory.finite_principalUnitsSuccQuot

Documentation

Successive principal-unit quotients over a local field are finite.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem finite_principalUnitsSuccQuot
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) (hn : 1 ≤ n) :
    Finite (PrincipalUnitsSuccQuot K n)

Module documentation

Residue and maximal-ideal successive quotients

Declarations