NYLL
Module

PadicValuationComparison.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PadicValuationComparison
6 declarations indexed from sourceView source ↗

Module documentation

Comparison of the chosen and canonical valuations on the p-adic field

The concrete local-field package on ℚ_[p] uses the DVR valuation obtained from ℤ_[p], whereas mathlib's nonarchimedean-local-field API uses ValuativeRel.valuation ℚ_[p]. This file proves that these are equivalent valuations and makes the comparison usable when transporting valuation extensions.

Imports4
Imported by3

Declarations

theorem

padicDVRValuation_isEquiv_valuativeRelValuation

L37 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation_isEquiv_valuativeRelValuation
Documentation

The DVR valuation on ℚ_[p] obtained from ℤ_[p] is equivalent to the canonical valuation attached to the p-adic valuative relation.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalFieldTheory
namespace DiscreteValuationField
namespace Examples
namespace Qp
universe u v
Lean source · statement
theorem padicDVRValuation_isEquiv_valuativeRelValuation
    (p : ℕ) [Fact p.Prime] :
    (padicDVRValuation p).IsEquiv
      (ValuativeRel.valuation ℚ_[p])
theorem

padicLocalField_valuation_isEquiv_valuativeRelValuation

L54 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicLocalField_valuation_isEquiv_valuativeRelValuation
Documentation

The valuation selected by the concrete p-adic local-field package is equivalent to mathlib's canonical valuation on ℚ_[p].

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalFieldTheory
namespace DiscreteValuationField
namespace Examples
namespace Qp
universe u v
Lean source · statement
theorem padicLocalField_valuation_isEquiv_valuativeRelValuation
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).toCompleteDVF.valuation.IsEquiv
      (ValuativeRel.valuation ℚ_[p])
theorem

padicLocalField_valuation_isEquiv_localCompleteDVF

L66 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicLocalField_valuation_isEquiv_localCompleteDVF
Documentation

The chosen valuation in padicLocalField p is equivalent to the canonical complete-DVF valuation supplied by the topology-first local-field structure on ℚ_[p].

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalFieldTheory
namespace DiscreteValuationField
namespace Examples
namespace Qp
universe u v
Lean source · statement
theorem padicLocalField_valuation_isEquiv_localCompleteDVF
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).toCompleteDVF.valuation.IsEquiv
      (LocalFieldTheory.localCompleteDVF ℚ_[p]).valuation
theorem

localCompleteDVF_valuation_isEquiv_padicLocalField

L75 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.localCompleteDVF_valuation_isEquiv_padicLocalField
Documentation

Symmetric comparison, oriented for transporting canonical local-field valuation extensions to the chosen p-adic DVR valuation.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalFieldTheory
namespace DiscreteValuationField
namespace Examples
namespace Qp
universe u v
Lean source · statement
theorem localCompleteDVF_valuation_isEquiv_padicLocalField
    (p : ℕ) [Fact p.Prime] :
    (LocalFieldTheory.localCompleteDVF ℚ_[p]).valuation.IsEquiv
      (padicLocalField p).toCompleteDVF.valuation
theorem

padicLocalFieldValuation_hasExtension_of_localCompleteDVF

L84 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicLocalFieldValuation_hasExtension_of_localCompleteDVF
Documentation

Any valuation extension of the canonical complete-DVF valuation on ℚ_[p] is also an extension of the valuation selected by padicLocalField p.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalFieldTheory
namespace DiscreteValuationField
namespace Examples
namespace Qp
universe u v
Lean source · statement
theorem padicLocalFieldValuation_hasExtension_of_localCompleteDVF
    (p : ℕ) [Fact p.Prime]
    {E : Type u} [Field E] [Algebra ℚ_[p] E]
    {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
    (wE : _root_.Valuation E Gamma)
    [(LocalFieldTheory.localCompleteDVF ℚ_[p]).valuation.HasExtension wE] :
    (padicLocalField p).toCompleteDVF.valuation.HasExtension wE
theorem

localCompleteDVFValuation_hasExtension_of_padicLocalField

L97 ↗
LocalFieldTheory.DiscreteValuationField.Examples.Qp.localCompleteDVFValuation_hasExtension_of_padicLocalField
Documentation

Conversely, any valuation extension of the valuation selected by padicLocalField p is also an extension of the canonical complete-DVF valuation on ℚ_[p].

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalFieldTheory
namespace DiscreteValuationField
namespace Examples
namespace Qp
universe u v
Lean source · statement
theorem localCompleteDVFValuation_hasExtension_of_padicLocalField
    (p : ℕ) [Fact p.Prime]
    {E : Type u} [Field E] [Algebra ℚ_[p] E]
    {Gamma : Type v} [LinearOrderedCommGroupWithZero Gamma]
    (wE : _root_.Valuation E Gamma)
    [(padicLocalField p).toCompleteDVF.valuation.HasExtension wE] :
    (LocalFieldTheory.localCompleteDVF ℚ_[p]).valuation.HasExtension wE

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