NYLL
Module

ChevalleyExtension.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ChevalleyExtension
70 declarations indexed from sourceView source ↗

Module documentation

Chevalley's valuation extension theorem

Mathlib has the predicate Valuation.HasExtension and the induced valuation subring/residue-field API. This file proves the field-extension form of Chevalley's valuation extension theorem from mathlib's maximal local subring construction: a local subring of a field is dominated by a valuation subring.

Imports4
Imported by15

Declarations

def

HasSomeExtensionTo

L39 ↗
ValuationTheory.DiscreteValuationField.Valuation.HasSomeExtensionTo
Documentation

A valuation on K has some extension to the field extension L / K.

Chevalley's extension theorem is precisely the general existence theorem for this predicate under algebraic field-extension hypotheses.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
def HasSomeExtensionTo (vK : _root_.Valuation K ΓK) : Prop
theorem

mem_base_valuationSubring_of_lift_mem

L47 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_base_valuationSubring_of_lift_mem
Documentation

If a valuation subring B of the extension field dominates the base valuation ring locally, then any base-field element whose image lies in B already lies in the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem mem_base_valuationSubring_of_lift_mem
    (vK : _root_.Valuation K ΓK)
    (B : ValuationSubring L)
    (hB : ∀ x : vK.valuationSubring, algebraMap vK.valuationSubring L x ∈ B.toSubring)
    (hlocal : IsLocalHom
      ((algebraMap vK.valuationSubring L).codRestrict B.toSubring hB))
    {x : K} (hxB : algebraMap K L x ∈ B.toSubring) :
    x ∈ vK.valuationSubring
theorem

exists_extension_valuationSubring

L86 ↗
ValuationTheory.DiscreteValuationField.Valuation.exists_extension_valuationSubring
Documentation

Chevalley's theorem in valuation-subring form.

For any field extension L / K, a valuation subring of K admits a dominating valuation subring of L, and the original valuation subring is exactly the pullback of the extension valuation subring along K → L. This is the construction-level statement behind chevalley_hasSomeExtensionTo; downstream finite-extension arguments can use the returned subring B before passing to its canonical valuation.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem exists_extension_valuationSubring
    (vK : _root_.Valuation K ΓK) :
    ∃ B : ValuationSubring L,
      ∃ hB : ∀ x : vK.valuationSubring,
        algebraMap vK.valuationSubring L x ∈ B.toSubring,
        IsLocalHom
          ((algebraMap vK.valuationSubring L).codRestrict B.toSubring hB) ∧
        ∀ x : K, algebraMap K L x ∈ B.toSubring ↔
          x ∈ vK.valuationSubring
theorem

hasExtension_valuation_of_valuationSubring_pullback

L113 ↗
ValuationTheory.DiscreteValuationField.Valuation.hasExtension_valuation_of_valuationSubring_pullback
Documentation

Exact pullback of valuation subrings gives a HasExtension proof for the canonical valuation attached to the target 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem hasExtension_valuation_of_valuationSubring_pullback
    (vK : _root_.Valuation K ΓK) (B : ValuationSubring L)
    (hpullback : ∀ x : K, algebraMap K L x ∈ B.toSubring ↔
      x ∈ vK.valuationSubring) :
    vK.HasExtension B.valuation
theorem

valuationSubring_pullback_of_hasExtension_valuation

L135 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_pullback_of_hasExtension_valuation
Documentation

A HasExtension proof for the canonical valuation attached to a valuation subring gives exact pullback 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_pullback_of_hasExtension_valuation
    (vK : _root_.Valuation K ΓK) (B : ValuationSubring L)
    [vK.HasExtension B.valuation] (x : K) :
    algebraMap K L x ∈ B.toSubring ↔ x ∈ vK.valuationSubring
theorem

hasExtension_valuation_iff_valuationSubring_pullback

L155 ↗
ValuationTheory.DiscreteValuationField.Valuation.hasExtension_valuation_iff_valuationSubring_pullback
Documentation

For the canonical valuation attached to a valuation subring of the target field, HasExtension is equivalent to exact pullback 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem hasExtension_valuation_iff_valuationSubring_pullback
    (vK : _root_.Valuation K ΓK) (B : ValuationSubring L) :
    vK.HasExtension B.valuation ↔
      ∀ x : K, algebraMap K L x ∈ B.toSubring ↔
        x ∈ vK.valuationSubring
theorem

integralClosure_mem_valuationSubring_of_hasExtension

L170 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosure_mem_valuationSubring_of_hasExtension
Documentation

Every element integral over the base valuation ring lies in any valuation ring extending the base valuation. This is the valuation-theoretic integral closure bridge used before specializing to complete or Henselian DVFs.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosure_mem_valuationSubring_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] (z : integralClosure vK.valuationSubring L) :
    (z : L) ∈ vL.valuationSubring
theorem

algebraMap_mem_integralClosure_valuationSubring_iff

L190 ↗
ValuationTheory.DiscreteValuationField.Valuation.algebraMap_mem_integralClosure_valuationSubring_iff
Documentation

The actual integral closure over the base valuation ring has exact pullback to the base field: a base-field element is integral over the base valuation ring in the extension field exactly when it already belongs to the base valuation ring.

This is the construction-level input needed to turn the actual integral closure into a valuation subring extending vK once the Henselian frontier proves the valuative dichotomy for that integral closure.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem algebraMap_mem_integralClosure_valuationSubring_iff
    (vK : _root_.Valuation K ΓK) (a : K) :
    algebraMap K L a ∈ (integralClosure vK.valuationSubring L).toSubring ↔
      a ∈ vK.valuationSubring
def

integralClosureValuationSubringOfMemOrInv

L222 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv
Documentation

If the actual integral closure over the base valuation ring satisfies the valuation-ring dichotomy inside the extension field, then it is the underlying subring of an actual ValuationSubring L.

This is not a replacement for the Henselian uniqueness theorem: the remaining frontier is to prove the dichotomy from Henselian hypotheses. The theorem constructs the valuation object that that proof will feed into.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
def integralClosureValuationSubringOfMemOrInv
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring) :
    ValuationSubring L
theorem

mem_integralClosureValuationSubringOfMemOrInv

L233 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_integralClosureValuationSubringOfMemOrInv
Documentation

The Chevalley valuation ring contains every integral element or its inverse.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem mem_integralClosureValuationSubringOfMemOrInv
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring)
    (z : L) :
    z ∈ integralClosureValuationSubringOfMemOrInv (L := L) vK hval ↔
      z ∈ (integralClosure vK.valuationSubring L).toSubring
theorem

integralClosureValuationSubringOfMemOrInv_pullback

L246 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv_pullback
Documentation

The valuation subring built from the actual integral closure has exact base-field pullback.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureValuationSubringOfMemOrInv_pullback
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring)
    (a : K) :
    algebraMap K L a ∈
        integralClosureValuationSubringOfMemOrInv (L := L) vK hval ↔
      a ∈ vK.valuationSubring
theorem

integralClosureValuationSubringOfMemOrInv_hasExtension

L262 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv_hasExtension
Documentation

Once the actual integral closure over the base valuation ring has been proved to be a valuation subring, its canonical valuation is an extension of the base valuation.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureValuationSubringOfMemOrInv_hasExtension
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring) :
    vK.HasExtension
      (integralClosureValuationSubringOfMemOrInv (L := L) vK hval).valuation
theorem

integralClosureValuationSubringOfMemOrInv_isIntegralClosure

L282 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv_isIntegralClosure
Documentation

The valuation subring built from the actual integral closure is the actual integral closure of the base valuation ring in the extension field.

This removes the earlier packaging gap: after the Henselian frontier supplies the valuative dichotomy for integralClosure vK.valuationSubring L, the constructed valuation subring carries the canonical extension valuation and satisfies the defining IsIntegralClosure equivalence, not merely equality of underlying 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · full declaration
theorem integralClosureValuationSubringOfMemOrInv_isIntegralClosure
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring) :
    let B := integralClosureValuationSubringOfMemOrInv (L := L) vK hval
    letI : vK.HasExtension B.valuation :=
      integralClosureValuationSubringOfMemOrInv_hasExtension (L := L) vK hval
    IsIntegralClosure B vK.valuationSubring L := by
  let B := integralClosureValuationSubringOfMemOrInv (L := L) vK hval
  let : vK.HasExtension B.valuation :=
    integralClosureValuationSubringOfMemOrInv_hasExtension (L := L) vK hval
  change IsIntegralClosure B vK.valuationSubring L
  refine
    { algebraMap_injective := Subtype.coe_injective
      isIntegral_iff := ?_ }
  intro z
  constructor
  · intro hz
    refine ⟨⟨z, ?_⟩, ?_⟩
    · exact
        (mem_integralClosureValuationSubringOfMemOrInv
          (L := L) vK hval z).2 hz
    · rfl
  · rintro ⟨y, rfl⟩
    exact
      (mem_integralClosureValuationSubringOfMemOrInv
        (L := L) vK hval (y : L)).1 y.2
theorem

integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension

L314 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
Documentation

The integral-closure valuation subring is contained in every valuation subring whose canonical valuation extends the base valuation.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureValuationSubringOfMemOrInv_le_valuationSubring_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring)
    [vK.HasExtension vL] :
    integralClosureValuationSubringOfMemOrInv (L := L) vK hval ≤
      vL.valuationSubring
theorem

exists_integralClosure_valuationSubring_of_forall_mem_or_inv

L336 ↗
ValuationTheory.DiscreteValuationField.Valuation.exists_integralClosure_valuationSubring_of_forall_mem_or_inv
Documentation

Construction-level package for the integral-closure valuation subring: the actual integral closure, once it satisfies the valuation-ring dichotomy, is a valuation subring whose canonical valuation extends the base valuation.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem exists_integralClosure_valuationSubring_of_forall_mem_or_inv
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring) :
    ∃ B : ValuationSubring L,
      B.toSubring = (integralClosure vK.valuationSubring L).toSubring ∧
        vK.HasExtension B.valuation
theorem

exists_integralClosure_valuationSubring_isIntegralClosure_of_forall_mem_or_inv

L353 ↗
ValuationTheory.DiscreteValuationField.Valuation.exists_integralClosure_valuationSubring_isIntegralClosure_of_forall_mem_or_inv
Documentation

Construction-level package for the actual integral-closure valuation subring, including the integral-closure proof itself. The second witness is kept explicit so downstream proofs can install it as an instance only where they need the induced algebra structure from the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · full declaration
theorem exists_integralClosure_valuationSubring_isIntegralClosure_of_forall_mem_or_inv
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring) :
    ∃ B : ValuationSubring L,
      ∃ hExt : vK.HasExtension B.valuation,
        letI : vK.HasExtension B.valuation := hExt
        B.toSubring = (integralClosure vK.valuationSubring L).toSubring ∧
          IsIntegralClosure B vK.valuationSubring L := by
  let B := integralClosureValuationSubringOfMemOrInv (L := L) vK hval
  let hExt : vK.HasExtension B.valuation :=
    integralClosureValuationSubringOfMemOrInv_hasExtension (L := L) vK hval
  refine ⟨B, hExt, ?_⟩
  let : vK.HasExtension B.valuation := hExt
  exact ⟨rfl, integralClosureValuationSubringOfMemOrInv_isIntegralClosure
    (L := L) vK hval⟩
theorem

valuationSubring_eq_of_le_of_idealOfLE_eq_maximalIdeal

L376 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_eq_of_le_of_idealOfLE_eq_maximalIdeal
Documentation

A valuation overring of a valuation subring is equal to it when the corresponding localization prime is the maximal ideal of the smaller valuation subring. This is the prime-theoretic comparison bridge used after proving that an integral closure has a unique prime above the base maximal ideal.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_eq_of_le_of_idealOfLE_eq_maximalIdeal
    (R S : ValuationSubring L) (hRS : R ≤ S)
    (hcenter :
      ValuationSubring.idealOfLE R S hRS = IsLocalRing.maximalIdeal R) :
    S = R
theorem

idealOfLE_eq_maximalIdeal_of_mem_maximalIdeal_iff

L414 ↗
ValuationTheory.DiscreteValuationField.Valuation.idealOfLE_eq_maximalIdeal_of_mem_maximalIdeal_iff
Documentation

Elementwise form of the center condition for a valuation overring. The center idealOfLE R S hRS is the maximal ideal of R exactly when membership in the maximal ideal of S, after the inclusion R → S, agrees with membership in the maximal ideal of R.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem idealOfLE_eq_maximalIdeal_of_mem_maximalIdeal_iff
    (R S : ValuationSubring L) (hRS : R ≤ S)
    (hmem :
      ∀ x : R,
        R.inclusion S hRS x ∈ IsLocalRing.maximalIdeal S ↔
          x ∈ IsLocalRing.maximalIdeal R) :
    ValuationSubring.idealOfLE R S hRS = IsLocalRing.maximalIdeal R
theorem

valuationSubring_eq_of_le_of_mem_maximalIdeal_iff

L430 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_eq_of_le_of_mem_maximalIdeal_iff
Documentation

Elementwise maximal-ideal criterion for collapse of a valuation overring. This is the form used when the remaining Henselian argument proves equality of centers by checking elements, rather than by manipulating idealOfLE directly.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_eq_of_le_of_mem_maximalIdeal_iff
    (R S : ValuationSubring L) (hRS : R ≤ S)
    (hmem :
      ∀ x : R,
        R.inclusion S hRS x ∈ IsLocalRing.maximalIdeal S ↔
          x ∈ IsLocalRing.maximalIdeal R) :
    S = R
theorem

valuationSubring_eq_of_le_of_inclusion_isLocalHom

L443 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_eq_of_le_of_inclusion_isLocalHom
Documentation

A valuation overring of a valuation subring is equal to it as soon as the inclusion is local. This is the local-map form of valuationSubring_eq_of_le_of_idealOfLE_eq_maximalIdeal.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_eq_of_le_of_inclusion_isLocalHom
    (R S : ValuationSubring L) (hRS : R ≤ S)
    [IsLocalHom (R.inclusion S hRS)] :
    S = R
theorem

mem_integralClosure_baseRange_iff_forall_valuationSubring

L458 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_integralClosure_baseRange_iff_forall_valuationSubring
Documentation

Chevalley's intersection theorem in the form needed for valuation extensions: an element is integral over the image of the base valuation ring exactly when it lies in every valuation subring of the extension field containing that image. This is the construction-level bridge from the actual integral closure frontier to valuation-overring arguments.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem mem_integralClosure_baseRange_iff_forall_valuationSubring
    (vK : _root_.Valuation K ΓK) (z : L) :
    z ∈ (integralClosure
        (Subring.closure (Set.range (algebraMap vK.valuationSubring L))) L).toSubring ↔
      ∀ V : ValuationSubring L,
        (∀ x : vK.valuationSubring,
          algebraMap vK.valuationSubring L x ∈ V.toSubring) →
        z ∈ V.toSubring
theorem

integralClosure_toSubring_eq_integralClosure_botSubalgebra_toSubring

L480 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosure_toSubring_eq_integralClosure_botSubalgebra_toSubring
Documentation

The actual integral closure over the base valuation ring has the same underlying subring as the integral closure over the bottom vK-subalgebra of L, i.e. over the image of the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosure_toSubring_eq_integralClosure_botSubalgebra_toSubring
    (vK : _root_.Valuation K ΓK) :
    (integralClosure vK.valuationSubring L).toSubring =
      (integralClosure (⊥ : Subalgebra vK.valuationSubring L) L).toSubring
theorem

integralClosure_toSubring_eq_integralClosure_baseRange

L503 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosure_toSubring_eq_integralClosure_baseRange
Documentation

The actual integral closure over the base valuation ring agrees, as an underlying subring of the extension field, with the integral closure over the subring generated by the image of the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosure_toSubring_eq_integralClosure_baseRange
    (vK : _root_.Valuation K ΓK) :
    (integralClosure vK.valuationSubring L).toSubring =
      (integralClosure
        (Subring.closure (Set.range (algebraMap vK.valuationSubring L))) L).toSubring
theorem

mem_integralClosure_iff_forall_valuationSubring

L536 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_integralClosure_iff_forall_valuationSubring
Documentation

Chevalley's intersection theorem for the actual integral closure over the base valuation ring: an element is integral over the base valuation ring iff it lies in every valuation subring of the extension field containing the base valuation ring's image.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem mem_integralClosure_iff_forall_valuationSubring
    (vK : _root_.Valuation K ΓK) (z : L) :
    z ∈ (integralClosure vK.valuationSubring L).toSubring ↔
      ∀ V : ValuationSubring L,
        (∀ x : vK.valuationSubring,
          algebraMap vK.valuationSubring L x ∈ V.toSubring) →
        z ∈ V.toSubring
def

integralClosureToValuationSubringOfHasExtension

L549 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureToValuationSubringOfHasExtension
Documentation

The canonical map from the actual integral closure of the base valuation ring to any valuation ring extending the base valuation.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · full declaration
def integralClosureToValuationSubringOfHasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    integralClosure vK.valuationSubring L →+* vL.valuationSubring where
  toFun z :=
    ⟨(z : L),
      integralClosure_mem_valuationSubring_of_hasExtension
        (L := L) vK vL z⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_add' z₁ z₂ := by ext; simp
  map_mul' z₁ z₂ := by ext; simp
theorem

integralClosureToValuationSubringOfHasExtension_apply

L564 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureToValuationSubringOfHasExtension_apply
Documentation

The canonical map from the integral closure to an extending valuation ring is inclusion.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureToValuationSubringOfHasExtension_apply
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (z : integralClosure vK.valuationSubring L) :
    ((integralClosureToValuationSubringOfHasExtension
      (L := L) vK vL z : vL.valuationSubring) : L) = z
theorem

integralClosureToValuationSubringOfHasExtension_injective

L574 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureToValuationSubringOfHasExtension_injective
Documentation

The integral-closure map into an extension valuation ring is injective.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureToValuationSubringOfHasExtension_injective
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    Function.Injective
      (integralClosureToValuationSubringOfHasExtension
        (L := L) vK vL)
theorem

valuationSubring_mem_integralClosure_of_moduleFinite

L587 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_mem_integralClosure_of_moduleFinite
Documentation

If an extension valuation ring is finite over the base valuation ring, then each of its elements is integral over the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_mem_integralClosure_of_moduleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring]
    (z : vL.valuationSubring) :
    (z : L) ∈ integralClosure vK.valuationSubring L
theorem

valuationSubring_mem_integralClosure_of_isIntegral

L607 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_mem_integralClosure_of_isIntegral
Documentation

If an extension valuation ring is integral over the base valuation ring, then every target valuation-ring element lies in the actual integral closure. This is the construction-level condition needed in the Henselian finite-extension frontier.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_mem_integralClosure_of_isIntegral
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Algebra.IsIntegral vK.valuationSubring vL.valuationSubring]
    (z : vL.valuationSubring) :
    (z : L) ∈ integralClosure vK.valuationSubring L
def

valuationSubringToIntegralClosureOfModuleFinite

L625 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubringToIntegralClosureOfModuleFinite
Documentation

The reverse map from a module-finite extension valuation ring into the actual integral closure.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · full declaration
def valuationSubringToIntegralClosureOfModuleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring] :
    vL.valuationSubring →+* integralClosure vK.valuationSubring L where
  toFun z :=
    ⟨(z : L),
      valuationSubring_mem_integralClosure_of_moduleFinite
        (L := L) vK vL z⟩
  map_zero' := by ext; simp
  map_one' := by ext; simp
  map_add' z₁ z₂ := by ext; simp
  map_mul' z₁ z₂ := by ext; simp
theorem

valuationSubringToIntegralClosureOfModuleFinite_apply

L641 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubringToIntegralClosureOfModuleFinite_apply
Documentation

Under module finiteness, a valuation-ring element maps to its integral-closure class.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubringToIntegralClosureOfModuleFinite_apply
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring]
    (z : vL.valuationSubring) :
    ((valuationSubringToIntegralClosureOfModuleFinite
      (L := L) vK vL z : integralClosure vK.valuationSubring L) : L) = z
theorem

integralClosureToValuationSubringOfHasExtension_surjective_of_moduleFinite

L653 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureToValuationSubringOfHasExtension_surjective_of_moduleFinite
Documentation

Under module-finiteness, the integral closure maps onto the extension valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureToValuationSubringOfHasExtension_surjective_of_moduleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring] :
    Function.Surjective
      (integralClosureToValuationSubringOfHasExtension
        (L := L) vK vL)
theorem

integralClosureToValuationSubringOfHasExtension_bijective_of_moduleFinite

L669 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureToValuationSubringOfHasExtension_bijective_of_moduleFinite
Documentation

Under module-finiteness, the integral-closure map into the extension valuation ring is bijective.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integralClosureToValuationSubringOfHasExtension_bijective_of_moduleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring] :
    Function.Bijective
      (integralClosureToValuationSubringOfHasExtension
        (L := L) vK vL)
def

integralClosureRingEquivValuationSubringOfModuleFinite

L684 ↗
ValuationTheory.DiscreteValuationField.Valuation.integralClosureRingEquivValuationSubringOfModuleFinite
Documentation

A module-finite extension valuation ring is canonically equivalent to the actual integral closure of the base valuation ring in the field extension.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
def integralClosureRingEquivValuationSubringOfModuleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring] :
    integralClosure vK.valuationSubring L ≃+* vL.valuationSubring
theorem

valuationSubring_isIntegralClosure_of_moduleFinite

L698 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_isIntegralClosure_of_moduleFinite
Documentation

A module-finite extension valuation ring is the actual integral closure of the base valuation ring in the field extension.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_isIntegralClosure_of_moduleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Module.Finite vK.valuationSubring vL.valuationSubring] :
    IsIntegralClosure vL.valuationSubring vK.valuationSubring L
theorem

valuationSubring_isIntegralClosure_of_isIntegral

L721 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_isIntegralClosure_of_isIntegral
Documentation

An extension valuation ring that is integral over the base valuation ring is the actual integral closure of the base valuation ring in the field extension. No finite-module certificate is introduced here; the proof is the defining integral-closure 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_isIntegralClosure_of_isIntegral
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [Algebra.IsIntegral vK.valuationSubring vL.valuationSubring] :
    IsIntegralClosure vL.valuationSubring vK.valuationSubring L
theorem

valuationSubring_eq_of_hasExtension_of_isIntegral

L747 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_eq_of_hasExtension_of_isIntegral
Documentation

Two valuation extensions of the same base valuation have the same valuation subring once both extension valuation rings are integral over the base valuation ring.

This is the target-free uniqueness bridge used by the Henselian finite-level route: after the Henselian argument proves integrality for all extension valuation rings, no chosen target DVF package is needed to compare them.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_eq_of_hasExtension_of_isIntegral
    {Γ₁ : Type x} {Γ₂ : Type y}
    [LinearOrderedCommGroupWithZero Γ₁]
    [LinearOrderedCommGroupWithZero Γ₂]
    (vK : _root_.Valuation K ΓK)
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [vK.HasExtension v₁] [vK.HasExtension v₂]
    [Algebra.IsIntegral vK.valuationSubring v₁.valuationSubring]
    [Algebra.IsIntegral vK.valuationSubring v₂.valuationSubring] :
    v₁.valuationSubring = v₂.valuationSubring
theorem

valuation_isEquiv_of_hasExtension_of_isIntegral

L774 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuation_isEquiv_of_hasExtension_of_isIntegral
Documentation

Valuation-equivalence form of valuationSubring_eq_of_hasExtension_of_isIntegral.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuation_isEquiv_of_hasExtension_of_isIntegral
    {Γ₁ : Type x} {Γ₂ : Type y}
    [LinearOrderedCommGroupWithZero Γ₁]
    [LinearOrderedCommGroupWithZero Γ₂]
    (vK : _root_.Valuation K ΓK)
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [vK.HasExtension v₁] [vK.HasExtension v₂]
    [Algebra.IsIntegral vK.valuationSubring v₁.valuationSubring]
    [Algebra.IsIntegral vK.valuationSubring v₂.valuationSubring] :
    v₁.IsEquiv v₂
theorem

mem_valuationSubring_iff_of_hasExtension_of_isIntegral

L789 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_valuationSubring_iff_of_hasExtension_of_isIntegral
Documentation

Elementwise form of target-free integral valuation-extension uniqueness.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem mem_valuationSubring_iff_of_hasExtension_of_isIntegral
    {Γ₁ : Type x} {Γ₂ : Type y}
    [LinearOrderedCommGroupWithZero Γ₁]
    [LinearOrderedCommGroupWithZero Γ₂]
    (vK : _root_.Valuation K ΓK)
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [vK.HasExtension v₁] [vK.HasExtension v₂]
    [Algebra.IsIntegral vK.valuationSubring v₁.valuationSubring]
    [Algebra.IsIntegral vK.valuationSubring v₂.valuationSubring]
    (z : L) :
    z ∈ v₁.valuationSubring ↔ z ∈ v₂.valuationSubring
theorem

valuationSubring_eq_integralClosureValuationSubringOfMemOrInv_of_isIntegral

L810 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_eq_integralClosureValuationSubringOfMemOrInv_of_isIntegral
Documentation

An integral extension valuation ring is exactly the valuation subring constructed from the actual integral closure, once that integral closure has the valuation-ring dichotomy.

This is the comparison form used in finite-extension arguments: after proving integrality of a chosen extension valuation ring, no separate equality with the Chevalley/integral-closure construction has to be assumed.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_eq_integralClosureValuationSubringOfMemOrInv_of_isIntegral
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring)
    [vK.HasExtension vL]
    [Algebra.IsIntegral vK.valuationSubring vL.valuationSubring] :
    vL.valuationSubring =
      integralClosureValuationSubringOfMemOrInv (L := L) vK hval
theorem

moduleFinite_valuationSubring_of_isIntegralClosure

L839 ↗
ValuationTheory.DiscreteValuationField.Valuation.moduleFinite_valuationSubring_of_isIntegralClosure
Documentation

If an extension valuation ring is already the actual integral closure in a finite separable field extension over a Noetherian base valuation ring, then it is finite over the base valuation ring. This is the generic finite-extension input needed before specializing uniqueness of valuation extensions to Henselian DVFs.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem moduleFinite_valuationSubring_of_isIntegralClosure
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [IsNoetherianRing vK.valuationSubring]
    [IsIntegralClosure vL.valuationSubring vK.valuationSubring L] :
    Module.Finite vK.valuationSubring vL.valuationSubring
theorem

moduleFinite_integralClosureValuationSubringOfMemOrInv

L857 ↗
ValuationTheory.DiscreteValuationField.Valuation.moduleFinite_integralClosureValuationSubringOfMemOrInv
Documentation

Once the actual integral closure has been proved to be a valuation subring, finite separability and Noetherianity of the base valuation ring make the constructed integral-closure valuation ring finite over the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · full declaration
theorem moduleFinite_integralClosureValuationSubringOfMemOrInv
    (vK : _root_.Valuation K ΓK)
    (hval :
      ∀ z : L,
        z ∈ (integralClosure vK.valuationSubring L).toSubring ∨
          z⁻¹ ∈ (integralClosure vK.valuationSubring L).toSubring)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [IsNoetherianRing vK.valuationSubring] :
    let B := integralClosureValuationSubringOfMemOrInv (L := L) vK hval
    letI : vK.HasExtension B.valuation :=
      integralClosureValuationSubringOfMemOrInv_hasExtension (L := L) vK hval
    Module.Finite vK.valuationSubring B.valuation.valuationSubring := by
  let B := integralClosureValuationSubringOfMemOrInv (L := L) vK hval
  let : vK.HasExtension B.valuation :=
    integralClosureValuationSubringOfMemOrInv_hasExtension (L := L) vK hval
  let : IsIntegralClosure B.valuation.valuationSubring vK.valuationSubring L := by
    rw [ValuationSubring.valuationSubring_valuation B]
    exact integralClosureValuationSubringOfMemOrInv_isIntegralClosure
      (L := L) vK hval
  exact moduleFinite_valuationSubring_of_isIntegralClosure
    (L := L) vK B.valuation
theorem

valuationSubring_isIntegralClosure_iff_moduleFinite

L882 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_isIntegralClosure_iff_moduleFinite
Documentation

For finite separable field extensions with a chosen valuation extension over a Noetherian base valuation ring, being the integral closure is equivalent to being finite as a module over the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_isIntegralClosure_iff_moduleFinite
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [IsNoetherianRing vK.valuationSubring] :
    IsIntegralClosure vL.valuationSubring vK.valuationSubring L ↔
      Module.Finite vK.valuationSubring vL.valuationSubring
theorem

valuationSubring_isIntegralClosure_iff_isIntegral

L906 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_isIntegralClosure_iff_isIntegral
Documentation

For any chosen valuation extension, being the actual integral closure is equivalent to the target valuation ring being integral over the base valuation ring. The hard Henselian finite-extension step is therefore exactly to prove this integrality for all extension valuations.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_isIntegralClosure_iff_isIntegral
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    IsIntegralClosure vL.valuationSubring vK.valuationSubring L ↔
      Algebra.IsIntegral vK.valuationSubring vL.valuationSubring
theorem

valuationSubring_eq_of_hasExtension_of_moduleFinite

L926 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_eq_of_hasExtension_of_moduleFinite
Documentation

Two module-finite valuation extensions of the same base valuation have the same valuation subring. This is the finite-module uniqueness criterion that the Henselian finite-extension theorem must eventually supply automatically.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_eq_of_hasExtension_of_moduleFinite
    {Γ₁ : Type x} {Γ₂ : Type y}
    [LinearOrderedCommGroupWithZero Γ₁]
    [LinearOrderedCommGroupWithZero Γ₂]
    (vK : _root_.Valuation K ΓK)
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [vK.HasExtension v₁] [vK.HasExtension v₂]
    [Module.Finite vK.valuationSubring v₁.valuationSubring]
    [Module.Finite vK.valuationSubring v₂.valuationSubring] :
    v₁.valuationSubring = v₂.valuationSubring
theorem

valuation_isEquiv_of_hasExtension_of_moduleFinite

L952 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuation_isEquiv_of_hasExtension_of_moduleFinite
Documentation

Valuation-equivalence form of the module-finite uniqueness criterion.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuation_isEquiv_of_hasExtension_of_moduleFinite
    {Γ₁ : Type x} {Γ₂ : Type y}
    [LinearOrderedCommGroupWithZero Γ₁]
    [LinearOrderedCommGroupWithZero Γ₂]
    (vK : _root_.Valuation K ΓK)
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [vK.HasExtension v₁] [vK.HasExtension v₂]
    [Module.Finite vK.valuationSubring v₁.valuationSubring]
    [Module.Finite vK.valuationSubring v₂.valuationSubring] :
    v₁.IsEquiv v₂
theorem

mem_valuationSubring_iff_of_hasExtension_of_moduleFinite

L967 ↗
ValuationTheory.DiscreteValuationField.Valuation.mem_valuationSubring_iff_of_hasExtension_of_moduleFinite
Documentation

Elementwise form of module-finite valuation-extension uniqueness.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem mem_valuationSubring_iff_of_hasExtension_of_moduleFinite
    {Γ₁ : Type x} {Γ₂ : Type y}
    [LinearOrderedCommGroupWithZero Γ₁]
    [LinearOrderedCommGroupWithZero Γ₂]
    (vK : _root_.Valuation K ΓK)
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [vK.HasExtension v₁] [vK.HasExtension v₂]
    [Module.Finite vK.valuationSubring v₁.valuationSubring]
    [Module.Finite vK.valuationSubring v₂.valuationSubring]
    (z : L) :
    z ∈ v₁.valuationSubring ↔ z ∈ v₂.valuationSubring
theorem

exists_extension_valuationSubring_with_hasExtension

L983 ↗
ValuationTheory.DiscreteValuationField.Valuation.exists_extension_valuationSubring_with_hasExtension
Documentation

Chevalley's theorem in construction form, keeping the dominating valuation subring and the HasExtension proof attached to its canonical valuation.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem exists_extension_valuationSubring_with_hasExtension
    (vK : _root_.Valuation K ΓK) :
    ∃ B : ValuationSubring L,
      ∃ hB : ∀ x : vK.valuationSubring,
        algebraMap vK.valuationSubring L x ∈ B.toSubring,
        IsLocalHom
          ((algebraMap vK.valuationSubring L).codRestrict B.toSubring hB) ∧
        (∀ x : K, algebraMap K L x ∈ B.toSubring ↔
          x ∈ vK.valuationSubring) ∧
        vK.HasExtension B.valuation
theorem

chevalley_exists_extension_valuation_with_pullback

L1002 ↗
ValuationTheory.DiscreteValuationField.Valuation.chevalley_exists_extension_valuation_with_pullback
Documentation

Chevalley's theorem as an actual valuation extension with exact pullback of the extension valuation ring. This is the valuation-level form of exists_extension_valuationSubring_with_hasExtension, not just the existential predicate HasSomeExtensionTo.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem chevalley_exists_extension_valuation_with_pullback
    (vK : _root_.Valuation K ΓK) :
    ∃ ΓL : Type v,
      ∃ _ : LinearOrderedCommGroupWithZero ΓL,
        ∃ vL : _root_.Valuation L ΓL,
          ∃ _ : vK.HasExtension vL,
            ∀ x : K, algebraMap K L x ∈ vL.valuationSubring ↔
              x ∈ vK.valuationSubring
theorem

exists_extension_valuationSubring_with_integralClosure

L1019 ↗
ValuationTheory.DiscreteValuationField.Valuation.exists_extension_valuationSubring_with_integralClosure
Documentation

Chevalley's construction can be chosen with the integral-closure dominance made explicit: the produced extension valuation ring contains the actual integral closure of the base valuation ring in the extension field.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem exists_extension_valuationSubring_with_integralClosure
    (vK : _root_.Valuation K ΓK) :
    ∃ B : ValuationSubring L,
      ∃ hB : ∀ x : vK.valuationSubring,
        algebraMap vK.valuationSubring L x ∈ B.toSubring,
        IsLocalHom
          ((algebraMap vK.valuationSubring L).codRestrict B.toSubring hB) ∧
        (∀ x : K, algebraMap K L x ∈ B.toSubring ↔
          x ∈ vK.valuationSubring) ∧
        vK.HasExtension B.valuation ∧
        (∀ z : integralClosure vK.valuationSubring L,
          (z : L) ∈ B.toSubring)
theorem

chevalley_exists_extension_valuation_with_pullback_integralClosure

L1044 ↗
ValuationTheory.DiscreteValuationField.Valuation.chevalley_exists_extension_valuation_with_pullback_integralClosure
Documentation

Chevalley's valuation extension can be chosen with both exact pullback of the valuation ring and containment of the actual integral closure of the base valuation ring.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem chevalley_exists_extension_valuation_with_pullback_integralClosure
    (vK : _root_.Valuation K ΓK) :
    ∃ ΓL : Type v,
      ∃ _ : LinearOrderedCommGroupWithZero ΓL,
        ∃ vL : _root_.Valuation L ΓL,
          ∃ _ : vK.HasExtension vL,
            (∀ x : K, algebraMap K L x ∈ vL.valuationSubring ↔
              x ∈ vK.valuationSubring) ∧
            (∀ z : integralClosure vK.valuationSubring L,
              (z : L) ∈ vL.valuationSubring)
theorem

chevalley_exists_extension_valuation_with_pullback_integralClosure_local_data

L1067 ↗
ValuationTheory.DiscreteValuationField.Valuation.chevalley_exists_extension_valuation_with_pullback_integralClosure_local_data
Documentation

Chevalley's valuation extension with all construction-level data attached to the same witness: exact valuation-ring pullback, integral-closure containment, lies-over for maximal ideals, local valuation-ring map, and injective residue-field 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem chevalley_exists_extension_valuation_with_pullback_integralClosure_local_data
    (vK : _root_.Valuation K ΓK) :
    ∃ ΓL : Type v,
      ∃ _ : LinearOrderedCommGroupWithZero ΓL,
        ∃ vL : _root_.Valuation L ΓL,
          ∃ _ : vK.HasExtension vL,
            (∀ x : K, algebraMap K L x ∈ vL.valuationSubring ↔
              x ∈ vK.valuationSubring) ∧
            (∀ z : integralClosure vK.valuationSubring L,
              (z : L) ∈ vL.valuationSubring) ∧
            (IsLocalRing.maximalIdeal vL.valuationSubring).LiesOver
              (IsLocalRing.maximalIdeal vK.valuationSubring) ∧
            IsLocalHom
              (algebraMap vK.valuationSubring vL.valuationSubring) ∧
            Function.Injective
              (IsLocalRing.ResidueField.map
                (algebraMap vK.valuationSubring vL.valuationSubring))
theorem

chevalley_hasSomeExtensionTo

L1098 ↗
ValuationTheory.DiscreteValuationField.Valuation.chevalley_hasSomeExtensionTo
Documentation

Chevalley's valuation extension theorem: every valuation on a field extends to any field extension. The extended value group is the canonical value group of a valuation subring of the extension field supplied by mathlib's maximal local subring theorem.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem chevalley_hasSomeExtensionTo
    (vK : _root_.Valuation K ΓK) :
    HasSomeExtensionTo (L := L) vK
theorem

hasSomeExtensionTo_of_hasExtension

L1106 ↗
ValuationTheory.DiscreteValuationField.Valuation.hasSomeExtensionTo_of_hasExtension
Documentation

A specified valuation extension supplies existence of some extension to the target field.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem hasSomeExtensionTo_of_hasExtension
    {ΓL : Type v} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    HasSomeExtensionTo (L := L) vK
theorem

valuationSubring_liesOver_of_hasExtension

L1114 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_liesOver_of_hasExtension
Documentation

The target valuation subring lies over the source 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_liesOver_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    (IsLocalRing.maximalIdeal vL.valuationSubring).LiesOver
      (IsLocalRing.maximalIdeal vK.valuationSubring)
theorem

integerMap_isLocalHom_of_hasExtension

L1123 ↗
ValuationTheory.DiscreteValuationField.Valuation.integerMap_isLocalHom_of_hasExtension
Documentation

The integer map induced by a valuation extension is a local ring homomorphism.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem integerMap_isLocalHom_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    IsLocalHom (algebraMap vK.valuationSubring vL.valuationSubring)
theorem

valuationSubring_isScalarTower_of_hasExtension

L1132 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_isScalarTower_of_hasExtension
Documentation

The valuation-subring algebra maps are compatible with the ambient field algebra map for any chosen valuation extension.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem valuationSubring_isScalarTower_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    IsScalarTower vK.valuationSubring vL.valuationSubring L
theorem

residueMap_injective_of_hasExtension

L1148 ↗
ValuationTheory.DiscreteValuationField.Valuation.residueMap_injective_of_hasExtension
Documentation

The residue-field map attached to any valuation extension is injective.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residueMap_injective_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL] :
    Function.Injective
      (IsLocalRing.ResidueField.map
        (algebraMap vK.valuationSubring vL.valuationSubring))
theorem

residueMap_eq_zero_iff_of_hasExtension

L1160 ↗
ValuationTheory.DiscreteValuationField.Valuation.residueMap_eq_zero_iff_of_hasExtension
Documentation

The residue-field map attached to a valuation extension has trivial kernel.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residueMap_eq_zero_iff_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (z : IsLocalRing.ResidueField vK.valuationSubring) :
    IsLocalRing.ResidueField.map
        (algebraMap vK.valuationSubring vL.valuationSubring) z = 0 ↔
      z = 0
theorem

residueMap_eq_iff_of_hasExtension

L1173 ↗
ValuationTheory.DiscreteValuationField.Valuation.residueMap_eq_iff_of_hasExtension
Documentation

Equality of base residue classes can be checked after applying the residue-field map attached to a valuation extension.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residueMap_eq_iff_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (z₁ z₂ : IsLocalRing.ResidueField vK.valuationSubring) :
    IsLocalRing.ResidueField.map
        (algebraMap vK.valuationSubring vL.valuationSubring) z₁ =
        IsLocalRing.ResidueField.map
          (algebraMap vK.valuationSubring vL.valuationSubring) z₂ ↔
      z₁ = z₂
theorem

residueMap_residue_eq_residue_iff_sub_mem_maximalIdeal_of_hasExtension

L1189 ↗
ValuationTheory.DiscreteValuationField.Valuation.residueMap_residue_eq_residue_iff_sub_mem_maximalIdeal_of_hasExtension
Documentation

Equality between the mapped residue of a base valuation-ring element and a target valuation-ring residue representative is congruence modulo the target maximal ideal.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residueMap_residue_eq_residue_iff_sub_mem_maximalIdeal_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (a : vK.valuationSubring) (b : vL.valuationSubring) :
    IsLocalRing.ResidueField.map
        (algebraMap vK.valuationSubring vL.valuationSubring)
        (IsLocalRing.residue vK.valuationSubring a) =
        IsLocalRing.residue vL.valuationSubring b ↔
      algebraMap vK.valuationSubring vL.valuationSubring a - b ∈
        IsLocalRing.maximalIdeal vL.valuationSubring
theorem

residue_eq_residueMap_residue_iff_sub_mem_maximalIdeal_of_hasExtension

L1205 ↗
ValuationTheory.DiscreteValuationField.Valuation.residue_eq_residueMap_residue_iff_sub_mem_maximalIdeal_of_hasExtension
Documentation

Opposite-orientation congruence criterion for the residue-field map attached to a valuation extension.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residue_eq_residueMap_residue_iff_sub_mem_maximalIdeal_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (b : vL.valuationSubring) (a : vK.valuationSubring) :
    IsLocalRing.residue vL.valuationSubring b =
        IsLocalRing.ResidueField.map
          (algebraMap vK.valuationSubring vL.valuationSubring)
          (IsLocalRing.residue vK.valuationSubring a) ↔
      b - algebraMap vK.valuationSubring vL.valuationSubring a ∈
        IsLocalRing.maximalIdeal vL.valuationSubring
theorem

residue_algebraMap_eq_zero_iff_of_hasExtension

L1221 ↗
ValuationTheory.DiscreteValuationField.Valuation.residue_algebraMap_eq_zero_iff_of_hasExtension
Documentation

The target residue of a mapped base valuation-ring element is zero exactly when the base element lies in the base maximal ideal.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residue_algebraMap_eq_zero_iff_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (a : vK.valuationSubring) :
    IsLocalRing.residue vL.valuationSubring
        (algebraMap vK.valuationSubring vL.valuationSubring a) = 0 ↔
      a ∈ IsLocalRing.maximalIdeal vK.valuationSubring
theorem

residue_algebraMap_eq_iff_of_hasExtension

L1235 ↗
ValuationTheory.DiscreteValuationField.Valuation.residue_algebraMap_eq_iff_of_hasExtension
Documentation

Equality of target residues of two mapped base valuation-ring elements is equality of the corresponding base residues.

Source context 8 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem residue_algebraMap_eq_iff_of_hasExtension
    {ΓL : Type x} [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    [vK.HasExtension vL]
    (a b : vK.valuationSubring) :
    IsLocalRing.residue vL.valuationSubring
        (algebraMap vK.valuationSubring vL.valuationSubring a) =
        IsLocalRing.residue vL.valuationSubring
          (algebraMap vK.valuationSubring vL.valuationSubring b) ↔
      IsLocalRing.residue vK.valuationSubring a =
        IsLocalRing.residue vK.valuationSubring b
theorem

hasExtension_trans

L1258 ↗
ValuationTheory.DiscreteValuationField.Valuation.hasExtension_trans
Documentation

Valuation extension is transitive in a field tower.

Source context 14 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
section Tower
variable {M : Type y} [Field M]
variable [Algebra L M] [Algebra K M] [IsScalarTower K L M]
variable {ΓL : Type x} {ΓM : Type z}
variable [LinearOrderedCommGroupWithZero ΓL]
variable [LinearOrderedCommGroupWithZero ΓM]
Lean source · statement
theorem hasExtension_trans
    (vK : _root_.Valuation K ΓK)
    (vL : _root_.Valuation L ΓL)
    (vM : _root_.Valuation M ΓM)
    [vK.HasExtension vL] [vL.HasExtension vM] :
    vK.HasExtension vM
theorem

valuationSubring_liesOver_tower_of_hasExtension

L1277 ↗
ValuationTheory.DiscreteValuationField.Valuation.valuationSubring_liesOver_tower_of_hasExtension
Documentation

In a tower of valuation extensions, the top valuation ring lies over the bottom valuation ring.

Source context 14 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
section Tower
variable {M : Type y} [Field M]
variable [Algebra L M] [Algebra K M] [IsScalarTower K L M]
variable {ΓL : Type x} {ΓM : Type z}
variable [LinearOrderedCommGroupWithZero ΓL]
variable [LinearOrderedCommGroupWithZero ΓM]
Lean source · full declaration
theorem valuationSubring_liesOver_tower_of_hasExtension
    (vK : _root_.Valuation K ΓK)
    (vL : _root_.Valuation L ΓL)
    (vM : _root_.Valuation M ΓM)
    [vK.HasExtension vL] [vL.HasExtension vM] :
    letI : vK.HasExtension vM := hasExtension_trans vK vL vM
    (IsLocalRing.maximalIdeal vM.valuationSubring).LiesOver
      (IsLocalRing.maximalIdeal vK.valuationSubring) := by
  let : vK.HasExtension vM := hasExtension_trans vK vL vM
  exact valuationSubring_liesOver_of_hasExtension vK vM
theorem

integerMap_comp_of_hasExtension_tower

L1291 ↗
ValuationTheory.DiscreteValuationField.Valuation.integerMap_comp_of_hasExtension_tower
Documentation

The valuation-ring algebra maps in a tower agree with the direct valuation-ring algebra map. The direct HasExtension instance can be supplied by hasExtension_trans.

Source context 14 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
section Tower
variable {M : Type y} [Field M]
variable [Algebra L M] [Algebra K M] [IsScalarTower K L M]
variable {ΓL : Type x} {ΓM : Type z}
variable [LinearOrderedCommGroupWithZero ΓL]
variable [LinearOrderedCommGroupWithZero ΓM]
Lean source · statement
theorem integerMap_comp_of_hasExtension_tower
    (vK : _root_.Valuation K ΓK)
    (vL : _root_.Valuation L ΓL)
    (vM : _root_.Valuation M ΓM)
    [vK.HasExtension vL] [vL.HasExtension vM] [vK.HasExtension vM] :
    (algebraMap vL.valuationSubring vM.valuationSubring).comp
        (algebraMap vK.valuationSubring vL.valuationSubring) =
      algebraMap vK.valuationSubring vM.valuationSubring
theorem

residueMap_comp_of_hasExtension_tower

L1306 ↗
ValuationTheory.DiscreteValuationField.Valuation.residueMap_comp_of_hasExtension_tower
Documentation

Residue-field maps in a tower compose to the direct residue-field map. The direct HasExtension instance can be supplied by hasExtension_trans.

Source context 14 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
section Tower
variable {M : Type y} [Field M]
variable [Algebra L M] [Algebra K M] [IsScalarTower K L M]
variable {ΓL : Type x} {ΓM : Type z}
variable [LinearOrderedCommGroupWithZero ΓL]
variable [LinearOrderedCommGroupWithZero ΓM]
Lean source · statement
theorem residueMap_comp_of_hasExtension_tower
    (vK : _root_.Valuation K ΓK)
    (vL : _root_.Valuation L ΓL)
    (vM : _root_.Valuation M ΓM)
    [vK.HasExtension vL] [vL.HasExtension vM] [vK.HasExtension vM] :
    (IsLocalRing.ResidueField.map
        (algebraMap vL.valuationSubring vM.valuationSubring)).comp
        (IsLocalRing.ResidueField.map
          (algebraMap vK.valuationSubring vL.valuationSubring)) =
      IsLocalRing.ResidueField.map
        (algebraMap vK.valuationSubring vM.valuationSubring)
theorem

residueMap_tower_apply_of_hasExtension

L1330 ↗
ValuationTheory.DiscreteValuationField.Valuation.residueMap_tower_apply_of_hasExtension
Documentation

Elementwise form of residueMap_comp_of_hasExtension_tower.

Source context 14 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 Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
section Tower
variable {M : Type y} [Field M]
variable [Algebra L M] [Algebra K M] [IsScalarTower K L M]
variable {ΓL : Type x} {ΓM : Type z}
variable [LinearOrderedCommGroupWithZero ΓL]
variable [LinearOrderedCommGroupWithZero ΓM]
Lean source · statement
theorem residueMap_tower_apply_of_hasExtension
    (vK : _root_.Valuation K ΓK)
    (vL : _root_.Valuation L ΓL)
    (vM : _root_.Valuation M ΓM)
    [vK.HasExtension vL] [vL.HasExtension vM] [vK.HasExtension vM]
    (x : IsLocalRing.ResidueField vK.valuationSubring) :
    IsLocalRing.ResidueField.map
        (algebraMap vL.valuationSubring vM.valuationSubring)
        (IsLocalRing.ResidueField.map
          (algebraMap vK.valuationSubring vL.valuationSubring) x) =
      IsLocalRing.ResidueField.map
        (algebraMap vK.valuationSubring vM.valuationSubring) x
theorem

chevalley_exists_extension_with_local_data

L1351 ↗
ValuationTheory.DiscreteValuationField.Valuation.chevalley_exists_extension_with_local_data
Documentation

Chevalley's extension theorem with the local valuation-ring data needed by finite-extension and residue-field arguments: the chosen extension has a valuation-ring map whose target maximal ideal lies over the base maximal ideal, is local, and induces an injective residue-field 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 z
namespace DiscreteValuationField
namespace Valuation
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable {ΓK : Type w} [LinearOrderedCommGroupWithZero ΓK]
Lean source · statement
theorem chevalley_exists_extension_with_local_data
    (vK : _root_.Valuation K ΓK) :
    ∃ ΓL : Type v,
      ∃ _ : LinearOrderedCommGroupWithZero ΓL,
        ∃ vL : _root_.Valuation L ΓL,
          ∃ _ : vK.HasExtension vL,
            (IsLocalRing.maximalIdeal vL.valuationSubring).LiesOver
              (IsLocalRing.maximalIdeal vK.valuationSubring) ∧
            IsLocalHom
              (algebraMap vK.valuationSubring vL.valuationSubring) ∧
            Function.Injective
              (IsLocalRing.ResidueField.map
                (algebraMap vK.valuationSubring vL.valuationSubring))

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