Module

DiscreteValuedCompletion.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DiscreteValuedCompletion

6 declarations indexed from sourceView source ↗

Module documentation

Complete discrete valuations on the actual valued completion

The extended valuation has the same value group as the original valuation. For any discretely valued field, the native completeness of the valued completion therefore supplies a complete discrete valuation. The canonical field map preserves valuation values and hence the residue characteristic.

Imports8

Nyll.ValuedFieldTheory.Valuation.Completion.WithValScalars
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Complete
Nyll.ValuedFieldTheory.Valuation.ValuedAdicComplete
Mathlib.Algebra.GroupWithZero.Range
Mathlib.RingTheory.Valuation.Extension
Mathlib.Algebra.CharP.Algebra
Mathlib.Topology.Algebra.Valued.ValuedField
Mathlib.Topology.Algebra.Valued.WithVal

Imported by8

theorem

completion_valueGroup_eq

L29 ↗

ValuationTheory.DiscreteValuationField.Valuation.completion_valueGroup_eq

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
universe u v

Lean source · statement

theorem completion_valueGroup_eq
    {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
    (val : _root_.Valuation K Γ) :
    MonoidWithZeroHom.valueGroup
        (.ofClass (Valued.v : _root_.Valuation val.Completion Γ)) =
      MonoidWithZeroHom.valueGroup (.ofClass val)

theorem

completion_valuation_algebraMap

L67 ↗

ValuationTheory.DiscreteValuationField.Valuation.completion_valuation_algebraMap

Documentation

The canonical valuation on the completion preserves the original values along the existing ground-field algebra map.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
universe u v
variable {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]

Lean source · statement

theorem completion_valuation_algebraMap
    (val : _root_.Valuation K Γ) (x : K) :
    (Valued.v : _root_.Valuation val.Completion Γ)
      (algebraMap K val.Completion x) = val x

theorem

completion_isRankOneDiscrete

L77 ↗

ValuationTheory.DiscreteValuationField.Valuation.completion_isRankOneDiscrete

Documentation

Completion preserves rank-one discreteness; the generator remains a generator because the value group is unchanged.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
universe u v
variable {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]

Lean source · full declaration

theorem completion_isRankOneDiscrete
    (val : _root_.Valuation K Γ) [val.IsRankOneDiscrete] :
    (Valued.v : _root_.Valuation val.Completion
      Γ).IsRankOneDiscrete where
  exists_generator_lt_one' := by
    refine ⟨_root_.Valuation.IsRankOneDiscrete.generator val, ?_,
      _root_.Valuation.IsRankOneDiscrete.generator_lt_one val⟩
    exact (_root_.Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup val).trans
      (completion_valueGroup_eq val).symm

theorem

completion_isCompleteDiscrete

L89 ↗

ValuationTheory.DiscreteValuationField.Valuation.completion_isCompleteDiscrete

Documentation

The actual completion of a discretely valued field is complete discrete. Adic completeness is generated from its native valued-field completeness.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
universe u v
variable {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]

Lean source · statement

theorem completion_isCompleteDiscrete
    (val : _root_.Valuation K Γ) [val.IsRankOneDiscrete] :
    IsCompleteDiscrete (Valued.v : _root_.Valuation val.Completion
      Γ)

theorem

completion_hasExtension

L100 ↗

ValuationTheory.DiscreteValuationField.Valuation.completion_hasExtension

Documentation

The canonical completion valuation actually extends the original valuation.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
universe u v
variable {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]

Lean source · statement

theorem completion_hasExtension
    (val : _root_.Valuation K Γ) :
    val.HasExtension (Valued.v : _root_.Valuation val.Completion
      Γ)

theorem

completion_residueChar

L115 ↗

ValuationTheory.DiscreteValuationField.Valuation.completion_residueChar

Documentation

Completion preserves residue characteristic through the induced residue field embedding, with no residue-field comparison assumed as input.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
universe u v
variable {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]

Lean source · statement

theorem completion_residueChar
    (val : _root_.Valuation K Γ) (p : ℕ)
    [hres : CharP (IsLocalRing.ResidueField val.valuationSubring) p] :
    CharP (IsLocalRing.ResidueField
      (Valued.v : _root_.Valuation val.Completion
        Γ).valuationSubring) p

Module documentation

Complete discrete valuations on the actual valued completion

Declarations

completion_valueGroup_eq

completion_valuation_algebraMap

completion_isRankOneDiscrete

completion_isCompleteDiscrete

completion_hasExtension

completion_residueChar