Module

NormFormulaIntegralClosure.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaIntegralClosure

3 declarations indexed from sourceView source ↗

Module documentation

the actual integral closure is a valuation ring

The factorization form of Hensel's lemma forces the endpoint coefficient estimate for every irreducible polynomial. Applied to the norm-formula value, this says that every algebraic element or its inverse is integral over the base valuation ring. Thus the actual integral closure, rather than an assumed target ring, satisfies the valuation-ring dichotomy.

Imports2

Imported by9

theorem

normFormula_finiteExtensionNormFormulaValue_isIntegral_of_le_one_of_henselFactorization

L30 ↗

AlgebraicNumberTheory.Valuations.normFormula_finiteExtensionNormFormulaValue_isIntegral_of_le_one_of_henselFactorization

Documentation

A closed unit for the finite norm-formula value is integral over the base valuation ring, using only the primitive factorization definition's primitive factorization property.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped Polynomial

Lean source · statement

theorem normFormula_finiteExtensionNormFormulaValue_isIntegral_of_le_one_of_henselFactorization
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch))
    {x : L} (hx : finiteExtensionNormFormulaValue v x ≤ 1) :
    IsIntegral
      (absoluteValueValuationSubring v hnonarch) x

theorem

normFormula_finite_integralClosure_mem_or_inv_of_henselFactorization

L75 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_integralClosure_mem_or_inv_of_henselFactorization

Documentation

In a finite extension, every element or its inverse belongs to the actual integral closure of the base valuation ring.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped Polynomial

Lean source · statement

theorem normFormula_finite_integralClosure_mem_or_inv_of_henselFactorization
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch))
    (x : L) :
    x ∈ (integralClosure
        (absoluteValueValuationSubring v hnonarch) L).toSubring ∨
      x⁻¹ ∈ (integralClosure
        (absoluteValueValuationSubring v hnonarch) L).toSubring

theorem

normFormula_algebraic_integralClosure_mem_or_inv_of_henselFactorization

L107 ↗

AlgebraicNumberTheory.Valuations.normFormula_algebraic_integralClosure_mem_or_inv_of_henselFactorization

Documentation

the finite norm-formula theorem, source-producing algebraic endpoint: for an arbitrary algebraic extension, the actual integral closure of the Henselian valuation ring satisfies the valuation-ring dichotomy. Each element is handled inside the finite simple subextension that it generates.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
open scoped Polynomial

Lean source · statement

theorem normFormula_algebraic_integralClosure_mem_or_inv_of_henselFactorization
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch))
    (x : L) :
    x ∈ (integralClosure
        (absoluteValueValuationSubring v hnonarch) L).toSubring ∨
      x⁻¹ ∈ (integralClosure
        (absoluteValueValuationSubring v hnonarch) L).toSubring

Module documentation

the actual integral closure is a valuation ring

Declarations

normFormula_finiteExtensionNormFormulaValue_isIntegral_of_le_one_of_henselFactorization

normFormula_finite_integralClosure_mem_or_inv_of_henselFactorization

normFormula_algebraic_integralClosure_mem_or_inv_of_henselFactorization