Module

UniqueValuationSubring.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.UniqueValuationSubring

1 declaration indexed from sourceView source ↗

Module documentation

uniqueness from the integral-closure valuation ring

Once the actual integral closure of a valuation subring satisfies the valuative dichotomy, it is contained in every extension valuation ring. Its integrality over the base then forces the center of every such overring to be the unique maximal ideal, so the overring is the integral closure itself.

Imports1

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ChevalleyExtension

Imported by10

theorem

normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv

L37 ↗

DiscreteValuationField.Valuation.normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv

Documentation

the finite norm-formula theorem, uniqueness source after the actual integral closure has been shown to be a valuation ring.

No finiteness, separability, discreteness, or completeness assumption is used: every valuation of L extending the canonical valuation of V has valuation subring equal to the valuation subring built from the actual integral closure of V in L.

Source context 6 commands

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

noncomputable section
universe u v w
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField.Valuation
namespace Valuation
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv
    (V : ValuationSubring K)
    (hval :
      ∀ z : L,
        z ∈
            (integralClosure V.valuation.valuationSubring L).toSubring ∨
          z⁻¹ ∈
            (integralClosure V.valuation.valuationSubring L).toSubring)
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (wL : _root_.Valuation L Γ) [V.valuation.HasExtension wL] :
    wL.valuationSubring =
      integralClosureValuationSubringOfMemOrInv
        (L := L) V.valuation hval

Module documentation

uniqueness from the integral-closure valuation ring

Declarations

normFormula_extension_valuationSubring_eq_integralClosure_of_mem_or_inv