NYLL
Module

Filtration.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.Filtration
13 declarations indexed from sourceView source ↗

Module documentation

Principal-unit filtration from a valuation ring

For a complete DVF F, the concrete principal-unit filtration on the unit group of the valuation ring is

U^n = { u | u - 1 ∈ m^n }.

This file turns that definition into the abstract AntitoneSubgroupFiltration used by ramification and norm arguments.

Imports4
Imported by5

Declarations

def

higherPrincipalUnitGroup

L43 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
Documentation

The concrete n-th principal-unit subgroup of the valuation ring unit group.

Source context 9 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · full declaration
def higherPrincipalUnitGroup
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) (n : ℕ) :
    Subgroup F.valuationSubringˣ where
  carrier := {u | (u : F.valuationSubring) - 1 ∈ F.maximalIdeal ^ n}
  one_mem' := by
    simp
  mul_mem' := by
    intro x y hx hy
    have hxy :
        ((x * y : F.valuationSubringˣ) : F.valuationSubring) - 1 =
          (x : F.valuationSubring) * ((y : F.valuationSubring) - 1) +
            ((x : F.valuationSubring) - 1) := by
      simp
      ring
    change ((x * y : F.valuationSubringˣ) : F.valuationSubring) - 1 ∈ F.maximalIdeal ^ n
    rw [hxy]
    exact Ideal.add_mem _ (Ideal.mul_mem_left _ _ hy) hx
  inv_mem' := by
    intro x hx
    have hxinv :
        ((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) - 1 =
            -(((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) *
              ((x : F.valuationSubring) - 1)) := by
      calc
        ((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) - 1 =
            ((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) -
              ((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) *
                (x : F.valuationSubring) := by
          simp
        _ = -(((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) *
              ((x : F.valuationSubring) - 1)) := by
          ring
    change ((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) - 1 ∈ F.maximalIdeal ^ n
    rw [hxinv]
    exact (F.maximalIdeal ^ n).neg_mem
      (Ideal.mul_mem_left (F.maximalIdeal ^ n)
        ((x⁻¹ : F.valuationSubringˣ) : F.valuationSubring) hx)
theorem

mem_iff

L89 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_iff
Documentation

Characterizes u ∈ higherPrincipalUnitGroup F n by the equivalent condition (u : F.valuationSubring) - 1 ∈ F.maximalIdeal ^ n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem mem_iff (n : ℕ) (u : F.valuationSubringˣ) :
    u ∈ higherPrincipalUnitGroup F n ↔
      (u : F.valuationSubring) - 1 ∈ F.maximalIdeal ^ n
theorem

antitone

L95 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.antitone
Documentation

Higher levels are contained in lower levels.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem antitone {m n : ℕ} (h : m ≤ n) :
    higherPrincipalUnitGroup F n ≤ higherPrincipalUnitGroup F m
theorem

one_add_pow_prime_sub_one_mem_pow_succ

L102 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.one_add_pow_prime_sub_one_mem_pow_succ
Documentation

Prime-binomial containment in an ideal. If p ∈ I and a ∈ I^n with n ≥ 1, then (1 + a)^p - 1 is one level deeper.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem one_add_pow_prime_sub_one_mem_pow_succ
    {R : Type*} [CommRing R] (I : Ideal R)
    {p n : ℕ} (hp : Nat.Prime p) (hn : 1 ≤ n)
    (hp_mem : (p : R) ∈ I) {a : R} (ha : a ∈ I ^ n) :
    (1 + a) ^ p - 1 ∈ I ^ (n + 1)
theorem

natCast_mem_maximalIdeal_of_residue_ringChar_eq

L129 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.natCast_mem_maximalIdeal_of_residue_ringChar_eq
Documentation

If the residue field has ring characteristic p, then p lies in the maximal ideal of the valuation ring.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem natCast_mem_maximalIdeal_of_residue_ringChar_eq
    {p : ℕ} (hchar : ringChar F.residueField = p) :
    (p : F.valuationSubring) ∈ F.maximalIdeal
theorem

pow_mem_succ_of_natCast_mem_maximalIdeal

L139 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.pow_mem_succ_of_natCast_mem_maximalIdeal
Documentation

Concrete principal-unit form of the prime-binomial containment: if p ∈ m, then the pth power carries U^n into U^(n+1) for n ≥ 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem pow_mem_succ_of_natCast_mem_maximalIdeal
    {p n : ℕ} (hp : Nat.Prime p) (hn : 1 ≤ n)
    (hp_mem : (p : F.valuationSubring) ∈ F.maximalIdeal)
    {u : F.valuationSubringˣ}
    (hu : u ∈ higherPrincipalUnitGroup F n) :
    u ^ p ∈ higherPrincipalUnitGroup F (n + 1)
theorem

pow_mem_succ_of_residue_ringChar_eq

L161 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.pow_mem_succ_of_residue_ringChar_eq
Documentation

Residue-characteristic form of pow_mem_succ_of_natCast_mem_maximalIdeal: if the residue field has characteristic p, then pth powers move principal units one step deeper.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem pow_mem_succ_of_residue_ringChar_eq
    {p n : ℕ} (hp : Nat.Prime p) (hn : 1 ≤ n)
    (hchar : ringChar F.residueField = p)
    {u : F.valuationSubringˣ}
    (hu : u ∈ higherPrincipalUnitGroup F n) :
    u ^ p ∈ higherPrincipalUnitGroup F (n + 1)
theorem

zero_eq_top

L174 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.zero_eq_top
Documentation

Establishes the identity higherPrincipalUnitGroup F 0 = ⊤.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem zero_eq_top :
    higherPrincipalUnitGroup F 0 = ⊤
def

residueUnitHom

L181 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueUnitHom
Documentation

The residue of a valuation-ring unit, viewed as a unit of the residue field.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def residueUnitHom :
    F.valuationSubringˣ →* F.residueFieldˣ
theorem

residueUnitHom_apply

L189 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueUnitHom_apply
Documentation

The defining evaluation formula for residueUnitHom is ((higherPrincipalUnitGroup.residueUnitHom F u : F.residueFieldˣ) : F.residueField) = F.residueMap (u : F.valuationSubring).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueUnitHom_apply (u : F.valuationSubringˣ) :
    ((higherPrincipalUnitGroup.residueUnitHom F u : F.residueFieldˣ) :
        F.residueField) =
      F.residueMap (u : F.valuationSubring)
theorem

mem_one_iff_residue_eq_one

L197 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_one_iff_residue_eq_one
Documentation

The first concrete principal-unit level consists exactly of units whose residue is 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem mem_one_iff_residue_eq_one (u : F.valuationSubringˣ) :
    u ∈ higherPrincipalUnitGroup F 1 ↔
      F.residueMap (u : F.valuationSubring) = 1
theorem

residueUnitHom_eq_one_iff

L219 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueUnitHom_eq_one_iff
Documentation

Characterizes higherPrincipalUnitGroup.residueUnitHom F u = 1 by the equivalent condition u ∈ higherPrincipalUnitGroup F 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueUnitHom_eq_one_iff (u : F.valuationSubringˣ) :
    higherPrincipalUnitGroup.residueUnitHom F u = 1 ↔
      u ∈ higherPrincipalUnitGroup F 1
theorem

residueUnitHom_eq_iff_residue_eq

L237 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueUnitHom_eq_iff_residue_eq
Documentation

Characterizes higherPrincipalUnitGroup.residueUnitHom F u = higherPrincipalUnitGroup.residueUnitHom F v by the equivalent condition F.residueMap (u : F.valuationSubring) = F.residueMap (v : F.valuationSubring).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueUnitHom_eq_iff_residue_eq
    (u v : F.valuationSubringˣ) :
    higherPrincipalUnitGroup.residueUnitHom F u =
        higherPrincipalUnitGroup.residueUnitHom F v ↔
      F.residueMap (u : F.valuationSubring) =
        F.residueMap (v : F.valuationSubring)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.