NYLL
Module

NormalizedCompleteExtension.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.NormalizedCompleteExtension
2 declarations indexed from sourceView source ↗

Module documentation

Integer-valued complete extensions

The integral closure supplies a complete extension valuation, and its localization supplies an integer-valued discrete extension valuation. Uniqueness identifies their valuation subrings and transports completeness.

Imports3
Imported by2

Declarations

theorem

isCompleteDiscrete_of_valuationSubring_eq

L23 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isCompleteDiscrete_of_valuationSubring_eq
Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w
Lean source · statement
theorem isCompleteDiscrete_of_valuationSubring_eq
    {L Γ₁ Γ₂ : Type*} [Field L]
    [LinearOrderedCommGroupWithZero Γ₁] [LinearOrderedCommGroupWithZero Γ₂]
    (v₁ : _root_.Valuation L Γ₁) (v₂ : _root_.Valuation L Γ₂)
    [Valuation.IsCompleteDiscrete v₁] [v₂.IsRankOneDiscrete]
    (h : v₁.valuationSubring = v₂.valuationSubring) :
    Valuation.IsCompleteDiscrete v₂
theorem

exists_normalized_complete_valuation_of_finite_separable

L38 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.exists_normalized_complete_valuation_of_finite_separable
Documentation

Every finite separable extension of a complete DVF has an actual integer-valued complete discrete valuation extending the base valuation.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w
Lean source · statement
theorem exists_normalized_complete_valuation_of_finite_separable
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (base : CompleteDVF.{u, v} K) :
    ∃ vL : _root_.Valuation L (WithZero (Multiplicative ℤ)),
      Valuation.IsCompleteDiscrete vL ∧ base.valuation.HasExtension vL

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