NYLL
Module

HenselianAlgebraicExtension.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.HenselianAlgebraicExtension
2 declarations indexed from sourceView source ↗

Module documentation

Henselianity along algebraic valued extensions

The proof of the unramified base-change theorem applies Hensel's lemma after base change from K to an algebraic extension K'. This file supplies the source used there: the unique extension of a Henselian valuation to an algebraic field is again Henselian. The result is derived from the unique extension criterion of the unique-extension criterion, rather than added as an assumption to the unramified base-change theorem.

Imports1
Imported by5

Declarations

theorem

exponentialValuation_hasUniqueAlgebraicValuationSubringExtensions

L32 ↗
AlgebraicNumberTheory.Valuations.exponentialValuation_hasUniqueAlgebraicValuationSubringExtensions
Documentation

The exponential presentation of a Henselian valuation has a unique valuation-subring extension to every algebraic field in the same universe. This is the unique-extension criterion transported through the associated nonarchimedean absolute value.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
universe u
Lean source · statement
theorem exponentialValuation_hasUniqueAlgebraicValuationSubringExtensions
    {K : Type u} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation) :
    HasUniqueAlgebraicValuationSubringExtensions
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v)
theorem

henselianValuation_of_algebraic_extension

L67 ↗
AlgebraicNumberTheory.Valuations.henselianValuation_of_algebraic_extension
Documentation

An algebraic extension of a Henselian valued field is Henselian for its unique extended valuation.

Only the actual exact extension of the two exponential valuations is an input. For a further algebraic extension M/L, uniqueness over K first forces the restriction of its unique valuation ring to be the chosen ring on L; transitivity then gives uniqueness over L, and the unique-extension criterion supplies Hensel factorization on the target valuation ring.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
universe u
Lean source · statement
theorem henselianValuation_of_algebraic_extension
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation) :
    ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring w).valuation

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