Module

UniqueAlgebraicExtensions.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.UniqueAlgebraicExtensions

8 declarations indexed from sourceView source ↗

Module documentation

unique extension criterion

Valuations are regarded valuations up to equivalence. Accordingly, uniqueness on an algebraic extension is stated as literal uniqueness of its valuation subring. This is the same endpoint used in the finite norm-formula theorem.

Imports3

Imported by10

def

HasUniqueValuationSubringExtension

L27 ↗

AlgebraicNumberTheory.Valuations.HasUniqueValuationSubringExtension

Documentation

A valuation subring has a unique extension valuation ring to L.

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

def HasUniqueValuationSubringExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) : Prop

def

HasUniqueAlgebraicValuationSubringExtensions

L35 ↗

AlgebraicNumberTheory.Valuations.HasUniqueAlgebraicValuationSubringExtensions

Documentation

A valuation subring has a unique extension valuation ring on every algebraic extension in the same universe. This is the valuation-ring form of the right-hand side of the unique-extension criterion.

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

def HasUniqueAlgebraicValuationSubringExtensions
    {K : Type u} [Field K] (V : ValuationSubring K) : Prop

theorem

monicResidualCoprimeFactorLifting_of_unique_algebraic_extensions

L45 ↗

AlgebraicNumberTheory.Valuations.monicResidualCoprimeFactorLifting_of_unique_algebraic_extensions

Documentation

Unique extension on every algebraic field supplies the exact monic coprime-factor lifting property. Factor the monic polynomial into monic irreducibles over the valuation ring; uniqueness on each splitting field forces every irreducible reduction to lie wholly on one side of a coprime residual factorization.

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 monicResidualCoprimeFactorLifting_of_unique_algebraic_extensions
    {K : Type u} [Field K] (V : ValuationSubring K)
    (hunique : HasUniqueAlgebraicValuationSubringExtensions V) :
    DiscreteValuationField.MonicResidualCoprimeFactorLifting V

theorem

henselianUniqueExtension_unique_algebraic_valuationSubring_extension_of_henselian

L72 ↗

AlgebraicNumberTheory.Valuations.henselianUniqueExtension_unique_algebraic_valuationSubring_extension_of_henselian

Documentation

the unique-extension criterion, forward direction. the primitive factorization definition, in its exact factorization form, gives a unique extension valuation ring on every algebraic extension.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
universe u
open _root_.DiscreteValuationField.Valuation in

Lean source · statement

theorem henselianUniqueExtension_unique_algebraic_valuationSubring_extension_of_henselian
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (absoluteValueValuationSubring
        v hnonarch).valuation) :
    HasUniqueValuationSubringExtension
      (L := L) (absoluteValueValuationSubring v hnonarch)

theorem

henselianUniqueExtension_unique_algebraic_valuationSubring_extensions_of_henselian

L124 ↗

AlgebraicNumberTheory.Valuations.henselianUniqueExtension_unique_algebraic_valuationSubring_extensions_of_henselian

Documentation

the unique-extension criterion, forward implication simultaneously for every algebraic extension.

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 henselianUniqueExtension_unique_algebraic_valuationSubring_extensions_of_henselian
    {K : Type u} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (absoluteValueValuationSubring
        v hnonarch).valuation) :
    HasUniqueAlgebraicValuationSubringExtensions
      (absoluteValueValuationSubring v hnonarch)

theorem

henselFactorization_of_unique_algebraic_valuationSubring_extensions

L142 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_of_unique_algebraic_valuationSubring_extensions

Documentation

the unique-extension criterion, converse in the exact factorization form of the primitive factorization definition. The Galois argument gives the primitive-irreducible reduction property, and the primitive-factor partition turns it into the required degree-controlled factorization.

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 henselFactorization_of_unique_algebraic_valuationSubring_extensions
    {K : Type u} [Field K] (V : ValuationSubring K)
    (hunique : HasUniqueAlgebraicValuationSubringExtensions V) :
    ValuationTheory.DiscreteValuationField.HenselFactorizationProperty V

theorem

henselianUniqueExtension_henselian_of_unique_algebraic_valuationSubring_extensions

L154 ↗

AlgebraicNumberTheory.Valuations.henselianUniqueExtension_henselian_of_unique_algebraic_valuationSubring_extensions

Documentation

The converse of the unique-extension criterion for the valuation attached to the construction's 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 henselianUniqueExtension_henselian_of_unique_algebraic_valuationSubring_extensions
    {K : Type u} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hunique : HasUniqueAlgebraicValuationSubringExtensions
      (absoluteValueValuationSubring v hnonarch)) :
    ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (absoluteValueValuationSubring
        v hnonarch).valuation

theorem

henselianUniqueExtension_henselian_iff_unique_algebraic_valuationSubring_extensions

L176 ↗

AlgebraicNumberTheory.Valuations.henselianUniqueExtension_henselian_iff_unique_algebraic_valuationSubring_extensions

Documentation

the unique-extension criterion. A nonarchimedean valuation is Henselian exactly when its valuation ring has a unique extension valuation ring on every algebraic extension. Literal equality of valuation rings is the equivalence relation on valuations.

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 henselianUniqueExtension_henselian_iff_unique_algebraic_valuationSubring_extensions
    {K : Type u} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v) :
    ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
        (absoluteValueValuationSubring
          v hnonarch).valuation ↔
      HasUniqueAlgebraicValuationSubringExtensions
        (absoluteValueValuationSubring v hnonarch)

Module documentation

unique extension criterion

Declarations