Module

Core.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Core

25 declarations indexed from sourceView source ↗

Module documentation

Uniqueness criteria for extensions of Henselian discrete valuations

The integral closure of the base valuation ring supplies the valuation subring used to compare extensions. Local maximal-ideal centers and subsingleton fibers lead to uniqueness criteria, including criteria obtained from Henselian quotient maps, adic completeness, and finite-separable extensions.

Imports2

Imported by8

def

integralClosureValuationSubringIntegerMapOfMemOrInv

L36 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosureValuationSubringIntegerMapOfMemOrInv

Documentation

The canonical integer map from a Henselian base valuation ring to the valuation subring constructed from the actual integral closure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · full declaration

def integralClosureValuationSubringIntegerMapOfMemOrInv
    (base : HenselianDVF.{u, v} K)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    base.valuationSubring →+*
      ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
        (L := L) base.toDVF.valuation hval where
  toFun a :=
    ⟨algebraMap K L (a : K),
      (Valuation.integralClosureValuationSubringOfMemOrInv_pullback
        (L := L) base.toDVF.valuation hval (a : K)).2 a.2⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_add' := by intro a b; ext; simp
  map_mul' := by intro a b; ext; simp

theorem

integralClosureValuationSubringIntegerMapOfMemOrInv_apply

L56 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosureValuationSubringIntegerMapOfMemOrInv_apply

Documentation

The integer map into the integral-closure valuation ring is the ambient algebra map.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureValuationSubringIntegerMapOfMemOrInv_apply
    (base : HenselianDVF.{u, v} K)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (a : base.valuationSubring) :
    ((integralClosureValuationSubringIntegerMapOfMemOrInv
      (K := K) (L := L) base hval a :
        ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
          (L := L) base.toDVF.valuation hval) : L) =
      algebraMap K L (a : K)

theorem

integralClosureValuationSubringIntegerMapOfMemOrInv_injective

L73 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosureValuationSubringIntegerMapOfMemOrInv_injective

Documentation

The canonical integer map into the valuation subring built from the actual integral closure is injective.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem integralClosureValuationSubringIntegerMapOfMemOrInv_injective
    (base : HenselianDVF.{u, v} K)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    Function.Injective
      (integralClosureValuationSubringIntegerMapOfMemOrInv
        (K := K) (L := L) base hval)

theorem

idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

L94 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

Documentation

The center of an extension valuation ring on the constructed actual integral-closure valuation subring contracts to the base maximal ideal.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L] in

Lean source · full declaration

theorem idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (base : HenselianDVF.{u, v} K) (vL : _root_.Valuation L ΓL)
    [base.toDVF.valuation.HasExtension vL]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    let B :=
      ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
        (L := L) base.toDVF.valuation hval
    let hvL_le : B ≤ vL.valuationSubring :=
      Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
        (L := L) base.toDVF.valuation vL hval
    (ValuationSubring.idealOfLE B vL.valuationSubring hvL_le).comap
        (integralClosureValuationSubringIntegerMapOfMemOrInv
          (K := K) (L := L) base hval) =
      base.maximalIdeal := by
  let B :=
    ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
      (L := L) base.toDVF.valuation hval
  let hvL_le : B ≤ vL.valuationSubring :=
    Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
      (L := L) base.toDVF.valuation vL hval
  let i : base.valuationSubring →+* B :=
    integralClosureValuationSubringIntegerMapOfMemOrInv
      (K := K) (L := L) base hval
  apply Ideal.ext
  intro a
  rw [Ideal.mem_comap]
  change B.inclusion vL.valuationSubring hvL_le (i a) ∈
      IsLocalRing.maximalIdeal vL.valuationSubring ↔
    a ∈ IsLocalRing.maximalIdeal base.toDVF.valuation.valuationSubring
  rw [Valuation.mem_maximalIdeal_iff (v := vL)]
  rw [Valuation.mem_maximalIdeal_iff (v := base.toDVF.valuation)]
  have hcoe :
      ((B.inclusion vL.valuationSubring hvL_le (i a) :
        vL.valuationSubring) : L) =
        algebraMap K L (a : K) := by
    rfl
  rw [hcoe]
  exact Valuation.HasExtension.val_map_lt_one_iff base.toDVF.valuation vL (a : K)

theorem

prime_eq_maximalIdeal_of_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

L140 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.prime_eq_maximalIdeal_of_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal

Documentation

In a finite separable extension, once the actual integral closure has the valuation-ring dichotomy, the constructed integral-closure valuation ring has a unique prime over the base maximal ideal.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem prime_eq_maximalIdeal_of_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal
    (base : HenselianDVF.{u, v} K)
    [Algebra.IsSeparable K L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (P :
      Ideal
        (ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
          (L := L) base.toDVF.valuation hval))
    (hP : P.IsPrime)
    (hcomap :
      P.comap
          (integralClosureValuationSubringIntegerMapOfMemOrInv
            (K := K) (L := L) base hval) =
        base.maximalIdeal) :
    P =
      IsLocalRing.maximalIdeal
        (ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
          (L := L) base.toDVF.valuation hval)

theorem

hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_forall_center_eq_maximalIdeal

L209 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_forall_center_eq_maximalIdeal

Documentation

Center-equality form of Henselian-DVF valuation uniqueness after the actual integral closure has been turned into a valuation subring.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_forall_center_eq_maximalIdeal
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (htargetCenter :
      ValuationSubring.idealOfLE
        (ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
          (L := L) base.toDVF.valuation hval)
        target.toDVF.valuation.valuationSubring
        (Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
          (L := L) base.toDVF.valuation target.toDVF.valuation hval) =
        IsLocalRing.maximalIdeal
          (Valuation.integralClosureValuationSubringOfMemOrInv
            (L := L) base.toDVF.valuation hval))
    (hcenter :
      ∀ {Gamma' : Type y} [LinearOrderedCommGroupWithZero Gamma']
        (v' : _root_.Valuation L Gamma') [base.toDVF.valuation.HasExtension v'],
          ValuationSubring.idealOfLE
            (Valuation.integralClosureValuationSubringOfMemOrInv
              (L := L) base.toDVF.valuation hval)
            v'.valuationSubring
            (Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
              (L := L) base.toDVF.valuation v' hval) =
            IsLocalRing.maximalIdeal
              (Valuation.integralClosureValuationSubringOfMemOrInv
                (L := L) base.toDVF.valuation hval)) :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_unique_primes_over_base_maximal

L262 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_unique_primes_over_base_maximal

Documentation

Prime-uniqueness form of Henselian-DVF valuation uniqueness.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [FiniteDimensional K L] in

Lean source · full declaration

theorem hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_unique_primes_over_base_maximal
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring)
    (hunique :
      let B :=
        ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
          (L := L) base.toDVF.valuation hval
      let i : base.valuationSubring →+* B :=
        integralClosureValuationSubringIntegerMapOfMemOrInv
          (K := K) (L := L) base hval
      ∀ P : Ideal B, P.IsPrime → P.comap i = base.maximalIdeal →
        P = IsLocalRing.maximalIdeal B) :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target := by
  let B :=
    ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
      (L := L) base.toDVF.valuation hval
  let i : base.valuationSubring →+* B :=
    integralClosureValuationSubringIntegerMapOfMemOrInv
      (K := K) (L := L) base hval
  refine
    (hasUniqueValuationExtension_of_integralClosure_mem_or_inv_of_forall_center_eq_maximalIdeal
      (K := K) (L := L) (base := base) (target := target)  hval ?_ ?_ :
        HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target)
  · let htarget_le : B ≤ target.toDVF.valuation.valuationSubring :=
      Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
        (L := L) base.toDVF.valuation target.toDVF.valuation hval
    exact hunique
      (ValuationSubring.idealOfLE B target.toDVF.valuation.valuationSubring htarget_le)
      (by infer_instance)
      (by
        simpa [B, htarget_le, i] using
          idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal
            (K := K) (L := L) base target.toDVF.valuation hval)
  · intro Gamma' _ v' hExt
    let : base.toDVF.valuation.HasExtension v' := hExt
    let hv_le : B ≤ v'.valuationSubring :=
      Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
        (L := L) base.toDVF.valuation v' hval
    exact hunique
      (ValuationSubring.idealOfLE B v'.valuationSubring hv_le)
      (by infer_instance)
      (by
        simpa [B, hv_le, i] using
          idealOfLE_comap_integralClosureValuationSubringIntegerMap_eq_maximalIdeal
            (K := K) (L := L) base v' hval)

theorem

hasUniqueValuationExtension_of_integralClosure_mem_or_inv

L312 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_mem_or_inv

Documentation

Finite-separable Henselian-DVF uniqueness once the actual integral closure has the valuative dichotomy.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_integralClosure_mem_or_inv
    [Algebra.IsSeparable K L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuationSubring L).toSubring) :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_integralClosure_isLocalRing

L338 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_isLocalRing

Documentation

Finite-separable Henselian-DVF uniqueness once the actual integral closure is local.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_integralClosure_isLocalRing
    [Algebra.IsSeparable K L]
    [IsLocalRing (integralClosureIntegers base target)] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_subsingleton

L347 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_subsingleton

Documentation

Finite-separable Henselian-DVF uniqueness once the residue fiber over the base maximal ideal has at most one prime.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_subsingleton
    [Algebra.IsSeparable K L]
    [Subsingleton
      (PrimeSpectrum (base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_idempotents_lift

L361 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_idempotents_lift

Documentation

Finite-separable Henselian-DVF uniqueness from idempotent lifting in the residue fiber over the base maximal ideal.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_idempotents_lift
    [Algebra.IsSeparable K L]
    (hlift :
      ∀ e : base.maximalIdeal.Fiber (integralClosureIntegers base target),
        IsIdempotentElem e →
          ∃ b : (integralClosureIntegers base target),
            IsIdempotentElem b ∧
              Algebra.TensorProduct.includeRight b = e) :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

unique_of_includeRight_surjective_henselianRing_ker

L380 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.IntegralClosureFiber.unique_of_includeRight_surjective_henselianRing_ker

Documentation

Finite-separable Henselian-DVF uniqueness from the Henselian-kernel idempotent-lifting criterion for the residue-fiber includeRight map.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem IntegralClosureFiber.unique_of_includeRight_surjective_henselianRing_ker
    [Algebra.IsSeparable K L]
    (hsurj :
      Function.Surjective
        (Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_includeRight_henselianRing_ker

L408 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_includeRight_henselianRing_ker

Documentation

Finite-separable Henselian-DVF uniqueness from the Henselian-kernel criterion for the residue-fiber includeRight map. Surjectivity of includeRight is supplied by the local base valuation ring.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem
  hasUniqueValuationExtension_of_integralClosure_base_maximal_fiber_includeRight_henselianRing_ker
    [Algebra.IsSeparable K L]
    [HenselianRing (integralClosureIntegers base target)
      (RingHom.ker
        ((Algebra.TensorProduct.includeRight :
          (integralClosureIntegers base target) →ₐ[base.valuationSubring]
            base.maximalIdeal.Fiber (integralClosureIntegers base target)) :
          (integralClosureIntegers base target) →+*
            base.maximalIdeal.Fiber (integralClosureIntegers base target)))] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

integralClosure_base_maximal_map_henselianRing_of_isAdicComplete

L431 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_map_henselianRing_of_isAdicComplete

Documentation

If the base Henselian-DVF valuation ring is actually complete for its maximal-ideal topology, then the actual integral closure is Henselian along the ideal generated by the base maximal ideal.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_map_henselianRing_of_isAdicComplete
    [Algebra.IsSeparable K L]
    [IsAdicComplete base.maximalIdeal base.valuationSubring] :
    HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.valuationSubring (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_map_henselianRing_of_base_isPrecomplete

L454 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_map_henselianRing_of_base_isPrecomplete

Documentation

If the base Henselian-DVF valuation ring is precomplete for its maximal-ideal topology, then the actual integral closure is Henselian along the ideal generated by the base maximal ideal.

The separatedness needed upstairs is derived from the Henselian Jacobson condition and finite generation, so this does not assume base adic completeness.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_map_henselianRing_of_base_isPrecomplete
    [Algebra.IsSeparable K L]
    [IsPrecomplete base.maximalIdeal base.valuationSubring] :
    HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.valuationSubring (integralClosureIntegers base target)))

theorem

integralClosure_base_maximal_map_henselianRing_of_finiteTransfer

L487 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.integralClosure_base_maximal_map_henselianRing_of_finiteTransfer

Documentation

The actual integral closure is Henselian once finite-algebra transfer is available over the base valuation ring.

This is the CFT-facing specialization of the finite-algebra transfer frontier: the actual integral closure is module-finite over the Henselian base valuation ring in a finite separable extension, so the monogenic AdjoinRoot transfer route constructed in Henselian.lean gives the natural Henselian pair upstairs.

Source context 10 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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]
omit [base.toDVF.valuation.HasExtension target.toDVF.valuation] in

Lean source · statement

theorem integralClosure_base_maximal_map_henselianRing_of_finiteTransfer
    [Algebra.IsSeparable K L]
    (hTransfer :
      ∀ {T : Type w} [CommRing T] [Algebra base.valuationSubring T]
        [Module.Finite base.valuationSubring T],
          HenselianRing T
            (base.maximalIdeal.map
              (algebraMap base.valuationSubring T))) :
    HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.valuationSubring (integralClosureIntegers base target)))

theorem

hasUniqueValuationExtension_of_integralClosure_base_maximal_map_henselianRing

L507 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_integralClosure_base_maximal_map_henselianRing

Documentation

Finite-separable Henselian-DVF uniqueness from the natural Henselian-pair ideal in the actual integral closure.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_integralClosure_base_maximal_map_henselianRing
    [Algebra.IsSeparable K L]
    [HenselianRing (integralClosureIntegers base target)
      (base.maximalIdeal.map
        (algebraMap base.valuationSubring (integralClosureIntegers base target)))] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_finite_separable_of_base_isAdicComplete

L526 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_finite_separable_of_base_isAdicComplete

Documentation

Finite-separable Henselian-DVF uniqueness for bases that are complete for the maximal-ideal topology. This is the actual-integral-closure specialization of finite-algebra transfer in the complete-base case.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_finite_separable_of_base_isAdicComplete
    [Algebra.IsSeparable K L]
    [IsAdicComplete base.maximalIdeal base.valuationSubring] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_finite_separable_of_base_isPrecomplete

L543 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_finite_separable_of_base_isPrecomplete

Documentation

Finite-separable Henselian-DVF uniqueness for bases whose valuation ring is precomplete for the maximal-ideal topology. This is the CFT-facing specialization of finite-algebra transfer with separatedness derived from the Henselian Jacobson condition.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_finite_separable_of_base_isPrecomplete
    [Algebra.IsSeparable K L]
    [IsPrecomplete base.maximalIdeal base.valuationSubring] :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

hasUniqueValuationExtension_of_finite_separable_of_finiteTransfer

L563 ↗

ValuationTheory.DiscreteValuationField.ValuedExtension.Henselian.hasUniqueValuationExtension_of_finite_separable_of_finiteTransfer

Documentation

Finite-separable Henselian-DVF valuation uniqueness once finite-algebra Henselian transfer is available over the base valuation ring.

This is the downstream CFT specialization of the current finite-algebra frontier: finite transfer gives the Henselian pair on the actual integral closure, and the existing residue-fiber/localness argument then gives uniqueness of the extended valuation.

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.Henselian
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
variable [base.toDVF.valuation.HasExtension target.toDVF.valuation]

Lean source · statement

theorem hasUniqueValuationExtension_of_finite_separable_of_finiteTransfer
    [Algebra.IsSeparable K L]
    (hTransfer :
      ∀ {T : Type w} [CommRing T] [Algebra base.valuationSubring T]
        [Module.Finite base.valuationSubring T],
          HenselianRing T
            (base.maximalIdeal.map
              (algebraMap base.valuationSubring T))) :
    HenselianDVF.HasUniqueValuationExtension.{u, v, w, x, y} base target

theorem

valuationSubring_eq_of_finite_separable_of_forall_isIntegral

L595 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_eq_of_finite_separable_of_forall_isIntegral

Documentation

Target-free finite-separable valuation-subring uniqueness, reduced to the remaining Henselian integrality frontier.

Once every valuation subring extending the base valuation is integral over the base valuation ring, any two such valuation subrings coincide. This is the B C : ValuationSubring L form needed by the absolute route, without packaging either side as a target HenselianDVF.

Source context 6 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} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valuationSubring_eq_of_finite_separable_of_forall_isIntegral
    (base : HenselianDVF.{u, v} K)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hintegral :
      ∀ (B : ValuationSubring L)
        [_root_.Valuation.HasExtension base.valuation B.valuation],
          Algebra.IsIntegral base.valuation.valuationSubring
            B.valuation.valuationSubring)
    (B C : ValuationSubring L)
    [_root_.Valuation.HasExtension base.valuation B.valuation]
    [_root_.Valuation.HasExtension base.valuation C.valuation] :
    B = C

theorem

valuationSubring_eq_of_finite_separable_of_forall_moduleFinite

L639 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_eq_of_finite_separable_of_forall_moduleFinite

Documentation

Target-free finite-separable valuation-subring uniqueness from finite valuation-ring extensions.

This is the module-finite form of valuationSubring_eq_of_finite_separable_of_forall_isIntegral; finite valuation-ring extensions are converted to integral extensions before applying the integral uniqueness route.

Source context 6 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} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valuationSubring_eq_of_finite_separable_of_forall_moduleFinite
    (base : HenselianDVF.{u, v} K)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hfinite :
      ∀ (B : ValuationSubring L)
        [_root_.Valuation.HasExtension base.valuation B.valuation],
          Module.Finite base.valuation.valuationSubring
            B.valuation.valuationSubring)
    (B C : ValuationSubring L)
    [_root_.Valuation.HasExtension base.valuation B.valuation]
    [_root_.Valuation.HasExtension base.valuation C.valuation] :
    B = C

theorem

valuationSubring_eq_integralClosureValuationSubring_of_finite_separable

L668 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_eq_integralClosureValuationSubring_of_finite_separable

Documentation

In a finite separable extension, the target-free uniqueness theorem identifies every extension valuation subring with the valuation subring constructed from the actual integral closure.

The remaining upstream input is explicit: every valuation subring extending the base valuation must be integral over the base valuation ring, and the actual integral closure must satisfy the valuation-ring dichotomy.

Source context 6 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} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valuationSubring_eq_integralClosureValuationSubring_of_finite_separable
    (base : HenselianDVF.{u, v} K)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hval :
      ∀ z : L,
        z ∈ (integralClosure base.valuation.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure base.valuation.valuationSubring L).toSubring)
    (hintegral :
      ∀ (B : ValuationSubring L)
        [_root_.Valuation.HasExtension base.valuation B.valuation],
          Algebra.IsIntegral base.valuation.valuationSubring
            B.valuation.valuationSubring)
    (B : ValuationSubring L)
    [_root_.Valuation.HasExtension base.valuation B.valuation] :
    B =
      ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
        (L := L) base.valuation hval

theorem

mem_valuationSubring_iff_of_finite_separable_of_forall_isIntegral

L697 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.mem_valuationSubring_iff_of_finite_separable_of_forall_isIntegral

Documentation

Elementwise form of valuationSubring_eq_of_finite_separable_of_forall_isIntegral.

Source context 6 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} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_valuationSubring_iff_of_finite_separable_of_forall_isIntegral
    (base : HenselianDVF.{u, v} K)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hintegral :
      ∀ (B : ValuationSubring L)
        [_root_.Valuation.HasExtension base.valuation B.valuation],
          Algebra.IsIntegral base.valuation.valuationSubring
            B.valuation.valuationSubring)
    (B C : ValuationSubring L)
    [_root_.Valuation.HasExtension base.valuation B.valuation]
    [_root_.Valuation.HasExtension base.valuation C.valuation]
    (z : L) :
    z ∈ B ↔ z ∈ C

theorem

mem_valuationSubring_iff_of_finite_separable_of_forall_moduleFinite

L715 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.mem_valuationSubring_iff_of_finite_separable_of_forall_moduleFinite

Documentation

Elementwise form of valuationSubring_eq_of_finite_separable_of_forall_moduleFinite.

Source context 6 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} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_valuationSubring_iff_of_finite_separable_of_forall_moduleFinite
    (base : HenselianDVF.{u, v} K)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hfinite :
      ∀ (B : ValuationSubring L)
        [_root_.Valuation.HasExtension base.valuation B.valuation],
          Module.Finite base.valuation.valuationSubring
            B.valuation.valuationSubring)
    (B C : ValuationSubring L)
    [_root_.Valuation.HasExtension base.valuation B.valuation]
    [_root_.Valuation.HasExtension base.valuation C.valuation]
    (z : L) :
    z ∈ B ↔ z ∈ C

Module documentation

Uniqueness criteria for extensions of Henselian discrete valuations

Declarations