NYLL
Module

AmbientUniformizer.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.AmbientUniformizer
6 declarations indexed from sourceView source ↗

Module documentation

Uniformizers detected in an ambient complete discrete valuation field

An embedding into an ambient complete DVF can make a uniformizer easier to recognize. For a finite separable extension, uniqueness of the extended valuation transports that recognition back to the chosen valuation.

Imports1
Imported by2

Declarations

def

valuationSubringMapOfIsEquivComap

L34 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.valuationSubringMapOfIsEquivComap
Documentation

An embedding into an ambient valued field restricts to valuation rings whenever the chosen source valuation is equivalent to the pulled-back ambient 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 z
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
Lean source · full declaration
def valuationSubringMapOfIsEquivComap
    {M : Type y} [Field M]
    {GammaL : Type x} {GammaM : Type z}
    [LinearOrderedCommGroupWithZero GammaL]
    [LinearOrderedCommGroupWithZero GammaM]
    (vL : _root_.Valuation L GammaL)
    (vM : _root_.Valuation M GammaM)
    (ι : L →+* M)
    (hEquiv : vL.IsEquiv (vM.comap ι)) :
    vL.valuationSubring →+* vM.valuationSubring where
  toFun a :=
    ⟨ι (a : L), by
      have ha :
          vL (a : L) ≤ vL 1 :=
        by
          rw [map_one]
          exact a.property
      have hcomap :=
        (hEquiv.le_iff_le
          (x := (a : L)) (y := (1 : L))).1 ha
      change vM (ι (a : L)) ≤ 1
      simpa only [_root_.Valuation.comap_apply, map_one] using hcomap⟩
  map_one' := by
    apply Subtype.ext
    simp
  map_mul' a b := by
    apply Subtype.ext
    simp
  map_zero' := by
    apply Subtype.ext
    simp
  map_add' a b := by
    apply Subtype.ext
    simp
theorem

valuationSubringMapOfIsEquivComap_apply

L72 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.valuationSubringMapOfIsEquivComap_apply
Documentation

The valuation-ring map induced by an equivalent ambient pullback acts through the original field embedding.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y z
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
Lean source · statement
theorem valuationSubringMapOfIsEquivComap_apply
    {M : Type y} [Field M]
    {GammaL : Type x} {GammaM : Type z}
    [LinearOrderedCommGroupWithZero GammaL]
    [LinearOrderedCommGroupWithZero GammaM]
    (vL : _root_.Valuation L GammaL)
    (vM : _root_.Valuation M GammaM)
    (ι : L →+* M)
    (hEquiv : vL.IsEquiv (vM.comap ι))
    (a : vL.valuationSubring) :
    ((valuationSubringMapOfIsEquivComap vL vM ι hEquiv a :
      vM.valuationSubring) : M) =
      ι (a : L)
theorem

valuationSubringMapOfIsEquivComap_isLocalHom

L89 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.valuationSubringMapOfIsEquivComap_isLocalHom
Documentation

The valuation-ring map induced by an equivalent ambient pullback is a local homomorphism.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y z
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
Lean source · statement
theorem valuationSubringMapOfIsEquivComap_isLocalHom
    {M : Type y} [Field M]
    {GammaL : Type x} {GammaM : Type z}
    [LinearOrderedCommGroupWithZero GammaL]
    [LinearOrderedCommGroupWithZero GammaM]
    (vL : _root_.Valuation L GammaL)
    (vM : _root_.Valuation M GammaM)
    (ι : L →+* M)
    (hEquiv : vL.IsEquiv (vM.comap ι)) :
    IsLocalHom
      (valuationSubringMapOfIsEquivComap vL vM ι hEquiv)
def

residueFieldMapOfIsEquivComap

L117 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldMapOfIsEquivComap
Documentation

The induced injection from the chosen residue field into the ambient residue field.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y z
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
Lean source · statement
def residueFieldMapOfIsEquivComap
    {M : Type y} [Field M]
    {GammaL : Type x} {GammaM : Type z}
    [LinearOrderedCommGroupWithZero GammaL]
    [LinearOrderedCommGroupWithZero GammaM]
    (vL : _root_.Valuation L GammaL)
    (vM : _root_.Valuation M GammaM)
    (ι : L →+* M)
    (hEquiv : vL.IsEquiv (vM.comap ι)) :
    IsLocalRing.ResidueField vL.valuationSubring →+*
      IsLocalRing.ResidueField vM.valuationSubring
theorem

residueFieldMapOfIsEquivComap_mapEquiv

L140 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueFieldMapOfIsEquivComap_mapEquiv
Documentation

Reduction modulo the maximal ideal commutes with compatible automorphisms of the source and ambient valuation rings. This is the residue-field naturality needed when a finite valued subfield is realized inside a larger complete discrete valuation field.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y z
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
Lean source · statement
theorem residueFieldMapOfIsEquivComap_mapEquiv
    {M : Type y} [Field M]
    {GammaL : Type x} {GammaM : Type z}
    [LinearOrderedCommGroupWithZero GammaL]
    [LinearOrderedCommGroupWithZero GammaM]
    (vL : _root_.Valuation L GammaL)
    (vM : _root_.Valuation M GammaM)
    (ι : L →+* M)
    (hEquiv : vL.IsEquiv (vM.comap ι))
    (σL : vL.valuationSubring ≃+* vL.valuationSubring)
    (σM : vM.valuationSubring ≃+* vM.valuationSubring)
    (hcompat :
      ∀ a : vL.valuationSubring,
        valuationSubringMapOfIsEquivComap vL vM ι hEquiv (σL a) =
          σM
            (valuationSubringMapOfIsEquivComap
              vL vM ι hEquiv a))
    (a : IsLocalRing.ResidueField vL.valuationSubring) :
    residueFieldMapOfIsEquivComap vL vM ι hEquiv
        (IsLocalRing.ResidueField.mapEquiv σL a) =
      IsLocalRing.ResidueField.mapEquiv σM
        (residueFieldMapOfIsEquivComap vL vM ι hEquiv a)
theorem

isUniformizer_of_ambient_image_isUniformizer

L195 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isUniformizer_of_ambient_image_isUniformizer
Documentation

Let L / K be finite separable with a chosen complete discrete valuation extending the one on K. If a field embedding of L into another complete DVF sends π to an ambient uniformizer, and the pulled-back ambient valuation also extends the base valuation, then π is a uniformizer for the chosen valuation on L.

The proof first uses uniqueness of valuation extension to compare the chosen valuation with the ambient comap valuation. It then pulls divisibility by the ambient uniformizer back through the field embedding, proving that π generates the chosen maximal ideal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v w x y z
namespace DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
Lean source · statement
theorem isUniformizer_of_ambient_image_isUniformizer
    {M : Type y} [Field M]
    (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
    (ambient : CompleteDVF.{y, z} M)
    [base.valuation.HasExtension target.valuation]
    (ι : L →+* M)
    [base.valuation.HasExtension (ambient.valuation.comap ι)]
    {π : L} (hπ : ambient.valuation.IsUniformizer (ι π)) :
    target.valuation.IsUniformizer π

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