Module

Basic.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic

55 declarations indexed from sourceView source ↗

Module documentation

Discretely valued fields

This is the basic one-dimensional API for fields equipped with a chosen rank-one discrete valuation.

Successive quotients of powers of the maximal ideal

Imports4

Mathlib.Algebra.CharP.Subring
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.Valuation.Discrete.Basic
Mathlib.RingTheory.Valuation.LocalSubring

Imported by17

instance

charP

L28 ↗

ValuationTheory.ValuationSubring.charP

Documentation

A valuation subring has the characteristic of its ambient field.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace ValuationSubring

Lean source · statement

instance charP {K : Type u} [Field K] (R : ValuationSubring K) (p : ℕ) [CharP K p] :
    CharP R p

structure

DVF

L37 ↗

ValuationTheory.DiscreteValuationField.DVF

Documentation

A field with a chosen rank-one discrete valuation.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · full declaration

structure DVF (K : Type u) [Field K] where
  /-- The ordered multiplicative value group. -/
  ValueGroup : Type v
  /-- The ordered commutative group-with-zero structure on the value group. -/
  [instValueGroup : LinearOrderedCommGroupWithZero ValueGroup]
  /-- The chosen valuation on the field. -/
  valuation : _root_.Valuation K ValueGroup
  /-- The chosen valuation has discrete rank one. -/
  [instRankOneDiscrete : valuation.IsRankOneDiscrete]

abbrev

valuationSubring

L54 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring

Documentation

The valuation subring of a DVF.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev valuationSubring (F : DVF.{u, v} K) : Type u

instance

commRing

L58 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring.commRing

Documentation

The valuation subring of a discrete valuation field is a commutative ring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

instance valuationSubring.commRing (F : DVF.{u, v} K) :
    CommRing F.valuationSubring

instance

isLocalRing

L63 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring.isLocalRing

Documentation

The valuation subring of a discrete valuation field is local.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

instance valuationSubring.isLocalRing (F : DVF.{u, v} K) :
    IsLocalRing F.valuationSubring

instance

isDomain

L68 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring.isDomain

Documentation

The valuation subring of a discrete valuation field is an integral domain.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

instance valuationSubring.isDomain (F : DVF.{u, v} K) :
    IsDomain F.valuationSubring

abbrev

maximalIdeal

L73 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdeal

Documentation

The maximal ideal of the valuation subring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev maximalIdeal (F : DVF.{u, v} K) : Ideal F.valuationSubring

abbrev

residueField

L77 ↗

ValuationTheory.DiscreteValuationField.DVF.residueField

Documentation

The residue field of the valuation subring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev residueField (F : DVF.{u, v} K) : Type u

instance

field

L81 ↗

ValuationTheory.DiscreteValuationField.DVF.residueField.field

Documentation

The residue ring of a discrete valuation field carries its canonical field structure.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

instance residueField.field (F : DVF.{u, v} K) : Field F.residueField

abbrev

residueMap

L85 ↗

ValuationTheory.DiscreteValuationField.DVF.residueMap

Documentation

The residue map of a DVF.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev residueMap (F : DVF.{u, v} K) :
    RingHom F.valuationSubring F.residueField

theorem

valuationSubring_isDiscreteValuationRing

L90 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring_isDiscreteValuationRing

Documentation

The valuation subring of a DVF is a DVR.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem valuationSubring_isDiscreteValuationRing (F : DVF.{u, v} K) :
    IsDiscreteValuationRing F.valuationSubring

theorem

valuationSubring_isFractionRing

L95 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring_isFractionRing

Documentation

The valuation ring of a DVF is a fraction ring inside the field.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem valuationSubring_isFractionRing (F : DVF.{u, v} K) :
    IsFractionRing F.valuationSubring K

theorem

valuationSubring_isIntegrallyClosed

L100 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring_isIntegrallyClosed

Documentation

The valuation ring of a DVF is integrally closed.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem valuationSubring_isIntegrallyClosed (F : DVF.{u, v} K) :
    IsIntegrallyClosed F.valuationSubring

theorem

valuationSubring_isNoetherianRing

L106 ↗

ValuationTheory.DiscreteValuationField.DVF.valuationSubring_isNoetherianRing

Documentation

The valuation ring of a DVF is Noetherian.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem valuationSubring_isNoetherianRing (F : DVF.{u, v} K) :
    IsNoetherianRing F.valuationSubring

theorem

mem_valuationSubring_iff

L113 ↗

ValuationTheory.DiscreteValuationField.DVF.mem_valuationSubring_iff

Documentation

Membership in the valuation subring is v x <= 1.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem mem_valuationSubring_iff (F : DVF.{u, v} K) (x : K) :
    x ∈ F.valuation.valuationSubring ↔ F.valuation x <= 1

theorem

mem_maximalIdeal_iff

L118 ↗

ValuationTheory.DiscreteValuationField.DVF.mem_maximalIdeal_iff

Documentation

Maximal-ideal membership is v x < 1.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem mem_maximalIdeal_iff (F : DVF.{u, v} K)
    (x : F.valuationSubring) :
    x ∈ F.maximalIdeal ↔ F.valuation (x : K) < 1

theorem

residue_eq_zero_iff

L127 ↗

ValuationTheory.DiscreteValuationField.DVF.residue_eq_zero_iff

Documentation

Zero residue is equivalent to membership in the maximal ideal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem residue_eq_zero_iff (F : DVF.{u, v} K)
    (x : F.valuationSubring) :
    F.residueMap x = 0 ↔ x ∈ F.maximalIdeal

theorem

residue_ne_zero_iff_isUnit

L137 ↗

ValuationTheory.DiscreteValuationField.DVF.residue_ne_zero_iff_isUnit

Documentation

A residue class in a DVF valuation ring is nonzero exactly when its representative is a unit of the valuation ring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem residue_ne_zero_iff_isUnit (F : DVF.{u, v} K)
    (x : F.valuationSubring) :
    F.residueMap x ≠ 0 ↔ IsUnit x

theorem

residue_surjective

L144 ↗

ValuationTheory.DiscreteValuationField.DVF.residue_surjective

Documentation

The residue map is surjective.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem residue_surjective (F : DVF.{u, v} K) :
    Function.Surjective F.residueMap

theorem

exists_uniformizer

L149 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_uniformizer

Documentation

A DVF has a uniformizer in its valuation subring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · full declaration

theorem exists_uniformizer (F : DVF.{u, v} K) :
    Exists (fun pi : F.valuationSubring => F.valuation.IsUniformizer (pi : K)) := by
  change Exists
    (fun pi : F.valuation.valuationSubring => F.valuation.IsUniformizer (pi : K))
  exact Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial F.valuation

theorem

uniformizer_mem_maximalIdeal

L156 ↗

ValuationTheory.DiscreteValuationField.DVF.uniformizer_mem_maximalIdeal

Documentation

A uniformizer lies in the maximal ideal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem uniformizer_mem_maximalIdeal (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) :
    pi ∈ F.maximalIdeal

theorem

maximalIdeal_eq_span_uniformizer

L163 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdeal_eq_span_uniformizer

Documentation

A uniformizer generates the maximal ideal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdeal_eq_span_uniformizer (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) :
    F.maximalIdeal = Ideal.span (Set.singleton pi)

theorem

maximalIdeal_pow_eq_span_uniformizer_pow

L172 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdeal_pow_eq_span_uniformizer_pow

Documentation

Powers of the maximal ideal are generated by powers of any chosen uniformizer.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdeal_pow_eq_span_uniformizer_pow (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) :
    F.maximalIdeal ^ n = Ideal.span ({pi ^ n} : Set F.valuationSubring)

theorem

mem_maximalIdeal_pow_iff_uniformizer_pow_dvd

L181 ↗

ValuationTheory.DiscreteValuationField.DVF.mem_maximalIdeal_pow_iff_uniformizer_pow_dvd

Documentation

Membership in a power of the maximal ideal is divisibility by the corresponding power of a uniformizer.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem mem_maximalIdeal_pow_iff_uniformizer_pow_dvd (F : DVF.{u, v} K)
    {pi x : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    x ∈ F.maximalIdeal ^ n ↔ pi ^ n ∣ x

theorem

uniformizer_pow_not_mem_maximalIdeal_pow_succ

L190 ↗

ValuationTheory.DiscreteValuationField.DVF.uniformizer_pow_not_mem_maximalIdeal_pow_succ

Documentation

No power of a uniformizer lies one step deeper in the maximal-ideal filtration.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem uniformizer_pow_not_mem_maximalIdeal_pow_succ
    (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) :
    pi ^ n ∉ F.maximalIdeal ^ (n + 1)

theorem

uniformizer_not_mem_maximalIdeal_sq

L213 ↗

ValuationTheory.DiscreteValuationField.DVF.uniformizer_not_mem_maximalIdeal_sq

Documentation

A uniformizer belongs to the maximal ideal but not to its square.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem uniformizer_not_mem_maximalIdeal_sq (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) :
    pi ∉ F.maximalIdeal ^ 2

theorem

nonzero_ideal_eq_maximalIdeal_pow

L220 ↗

ValuationTheory.DiscreteValuationField.DVF.nonzero_ideal_eq_maximalIdeal_pow

Documentation

Every nonzero ideal in the valuation ring of a DVF is a power of the maximal ideal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem nonzero_ideal_eq_maximalIdeal_pow (F : DVF.{u, v} K)
    (I : Ideal F.valuationSubring) (hI : I ≠ ⊥) :
    ∃ n : ℕ, I = F.maximalIdeal ^ n

theorem

isUniformizer_of_mem_maximalIdeal_of_not_mem_maximalIdeal_sq

L234 ↗

ValuationTheory.DiscreteValuationField.DVF.isUniformizer_of_mem_maximalIdeal_of_not_mem_maximalIdeal_sq

Documentation

An element of the valuation ring lying in the maximal ideal but not in its square is a uniformizer.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem isUniformizer_of_mem_maximalIdeal_of_not_mem_maximalIdeal_sq
    (F : DVF.{u, v} K) {x : F.valuationSubring}
    (hx : x ∈ F.maximalIdeal) (hx_sq : x ∉ F.maximalIdeal ^ 2) :
    F.valuation.IsUniformizer (x : K)

theorem

uniformizer_mul_unit_not_mem_maximalIdeal_sq

L292 ↗

ValuationTheory.DiscreteValuationField.DVF.uniformizer_mul_unit_not_mem_maximalIdeal_sq

Documentation

Multiplying a uniformizer by a valuation-ring unit does not move it into the square of the maximal ideal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem uniformizer_mul_unit_not_mem_maximalIdeal_sq
    (F : DVF.{u, v} K) {pi u : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (hu : IsUnit u) :
    pi * u ∉ F.maximalIdeal ^ 2

theorem

maximalIdeal_ne_bot

L304 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdeal_ne_bot

Documentation

The maximal ideal of a DVF valuation ring is nonzero.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdeal_ne_bot (F : DVF.{u, v} K) :
    F.maximalIdeal ≠ ⊥

abbrev

maximalIdealPowSuccSubmodule

L319 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccSubmodule

Documentation

The submodule m^(n+1) inside m^n.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev maximalIdealPowSuccSubmodule (F : DVF.{u, v} K) (n : ℕ) :
    Submodule F.valuationSubring ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)

def

MaximalIdealPowSuccQuot

L326 ↗

ValuationTheory.DiscreteValuationField.DVF.MaximalIdealPowSuccQuot

Documentation

The additive ideal-power quotient m^n/m^(n+1).

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def MaximalIdealPowSuccQuot (F : DVF.{u, v} K) (n : ℕ) : Type u

instance

maximalIdealPowSuccQuotAddCommGroup

L331 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotAddCommGroup

Documentation

A successive maximal-ideal quotient is an additive commutative group.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

instance maximalIdealPowSuccQuotAddCommGroup
    (F : DVF.{u, v} K) (n : ℕ) :
    AddCommGroup (F.MaximalIdealPowSuccQuot n)

instance

maximalIdealPowSuccQuotModule

L340 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotModule

Documentation

A successive maximal-ideal quotient is a module over the valuation subring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

instance maximalIdealPowSuccQuotModule
    (F : DVF.{u, v} K) (n : ℕ) :
    Module F.valuationSubring (F.MaximalIdealPowSuccQuot n)

def

maximalIdealPowSuccQuotConcreteLinearEquiv

L349 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotConcreteLinearEquiv

Documentation

Explicit access to the concrete submodule-quotient representation.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def maximalIdealPowSuccQuotConcreteLinearEquiv
    (F : DVF.{u, v} K) (n : ℕ) :
    F.MaximalIdealPowSuccQuot n ≃ₗ[F.valuationSubring]
      (((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u) ⧸
        F.maximalIdealPowSuccSubmodule n)

def

maximalIdealPowSuccQuotMk

L362 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMk

Documentation

The quotient map m^n → m^n/m^(n+1).

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def maximalIdealPowSuccQuotMk (F : DVF.{u, v} K) (n : ℕ) :
    ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u) →ₗ[F.valuationSubring]
      F.MaximalIdealPowSuccQuot n

theorem

maximalIdealPowSuccQuotConcreteLinearEquiv_mk

L374 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotConcreteLinearEquiv_mk

Documentation

The concrete linear equivalence sends a quotient representative to the same coset.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotConcreteLinearEquiv_mk
    (F : DVF.{u, v} K) (n : ℕ)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    F.maximalIdealPowSuccQuotConcreteLinearEquiv n
        (F.maximalIdealPowSuccQuotMk n a) =
      Submodule.Quotient.mk a

theorem

maximalIdealPowSuccQuotMk_surjective

L383 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMk_surjective

Documentation

The canonical map onto a successive maximal-ideal quotient is surjective.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotMk_surjective
    (F : DVF.{u, v} K) (n : ℕ) :
    Function.Surjective (F.maximalIdealPowSuccQuotMk n)

theorem

inductionOn

L389 ↗

ValuationTheory.DiscreteValuationField.DVF.MaximalIdealPowSuccQuot.inductionOn

Documentation

Eliminate an ideal-power quotient class through its canonical map.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem MaximalIdealPowSuccQuot.inductionOn
    (F : DVF.{u, v} K) (n : ℕ)
    {motive : F.MaximalIdealPowSuccQuot n → Prop}
    (q : F.MaximalIdealPowSuccQuot n)
    (h : ∀ a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u),
      motive (F.maximalIdealPowSuccQuotMk n a)) :
    motive q

theorem

inductionOn₂

L405 ↗

ValuationTheory.DiscreteValuationField.DVF.MaximalIdealPowSuccQuot.inductionOn₂

Documentation

Binary elimination through arbitrary ideal-power representatives.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem MaximalIdealPowSuccQuot.inductionOn₂
    (F : DVF.{u, v} K) (n : ℕ)
    {motive : F.MaximalIdealPowSuccQuot n →
      F.MaximalIdealPowSuccQuot n → Prop}
    (q r : F.MaximalIdealPowSuccQuot n)
    (h : ∀ a b : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u),
      motive (F.maximalIdealPowSuccQuotMk n a)
        (F.maximalIdealPowSuccQuotMk n b)) :
    motive q r

def

maximalIdealPowSuccQuotLift

L423 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotLift

Documentation

Descend a representative-level function constant modulo m^(n+1).

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def maximalIdealPowSuccQuotLift
    (F : DVF.{u, v} K) {P : Sort*} (n : ℕ)
    (f : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u) → P)
    (h : ∀ a b, a - b ∈ F.maximalIdealPowSuccSubmodule n →
      f a = f b) :
    F.MaximalIdealPowSuccQuot n → P

theorem

maximalIdealPowSuccQuotLift_mk

L445 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotLift_mk

Documentation

A lift from the successive ideal quotient evaluates on representatives by the supplied map.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotLift_mk
    (F : DVF.{u, v} K) {P : Sort*} (n : ℕ)
    (f : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u) → P)
    (h : ∀ a b, a - b ∈ F.maximalIdealPowSuccSubmodule n →
      f a = f b)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    F.maximalIdealPowSuccQuotLift n f h
        (F.maximalIdealPowSuccQuotMk n a) = f a

def

maximalIdealPowSuccQuotLinearLift

L456 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotLinearLift

Documentation

Descend a linear map vanishing on m^(n+1) inside m^n.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def maximalIdealPowSuccQuotLinearLift
    (F : DVF.{u, v} K) {M : Type*} [AddCommGroup M]
    [Module F.valuationSubring M] (n : ℕ)
    (f : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)
      →ₗ[F.valuationSubring] M)
    (h : F.maximalIdealPowSuccSubmodule n ≤ f.ker) :
    F.MaximalIdealPowSuccQuot n →ₗ[F.valuationSubring] M

theorem

maximalIdealPowSuccQuotLinearLift_mk

L470 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotLinearLift_mk

Documentation

The linear lift from a successive ideal quotient has the prescribed value on representatives.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotLinearLift_mk
    (F : DVF.{u, v} K) {M : Type*} [AddCommGroup M]
    [Module F.valuationSubring M] (n : ℕ)
    (f : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)
      →ₗ[F.valuationSubring] M)
    (h : F.maximalIdealPowSuccSubmodule n ≤ f.ker)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    F.maximalIdealPowSuccQuotLinearLift n f h
        (F.maximalIdealPowSuccQuotMk n a) = f a

theorem

maximalIdealPowSuccQuotMk_eq_zero_iff

L483 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMk_eq_zero_iff

Documentation

A successive ideal-quotient class is zero exactly when its representative lies in the next power.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotMk_eq_zero_iff (F : DVF.{u, v} K) (n : ℕ)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    F.maximalIdealPowSuccQuotMk n a = 0 ↔
      (a : F.valuationSubring) ∈ F.maximalIdeal ^ (n + 1)

theorem

maximalIdealPowSuccQuotMk_eq_iff

L496 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMk_eq_iff

Documentation

Two successive ideal-quotient classes agree exactly when their difference lies in the next power.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotMk_eq_iff
    (F : DVF.{u, v} K) (n : ℕ)
    (a b : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    F.maximalIdealPowSuccQuotMk n a =
        F.maximalIdealPowSuccQuotMk n b ↔
      a - b ∈ F.maximalIdealPowSuccSubmodule n

theorem

mul_uniformizer_pow_mem_maximalIdeal_pow

L510 ↗

ValuationTheory.DiscreteValuationField.DVF.mul_uniformizer_pow_mem_maximalIdeal_pow

Documentation

Multiplication by the corresponding uniformizer power lands in the required maximal-ideal power.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem mul_uniformizer_pow_mem_maximalIdeal_pow (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (r : F.valuationSubring) :
    r * pi ^ n ∈ F.maximalIdeal ^ n

def

maximalIdealPowMulUniformizerPowMap

L519 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowMulUniformizerPowMap

Documentation

Multiplication by pi^n, landing in m^n.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · full declaration

def maximalIdealPowMulUniformizerPowMap (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    F.valuationSubring →ₗ[F.valuationSubring]
      ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u) where
  toFun r := ⟨r * pi ^ n, F.mul_uniformizer_pow_mem_maximalIdeal_pow hpi n r⟩
  map_add' r s := by
    ext
    simp [add_mul]
  map_smul' a r := by
    ext
    simp [mul_assoc]

theorem

mul_uniformizer_pow_mem_maximalIdeal_pow_succ_iff

L533 ↗

ValuationTheory.DiscreteValuationField.DVF.mul_uniformizer_pow_mem_maximalIdeal_pow_succ_iff

Documentation

After multiplying by a uniformizer power, next-level membership is equivalent to maximal-ideal membership.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem mul_uniformizer_pow_mem_maximalIdeal_pow_succ_iff (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (r : F.valuationSubring) :
    r * pi ^ n ∈ F.maximalIdeal ^ (n + 1) ↔ r ∈ F.maximalIdeal

def

maximalIdealPowSuccQuotMulUniformizerPowMap

L562 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMulUniformizerPowMap

Documentation

The map O → m^n/m^(n+1) induced by multiplication by pi^n.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def maximalIdealPowSuccQuotMulUniformizerPowMap (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    F.valuationSubring →ₗ[F.valuationSubring] F.MaximalIdealPowSuccQuot n

theorem

maximalIdealPowSuccQuotMulUniformizerPowMap_ker

L569 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMulUniformizerPowMap_ker

Documentation

The kernel of multiplication by a uniformizer power is the residue-level defining submodule.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotMulUniformizerPowMap_ker (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    LinearMap.ker (F.maximalIdealPowSuccQuotMulUniformizerPowMap hpi n) =
      F.maximalIdeal

theorem

maximalIdealPowSuccQuotMulUniformizerPowMap_surjective

L583 ↗

ValuationTheory.DiscreteValuationField.DVF.maximalIdealPowSuccQuotMulUniformizerPowMap_surjective

Documentation

Multiplication by a uniformizer power surjects onto the successive ideal quotient.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdealPowSuccQuotMulUniformizerPowMap_surjective (F : DVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    Function.Surjective (F.maximalIdealPowSuccQuotMulUniformizerPowMap hpi n)

def

residueLinearEquivMaximalIdealPowSuccQuotOfUniformizer

L606 ↗

ValuationTheory.DiscreteValuationField.DVF.residueLinearEquivMaximalIdealPowSuccQuotOfUniformizer

Documentation

Principal-ideal scaling: multiplication by pi^n identifies O/m linearly with m^n/m^(n+1).

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def residueLinearEquivMaximalIdealPowSuccQuotOfUniformizer
    (F : DVF.{u, v} K) {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    F.residueField ≃ₗ[F.valuationSubring] F.MaximalIdealPowSuccQuot n

def

residueAddEquivMaximalIdealPowSuccQuotOfUniformizer

L617 ↗

ValuationTheory.DiscreteValuationField.DVF.residueAddEquivMaximalIdealPowSuccQuotOfUniformizer

Documentation

Additive form of O/m ≃ m^n/m^(n+1).

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

def residueAddEquivMaximalIdealPowSuccQuotOfUniformizer
    (F : DVF.{u, v} K) {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    F.residueField ≃+ F.MaximalIdealPowSuccQuot n

theorem

residueAddEquivMaximalIdealPowSuccQuotOfUniformizer_residue

L625 ↗

ValuationTheory.DiscreteValuationField.DVF.residueAddEquivMaximalIdealPowSuccQuotOfUniformizer_residue

Documentation

The residue-to-graded-piece equivalence sends a residue class to its uniformizer-scaled quotient class.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] DVF.instValueGroup DVF.instRankOneDiscrete
namespace DVF
variable {K : Type u} [Field K]

Lean source · statement

theorem residueAddEquivMaximalIdealPowSuccQuotOfUniformizer_residue
    (F : DVF.{u, v} K) {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ)
    (r : F.valuationSubring) :
    F.residueAddEquivMaximalIdealPowSuccQuotOfUniformizer hpi n
        (F.residueMap r) =
      F.maximalIdealPowSuccQuotMulUniformizerPowMap hpi n r

Module documentation

Discretely valued fields

Successive quotients of powers of the maximal ideal

Declarations