NYLL
Module

HenselianValuationExtension.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianValuationExtension
10 declarations indexed from sourceView source ↗

Module documentation

Valuation-extension API for Henselian discretely valued fields

This file keeps the valuation-extension uniqueness interface separate from the lightweight Henselian-DVF core. The core file is used by Hensel lifting and does not need to import mathlib's full Valuation.HasExtension API.

Imports2
Imported by3

Declarations

def

HasUniqueValuationExtension

L33 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.HasUniqueValuationExtension
Documentation

A Henselian-DVF uniqueness predicate for extensions of the base valuation. This is the non-complete analogue of the complete-DVF predicate used by ValuedExtension.HasUniqueValuationExtension.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
Lean source · statement
def HasUniqueValuationExtension (base : HenselianDVF.{u, v} K)
    (target : HenselianDVF.{w, x} L) : Prop
theorem

valuation_isEquiv_of_valuationSubring_eq

L42 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.valuation_isEquiv_of_valuationSubring_eq
Documentation

A Henselian-DVF valuation is equivalent to another valuation as soon as their valuation subrings are equal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
omit [Algebra K L] in
Lean source · statement
theorem valuation_isEquiv_of_valuationSubring_eq
    (_base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma')
    (hsub : target.toDVF.valuation.valuationSubring = v'.valuationSubring) :
    target.toDVF.valuation.IsEquiv v'
theorem

valuationSubring_eq_of_valuation_isEquiv

L52 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_eq_of_valuation_isEquiv
Documentation

Equivalent valuations have the same valuation subring.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
omit [Algebra K L] in
Lean source · statement
theorem valuationSubring_eq_of_valuation_isEquiv
    (_base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    {v' : _root_.Valuation L Gamma'}
    (h : target.toDVF.valuation.IsEquiv v') :
    target.toDVF.valuation.valuationSubring = v'.valuationSubring
theorem

valuation_isEquiv_iff_valuationSubring_eq

L62 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.valuation_isEquiv_iff_valuationSubring_eq
Documentation

Valuation equivalence is exactly equality of valuation subrings.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
omit [Algebra K L] in
Lean source · statement
theorem valuation_isEquiv_iff_valuationSubring_eq
    (_base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') :
    target.toDVF.valuation.IsEquiv v' ↔
      target.toDVF.valuation.valuationSubring = v'.valuationSubring
theorem

valuationSubring_eq_iff_mem_valuationSubring

L73 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_eq_iff_mem_valuationSubring
Documentation

Equality of valuation subrings is exactly pointwise equality of membership in those subrings.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
omit [Algebra K L] in
Lean source · statement
theorem valuationSubring_eq_iff_mem_valuationSubring
    (_base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') :
    target.toDVF.valuation.valuationSubring = v'.valuationSubring ↔
      ∀ z : L, z ∈ target.toDVF.valuation.valuationSubring ↔
        z ∈ v'.valuationSubring
theorem

valuation_isEquiv_iff_mem_valuationSubring

L89 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.valuation_isEquiv_iff_mem_valuationSubring
Documentation

Valuation equivalence can be checked by pointwise equality of membership in valuation subrings.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
omit [Algebra K L] in
Lean source · statement
theorem valuation_isEquiv_iff_mem_valuationSubring
    (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') :
    target.toDVF.valuation.IsEquiv v' ↔
      ∀ z : L, z ∈ target.toDVF.valuation.valuationSubring ↔
        z ∈ v'.valuationSubring
theorem

hasUniqueValuationExtension_of_forall_valuationSubring_eq

L101 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.hasUniqueValuationExtension_of_forall_valuationSubring_eq
Documentation

Equality of valuation subrings for all extensions proves Henselian-DVF uniqueness up to mathlib's valuation equivalence.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
Lean source · statement
theorem hasUniqueValuationExtension_of_forall_valuationSubring_eq
    (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    (h :
      ∀ {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
        (v' : _root_.Valuation L Gamma') [base.toDVF.valuation.HasExtension v'],
          target.toDVF.valuation.valuationSubring = v'.valuationSubring) :
    HasUniqueValuationExtension.{u, v, w, x, y} base target
theorem

valuationSubring_eq_of_hasUniqueValuationExtension

L113 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_eq_of_hasUniqueValuationExtension
Documentation

Henselian-DVF unique extension implies valuation-subring equality for every extension valuation.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
Lean source · statement
theorem valuationSubring_eq_of_hasUniqueValuationExtension
    (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    (huniq : HasUniqueValuationExtension.{u, v, w, x, y} base target)
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') [base.toDVF.valuation.HasExtension v'] :
    target.toDVF.valuation.valuationSubring = v'.valuationSubring
theorem

hasUniqueValuationExtension_iff_forall_valuationSubring_eq

L123 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.hasUniqueValuationExtension_iff_forall_valuationSubring_eq
Documentation

Henselian-DVF unique extension is equivalent to equality of the chosen target valuation subring with every extension valuation subring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
Lean source · statement
theorem hasUniqueValuationExtension_iff_forall_valuationSubring_eq
    (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L) :
    HasUniqueValuationExtension.{u, v, w, x, y} base target ↔
      ∀ {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
        (v' : _root_.Valuation L Gamma') [base.toDVF.valuation.HasExtension v'],
          target.toDVF.valuation.valuationSubring = v'.valuationSubring
theorem

hasUniqueValuationExtension_iff_forall_mem_valuationSubring

L137 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.hasUniqueValuationExtension_iff_forall_mem_valuationSubring
Documentation

Henselian-DVF unique extension can be checked pointwise on membership in valuation subrings.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]
variable {L : Type w} [Field L] [Algebra K L]
Lean source · statement
theorem hasUniqueValuationExtension_iff_forall_mem_valuationSubring
    (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L) :
    HasUniqueValuationExtension.{u, v, w, x, y} base target ↔
      ∀ {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
        (v' : _root_.Valuation L Gamma') [base.toDVF.valuation.HasExtension v'],
          ∀ z : L, z ∈ target.toDVF.valuation.valuationSubring ↔
            z ∈ v'.valuationSubring

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