Module

ValuationExtension.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ValuationExtension

12 declarations indexed from sourceView source ↗

Module documentation

Valuation extensions

Mathlib's uniqueness criterion for valuations is expressed through Valuation.IsEquiv: two valuations on the same field are equivalent exactly when they have the same valuation subring. The results here use the ambient valued-extension property directly; no marker object is introduced.

Imports1

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Extensions

Imported by5

theorem

hasExtension_of_isEquiv_base

L38 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.hasExtension_of_isEquiv_base

Documentation

Replacing the base valuation by an equivalent valuation preserves the extension relation.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section EquivalentBase
variable {Gamma₁ Gamma₂ GammaL : Type*}
variable [LinearOrderedCommGroupWithZero Gamma₁]
variable [LinearOrderedCommGroupWithZero Gamma₂]
variable [LinearOrderedCommGroupWithZero GammaL]

Lean source · full declaration

theorem hasExtension_of_isEquiv_base
    {v₁ : _root_.Valuation K Gamma₁}
    {v₂ : _root_.Valuation K Gamma₂}
    {wL : _root_.Valuation L GammaL}
    (h : v₁.IsEquiv v₂) [v₂.HasExtension wL] :
    v₁.HasExtension wL where
  val_isEquiv_comap :=
    h.trans
      (_root_.Valuation.HasExtension.val_isEquiv_comap
        (vR := v₂) (vA := wL))

theorem

hasExtension_comap_of_algebraMap_compatible

L61 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.hasExtension_comap_of_algebraMap_compatible

Documentation

If an ambient valuation extends the base valuation, then its pullback along any field embedding compatible with the two base embeddings also extends the base valuation.

Source context 11 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section ComapAlongCompatibleEmbedding
variable {M : Type y} [Field M] [Algebra K M]
variable {GammaK GammaM : Type*}
variable [LinearOrderedCommGroupWithZero GammaK]
variable [LinearOrderedCommGroupWithZero GammaM]

Lean source · full declaration

theorem hasExtension_comap_of_algebraMap_compatible
    {vK : _root_.Valuation K GammaK}
    {vM : _root_.Valuation M GammaM}
    (ι : L →+* M)
    (hι :
      ι.comp (algebraMap K L) =
        algebraMap K M)
    [vK.HasExtension vM] :
    vK.HasExtension (vM.comap ι) where
  val_isEquiv_comap := by
    rw [_root_.Valuation.isEquiv_iff_val_le_one]
    intro a
    change
      vK a ≤ 1 ↔
        vM (ι (algebraMap K L a)) ≤ 1
    rw [show ι (algebraMap K L a) = algebraMap K M a by
      exact DFunLike.congr_fun hι a]
    exact
      (_root_.Valuation.HasExtension.val_map_le_one_iff
        (vR := vK) (vA := vM) a).symm

theorem

valuation_hasExtension_of_local_valuationSubring_map

L95 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.valuation_hasExtension_of_local_valuationSubring_map

Documentation

A local map between the valuation rings, whose map on fraction fields is the given algebra map, determines an extension of valuations.

The locality hypothesis is the essential point: if an element of the base field is not integral, its inverse lies in the maximal ideal. Locality sends that inverse into the target maximal ideal, so the image of the original element cannot be integral.

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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section LocalValuationSubringMap
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuation_hasExtension_of_local_valuationSubring_map
    (f : base.valuationSubring →+* target.valuationSubring)
    [IsLocalHom f]
    (hcoe : ∀ z : base.valuationSubring,
      ((f z : target.valuationSubring) : L) =
        algebraMap K L (z : K)) :
    base.valuation.HasExtension target.valuation

theorem

valuation_hasExtension_of_valuationSubring_equiv

L163 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.valuation_hasExtension_of_valuationSubring_equiv

Documentation

An equivalence of valuation subrings whose underlying field map is the given algebra map determines an extension of valuations. Surjectivity makes the induced ring homomorphism local, so this is the source-producing equivalence form of valuation_hasExtension_of_local_valuationSubring_map.

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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section LocalValuationSubringMap
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuation_hasExtension_of_valuationSubring_equiv
    (e : base.valuationSubring ≃+* target.valuationSubring)
    (hcoe : ∀ z : base.valuationSubring,
      ((e z : target.valuationSubring) : L) =
        algebraMap K L (z : K)) :
    base.valuation.HasExtension target.valuation

theorem

comap_valuationSubring_eq_base

L183 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.comap_valuationSubring_eq_base

Documentation

The target valuation subring pulls back to the base valuation subring.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Pullback
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem comap_valuationSubring_eq_base :
    target.valuation.valuationSubring.comap (algebraMap K L) =
      base.valuation.valuationSubring

theorem

comap_valuationSubring_eq_base_of_hasExtension

L193 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.comap_valuationSubring_eq_base_of_hasExtension

Documentation

Any valuation extending the base valuation has valuation subring pulling back to the base valuation subring.

Source context 9 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Pullback
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem comap_valuationSubring_eq_base_of_hasExtension
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') [base.valuation.HasExtension v'] :
    v'.valuationSubring.comap (algebraMap K L) =
      base.valuation.valuationSubring

theorem

valuation_isEquiv_of_valuationSubring_eq

L210 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.valuation_isEquiv_of_valuationSubring_eq

Documentation

Equality of valuation subrings implies valuation equivalence.

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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Comparison
variable (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuation_isEquiv_of_valuationSubring_eq
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma')
    (hsub : target.valuation.valuationSubring = v'.valuationSubring) :
    target.valuation.IsEquiv v'

theorem

valuationSubring_eq_of_valuation_isEquiv

L218 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Comparison
variable (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuationSubring_eq_of_valuation_isEquiv
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    {v' : _root_.Valuation L Gamma'}
    (h : target.valuation.IsEquiv v') :
    target.valuation.valuationSubring = v'.valuationSubring

theorem

valuation_isEquiv_iff_valuationSubring_eq

L226 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Comparison
variable (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuation_isEquiv_iff_valuationSubring_eq
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') :
    target.valuation.IsEquiv v' ↔
      target.valuation.valuationSubring = v'.valuationSubring

theorem

valuationSubring_eq_iff_mem_valuationSubring

L234 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.valuationSubring_eq_iff_mem_valuationSubring

Documentation

Equality of valuation subrings is pointwise equality of membership.

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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Comparison
variable (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuationSubring_eq_iff_mem_valuationSubring
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') :
    target.valuation.valuationSubring = v'.valuationSubring ↔
      ∀ z : L, z ∈ target.valuation.valuationSubring ↔
        z ∈ v'.valuationSubring

theorem

valuation_isEquiv_iff_mem_valuationSubring

L247 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.valuation_isEquiv_iff_mem_valuationSubring

Documentation

Valuation equivalence can be checked pointwise on valuation-ring membership.

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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Comparison
variable (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuation_isEquiv_iff_mem_valuationSubring
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma') :
    target.valuation.IsEquiv v' ↔
      ∀ z : L, z ∈ target.valuation.valuationSubring ↔
        z ∈ v'.valuationSubring

theorem

valuation_isEquiv_of_mem_valuationSubring_iff

L258 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.valuation_isEquiv_of_mem_valuationSubring_iff

Documentation

A pointwise valuation-ring membership criterion gives valuation equivalence.

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 ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
section Comparison
variable (target : CompleteDVF.{w, x} L)

Lean source · statement

theorem valuation_isEquiv_of_mem_valuationSubring_iff
    {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
    (v' : _root_.Valuation L Gamma')
    (hmem : ∀ z : L,
      z ∈ target.valuation.valuationSubring ↔ z ∈ v'.valuationSubring) :
    target.valuation.IsEquiv v'

Module documentation

Valuation extensions

Declarations