NYLL
Module

Complete.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Complete
35 declarations indexed from sourceView source ↗

Module documentation

Complete discretely valued fields

Imports3
Imported by12

Declarations

class

IsCompleteDiscrete

L29 ↗
ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete
Documentation

A complete discrete valuation.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} [Field K]
variable {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
Lean source · full declaration
class IsCompleteDiscrete (val : _root_.Valuation K Gamma) : Prop where
  /-- A complete discrete valuation has discrete rank one. -/
  [isRankOneDiscrete : val.IsRankOneDiscrete]
  /-- The valuation ring is complete for its maximal-ideal adic topology. -/
  isAdicComplete :
    IsAdicComplete (IsLocalRing.maximalIdeal val.valuationSubring) val.valuationSubring
theorem

isAdicComplete

L39 ↗
ValuationTheory.DiscreteValuationField.Valuation.isAdicComplete
Documentation

Completeness of the valued field implies adic completeness of its valuation subring.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} [Field K]
variable {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
attribute [instance] IsCompleteDiscrete.isRankOneDiscrete
Lean source · statement
theorem isAdicComplete (val : _root_.Valuation K Gamma) [IsCompleteDiscrete val] :
    IsAdicComplete (IsLocalRing.maximalIdeal val.valuationSubring) val.valuationSubring
instance

isCompleteDiscrete_comap_ringEquiv

L45 ↗
ValuationTheory.DiscreteValuationField.Valuation.isCompleteDiscrete_comap_ringEquiv
Documentation

Pulling a complete discrete valuation back along a field equivalence preserves both rank-one discreteness and adic completeness.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} [Field K]
variable {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
attribute [instance] IsCompleteDiscrete.isRankOneDiscrete
Lean source · full declaration
instance isCompleteDiscrete_comap_ringEquiv
    {L : Type w} [Field L]
    (val : _root_.Valuation K Gamma) [IsCompleteDiscrete val] (e : L ≃+* K) :
    IsCompleteDiscrete (val.comap (e : L →+* K)) where
  isRankOneDiscrete := isRankOneDiscrete_comap_ringEquiv val e
  isAdicComplete := by
    let r := valuationSubringRingEquivOfComap val e
    have hmap :
        (IsLocalRing.maximalIdeal val.valuationSubring).map
            (r.symm : val.valuationSubring →+*
              (val.comap (e : L →+* K)).valuationSubring) =
          IsLocalRing.maximalIdeal
            (val.comap (e : L →+* K)).valuationSubring := by
      calc
        (IsLocalRing.maximalIdeal val.valuationSubring).map
            (r.symm : val.valuationSubring →+*
              (val.comap (e : L →+* K)).valuationSubring) =
            (IsLocalRing.maximalIdeal val.valuationSubring).comap
              (r : (val.comap (e : L →+* K)).valuationSubring →+*
                val.valuationSubring) := Ideal.map_symm r
        _ = IsLocalRing.maximalIdeal
              (val.comap (e : L →+* K)).valuationSubring :=
          maximalIdeal_comap_valuationSubringRingEquivOfComap val e
    let : IsAdicComplete
        (IsLocalRing.maximalIdeal val.valuationSubring) val.valuationSubring :=
      isAdicComplete val
    simpa [hmap] using
      (isAdicComplete_map_ringEquiv
        (I := IsLocalRing.maximalIdeal val.valuationSubring) r.symm)
theorem

henselianRing

L76 ↗
ValuationTheory.DiscreteValuationField.Valuation.henselianRing
Documentation

The valuation subring of a complete discrete valuation field is henselian.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} [Field K]
variable {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
attribute [instance] IsCompleteDiscrete.isRankOneDiscrete
Lean source · statement
theorem henselianRing (val : _root_.Valuation K Gamma) [IsCompleteDiscrete val] :
    HenselianRing val.valuationSubring (IsLocalRing.maximalIdeal val.valuationSubring)
theorem

mem_maximalIdeal_pow_iff_valuation_le_uniformizer_pow

L85 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_maximalIdeal_pow_iff_valuation_le_uniformizer_pow
Documentation

In a rank-one discrete valuation ring, membership in the n-th power of the maximal ideal is the same as the corresponding valuation bound against a chosen uniformizer power.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
namespace Valuation
variable {K : Type u} [Field K]
variable {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
attribute [instance] IsCompleteDiscrete.isRankOneDiscrete
Lean source · statement
theorem mem_maximalIdeal_pow_iff_valuation_le_uniformizer_pow
    (val : _root_.Valuation K Gamma) [val.IsRankOneDiscrete]
    {pi x : val.valuationSubring}
    (hpi : val.IsUniformizer (pi : K)) (n : ℕ) :
    x ∈ IsLocalRing.maximalIdeal val.valuationSubring ^ n ↔
      val (x : K) ≤ val ((pi ^ n : val.valuationSubring) : K)
structure

CompleteDVF

L100 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF
Documentation

A field with a chosen complete 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 w
namespace DiscreteValuationField
Lean source · full declaration
structure CompleteDVF (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 is complete and discretely rank one. -/
  [instCompleteDiscrete : Valuation.IsCompleteDiscrete valuation]
abbrev

toHenselianDVF

L118 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.toHenselianDVF
Documentation

A complete DVF is Henselian. This is the canonical forgetful projection: all weaker DVF data are obtained through this object.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · full declaration
abbrev toHenselianDVF (F : CompleteDVF.{u, v} K) : HenselianDVF.{u, v} K where
  toDVF :=
    { ValueGroup := F.ValueGroup
      valuation := F.valuation }
  instHenselian := by
    change HenselianRing F.valuation.valuationSubring
      (IsLocalRing.maximalIdeal F.valuation.valuationSubring)
    exact Valuation.henselianRing F.valuation
abbrev

toDVF

L129 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.toDVF
Documentation

The underlying DVF, obtained along the canonical CompleteDVF -> HenselianDVF -> DVF path.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
abbrev toDVF (F : CompleteDVF.{u, v} K) : DVF.{u, v} K
abbrev

valuationSubring

L133 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.valuationSubring
Documentation

Introduces the abbreviation valuationSubring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
abbrev valuationSubring (F : CompleteDVF.{u, v} K) : Type u
abbrev

maximalIdeal

L137 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.maximalIdeal
Documentation

Introduces the abbreviation maximalIdeal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
abbrev maximalIdeal (F : CompleteDVF.{u, v} K) : Ideal F.valuationSubring
abbrev

residueField

L141 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.residueField
Documentation

Introduces the abbreviation residueField.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
abbrev residueField (F : CompleteDVF.{u, v} K) : Type u
abbrev

residueMap

L145 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.residueMap
Documentation

Introduces the abbreviation residueMap.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
abbrev residueMap (F : CompleteDVF.{u, v} K) :
    RingHom F.valuationSubring F.residueField
theorem

valuationSubring_isDiscreteValuationRing

L150 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.valuationSubring_isDiscreteValuationRing
Documentation

The valuation subring in the complete model is a discrete valuation ring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubring_isDiscreteValuationRing (F : CompleteDVF.{u, v} K) :
    IsDiscreteValuationRing F.valuationSubring
theorem

isAdicComplete

L155 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.isAdicComplete
Documentation

The complete DVR model is complete for its maximal-ideal-adic topology.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem isAdicComplete (F : CompleteDVF.{u, v} K) :
    IsAdicComplete F.maximalIdeal F.valuationSubring
instance

instIsAdicComplete

L163 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.instIsAdicComplete
Documentation

The complete DVR valuation ring carries its canonical adic-completeness instance.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
instance instIsAdicComplete (F : CompleteDVF.{u, v} K) :
    IsAdicComplete F.maximalIdeal F.valuationSubring
theorem

henselianRing

L168 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.henselianRing
Documentation

Adic completeness makes the complete DVR valuation ring henselian.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem henselianRing (F : CompleteDVF.{u, v} K) :
    HenselianRing F.valuationSubring F.maximalIdeal
theorem

mem_valuationSubring_iff

L173 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.mem_valuationSubring_iff
Documentation

Membership in the valuation subring is characterized by nonnegative valuation.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem mem_valuationSubring_iff (F : CompleteDVF.{u, v} K) (x : K) :
    x ∈ F.valuation.valuationSubring ↔ F.valuation x <= 1
theorem

mem_maximalIdeal_iff

L178 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.mem_maximalIdeal_iff
Documentation

Membership in the maximal ideal is characterized by strictly positive valuation.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem mem_maximalIdeal_iff (F : CompleteDVF.{u, v} K)
    (x : F.valuationSubring) :
    x ∈ F.maximalIdeal ↔ F.valuation (x : K) < 1
theorem

residue_eq_zero_iff

L184 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.residue_eq_zero_iff
Documentation

An integral element has zero residue exactly when it 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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem residue_eq_zero_iff (F : CompleteDVF.{u, v} K)
    (x : F.valuationSubring) :
    F.residueMap x = 0 ↔ x ∈ F.maximalIdeal
theorem

residue_ne_zero_iff_isUnit

L190 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.residue_ne_zero_iff_isUnit
Documentation

An integral element has nonzero residue exactly when it is a unit.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem residue_ne_zero_iff_isUnit (F : CompleteDVF.{u, v} K)
    (x : F.valuationSubring) :
    F.residueMap x ≠ 0 ↔ IsUnit x
theorem

residue_surjective

L196 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.residue_surjective
Documentation

Every residue-field element has a representative in the valuation ring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem residue_surjective (F : CompleteDVF.{u, v} K) :
    Function.Surjective F.residueMap
theorem

exists_uniformizer

L201 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.exists_uniformizer
Documentation

A complete discrete valuation field admits a uniformizer.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · full declaration
theorem exists_uniformizer (F : CompleteDVF.{u, v} K) :
    Exists (fun pi : F.valuationSubring => F.valuation.IsUniformizer (pi : K)) :=
  F.toDVF.exists_uniformizer
theorem

uniformizer_mem_maximalIdeal

L206 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.uniformizer_mem_maximalIdeal
Documentation

Every chosen 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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem uniformizer_mem_maximalIdeal (F : CompleteDVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) :
    pi ∈ F.maximalIdeal
theorem

maximalIdeal_eq_span_uniformizer

L212 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.maximalIdeal_eq_span_uniformizer
Documentation

The maximal ideal is the principal ideal generated by a uniformizer.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem maximalIdeal_eq_span_uniformizer (F : CompleteDVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) :
    F.maximalIdeal = Ideal.span ({pi} : Set F.valuationSubring)
theorem

maximalIdeal_pow_eq_span_uniformizer_pow

L219 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem maximalIdeal_pow_eq_span_uniformizer_pow (F : CompleteDVF.{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

L227 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem mem_maximalIdeal_pow_iff_uniformizer_pow_dvd (F : CompleteDVF.{u, v} K)
    {pi x : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    x ∈ F.maximalIdeal ^ n ↔ pi ^ n ∣ x
theorem

uniformizer_not_mem_maximalIdeal_sq

L234 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem uniformizer_not_mem_maximalIdeal_sq (F : CompleteDVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K)) :
    pi ∉ F.maximalIdeal ^ 2
theorem

nonzero_ideal_eq_maximalIdeal_pow

L241 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.nonzero_ideal_eq_maximalIdeal_pow
Documentation

Every nonzero ideal in the valuation ring of a complete 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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem nonzero_ideal_eq_maximalIdeal_pow (F : CompleteDVF.{u, v} K)
    (I : Ideal F.valuationSubring) (hI : I ≠ ⊥) :
    ∃ n : ℕ, I = F.maximalIdeal ^ n
theorem

principalAdicComplete_of_ne_zero_mem_maximalIdeal

L249 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.principalAdicComplete_of_ne_zero_mem_maximalIdeal
Documentation

In a complete DVF, the principal filtration generated by any nonzero element of the maximal ideal is complete. The source is that every nonzero ideal in a DVR is a positive 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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem principalAdicComplete_of_ne_zero_mem_maximalIdeal
    (F : CompleteDVF.{u, v} K) {π : F.valuationSubring}
    (hπ_ne : π ≠ 0) (hπ_mem : π ∈ F.maximalIdeal) :
    IsAdicComplete (Ideal.span ({π} : Set F.valuationSubring))
      F.valuationSubring
theorem

principalPrecomplete_of_ne_zero_mem_maximalIdeal

L290 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.principalPrecomplete_of_ne_zero_mem_maximalIdeal
Documentation

Principal precompleteness generated from complete-DVF completeness.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem principalPrecomplete_of_ne_zero_mem_maximalIdeal
    (F : CompleteDVF.{u, v} K) {π : F.valuationSubring}
    (hπ_ne : π ≠ 0) (hπ_mem : π ∈ F.maximalIdeal) :
    IsPrecomplete (Ideal.span ({π} : Set F.valuationSubring))
      F.valuationSubring
theorem

principalHausdorff_of_ne_zero_mem_maximalIdeal

L299 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.principalHausdorff_of_ne_zero_mem_maximalIdeal
Documentation

Principal separatedness generated from complete-DVF completeness.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem principalHausdorff_of_ne_zero_mem_maximalIdeal
    (F : CompleteDVF.{u, v} K) {π : F.valuationSubring}
    (hπ_ne : π ≠ 0) (hπ_mem : π ∈ F.maximalIdeal) :
    IsHausdorff (Ideal.span ({π} : Set F.valuationSubring))
      F.valuationSubring
theorem

maximalIdeal_ne_bot

L308 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.maximalIdeal_ne_bot
Documentation

The maximal ideal of a complete 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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem maximalIdeal_ne_bot (F : CompleteDVF.{u, v} K) :
    F.maximalIdeal ≠ ⊥
theorem

uniformizer_pow_not_mem_maximalIdeal_pow_succ

L322 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.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 w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem uniformizer_pow_not_mem_maximalIdeal_pow_succ
    (F : CompleteDVF.{u, v} K)
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) :
    pi ^ n ∉ F.maximalIdeal ^ (n + 1)
theorem

eq_zero_of_mem_maximalIdeal_pow_all

L332 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.eq_zero_of_mem_maximalIdeal_pow_all
Documentation

The maximal-ideal topology on the valuation ring of a complete DVF is separated. This is the uniqueness half needed by unit-level completion arguments.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem eq_zero_of_mem_maximalIdeal_pow_all
    (F : CompleteDVF.{u, v} K) {x : F.valuationSubring}
    (hx : ∀ n : ℕ, x ∈ F.maximalIdeal ^ n) :
    x = 0
theorem

unit_eq_of_idealQuotient_eq_all

L362 ↗
ValuationTheory.DiscreteValuationField.CompleteDVF.unit_eq_of_idealQuotient_eq_all
Documentation

Valuation-ring units are separated by all finite maximal-ideal quotient coordinates.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w
namespace DiscreteValuationField
attribute [instance] CompleteDVF.instValueGroup CompleteDVF.instCompleteDiscrete
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem unit_eq_of_idealQuotient_eq_all
    (F : CompleteDVF.{u, v} K) {u₁ u₂ : F.valuationSubringˣ}
    (h :
      ∀ n : ℕ,
        Ideal.Quotient.mk (F.maximalIdeal ^ n) (u₁ : F.valuationSubring) =
          Ideal.Quotient.mk (F.maximalIdeal ^ n) (u₂ : F.valuationSubring)) :
    u₁ = u₂

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