Module

NormFormulaAbsoluteValue.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaAbsoluteValue

8 declarations indexed from sourceView source ↗

Module documentation

the finite norm-formula absolute value

The factorization form of Hensel's lemma makes the closed unit ball of the finite norm-formula value equal to the integral elements over the base valuation ring. This supplies the strong triangle inequality and hence the absolute value without completeness or separatedness assumptions.

Imports1

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaIntegralClosure

Imported by9

theorem

normFormula_finiteExtensionNormFormulaValue_add_le_one_of_le_one_of_henselFactorization

L25 ↗

AlgebraicNumberTheory.Valuations.normFormula_finiteExtensionNormFormulaValue_add_le_one_of_le_one_of_henselFactorization

Documentation

The closed unit ball of the finite norm-formula value is closed under addition, using only the primitive factorization form of Hensel's lemma.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finiteExtensionNormFormulaValue_add_le_one_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 y : L}
    (hx : finiteExtensionNormFormulaValue v x ≤ 1)
    (hy : finiteExtensionNormFormulaValue v y ≤ 1) :
    finiteExtensionNormFormulaValue v (x + y) ≤ 1

theorem

normFormula_finiteExtensionNormFormulaValue_strong_triangle_of_henselFactorization

L45 ↗

AlgebraicNumberTheory.Valuations.normFormula_finiteExtensionNormFormulaValue_strong_triangle_of_henselFactorization

Documentation

The finite norm-formula value satisfies the strong nonarchimedean triangle inequality under the primitive factorization form of Hensel's lemma.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finiteExtensionNormFormulaValue_strong_triangle_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 y : L) :
    finiteExtensionNormFormulaValue v (x + y) ≤
      max (finiteExtensionNormFormulaValue v x)
        (finiteExtensionNormFormulaValue v y)

def

normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization

L123 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization

Documentation

the finite norm-formula theorem finite norm formula bundled as an absolute value, assuming only the primitive factorization form of Hensel's lemma on the base valuation ring.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · full declaration

def normFormula_finite_normFormulaAbsoluteValue_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)) :
    AbsoluteValue L ℝ where
  toFun := finiteExtensionNormFormulaValue v
  map_mul' x y := normFormula_finiteExtensionNormFormulaValue_mul v x y
  nonneg' x := finiteExtensionNormFormulaValue_nonneg v x
  eq_zero' x := normFormula_finiteExtensionNormFormulaValue_eq_zero_iff v x
  add_le' x y := by
    have hstrong :=
      normFormula_finiteExtensionNormFormulaValue_strong_triangle_of_henselFactorization
        v hnonarch hv x y
    have hx_nonneg : 0 ≤ finiteExtensionNormFormulaValue v x :=
      finiteExtensionNormFormulaValue_nonneg v x
    have hy_nonneg : 0 ≤ finiteExtensionNormFormulaValue v y :=
      finiteExtensionNormFormulaValue_nonneg v y
    exact hstrong.trans
      (max_le
        (le_add_of_nonneg_right hy_nonneg)
        (le_add_of_nonneg_left hx_nonneg))

theorem

normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_apply

L149 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_apply

Documentation

The bundled finite norm-formula absolute value is pointwise the construction's displayed value.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_apply
    {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) :
    normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
        (K := K) (L := L) v hnonarch hv x =
      finiteExtensionNormFormulaValue v x

theorem

normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_extends_base

L163 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_extends_base

Documentation

The bundled norm-formula absolute value restricts to the original base absolute value.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_extends_base
    {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 : K) :
    normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
        (K := K) (L := L) v hnonarch hv (algebraMap K L x) = v x

theorem

normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean

L175 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean

Documentation

The bundled finite norm-formula absolute value is nonarchimedean.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean
    {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)) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
        (K := K) (L := L) v hnonarch hv)

theorem

normFormula_finite_mem_valuationSubring_iff_isIntegral_of_henselFactorization

L194 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_mem_valuationSubring_iff_isIntegral_of_henselFactorization

Documentation

The closed unit ball of the bundled norm formula consists exactly of the elements integral over the base valuation ring.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finite_mem_valuationSubring_iff_isIntegral_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 ∈ absoluteValueValuationSubring
        (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
          (K := K) (L := L) v hnonarch hv)
        (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean
          (K := K) (L := L) v hnonarch hv) ↔
      IsIntegral
        (absoluteValueValuationSubring v hnonarch) x

theorem

normFormula_finite_valuationSubring_eq_integralClosure_of_henselFactorization

L219 ↗

AlgebraicNumberTheory.Valuations.normFormula_finite_valuationSubring_eq_integralClosure_of_henselFactorization

Documentation

The valuation ring of the bundled finite norm formula is the actual integral closure of the base valuation ring in L.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem normFormula_finite_valuationSubring_eq_integralClosure_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)) :
    (absoluteValueValuationSubring
        (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization
          (K := K) (L := L) v hnonarch hv)
        (normFormula_finite_normFormulaAbsoluteValue_of_henselFactorization_nonarchimedean
          (K := K) (L := L) v hnonarch hv)).toSubring =
      (integralClosure
        (R := absoluteValueValuationSubring
          v hnonarch) L).toSubring

Module documentation

the finite norm-formula absolute value

Declarations