Module

PrincipalAdicCompleteness.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.PrincipalAdicCompleteness

5 declarations indexed from sourceView source ↗

Module documentation

Principal adic filtrations in complete nonarchimedean valuation rings

For a complete nonarchimedean absolute value, a nonzero element of the open unit ball generates a separated and precomplete principal filtration on the closed unit ball. These facts are shared by the coefficientwise Hensel construction and the irreducible-polynomial coefficient estimate.

Imports3

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.ValuationSubring
Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Completeness
Mathlib.RingTheory.AdicCompletion.Basic

Imported by5

theorem

principal_pow_mem_iff_abs_le

L27 ↗

AlgebraicNumberTheory.Valuations.principal_pow_mem_iff_abs_le

Documentation

Membership in the π-adic principal power is exactly the corresponding absolute-value bound on the closed unit ball of a nonarchimedean valued field.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem principal_pow_mem_iff_abs_le
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {π x : absoluteValueValuationSubring v hnonarch}
    (hπne : π ≠ 0) (n : ℕ) :
    x ∈ (Ideal.span ({π} : Set
        (absoluteValueValuationSubring v hnonarch))) ^ n ↔
      v (x : K) ≤ v ((π : absoluteValueValuationSubring v hnonarch) : K) ^ n

theorem

principal_smodEq_iff_abs_sub_le

L78 ↗

AlgebraicNumberTheory.Valuations.principal_smodEq_iff_abs_sub_le

Documentation

Principal congruence modulo (π)^n is exactly an absolute-value bound for the difference.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem principal_smodEq_iff_abs_sub_le
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {π x y : absoluteValueValuationSubring v hnonarch}
    (hπne : π ≠ 0) {n : ℕ} :
    x ≡ y [SMOD
      ((Ideal.span ({π} : Set
        (absoluteValueValuationSubring v hnonarch))) ^ n •
          ⊤ : Submodule
            (absoluteValueValuationSubring v hnonarch)
            (absoluteValueValuationSubring v hnonarch))] ↔
    v ((x : K) - (y : K)) ≤
      v ((π : absoluteValueValuationSubring v hnonarch) : K) ^ n

theorem

abs_sub_le_of_principal_smodEq

L110 ↗

AlgebraicNumberTheory.Valuations.abs_sub_le_of_principal_smodEq

Documentation

Forward direction of principal_smodEq_iff_abs_sub_le.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem abs_sub_le_of_principal_smodEq
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {π x y : absoluteValueValuationSubring v hnonarch}
    (hπne : π ≠ 0) {n : ℕ}
    (hxy : x ≡ y [SMOD
      ((Ideal.span ({π} : Set
        (absoluteValueValuationSubring v hnonarch))) ^ n •
          ⊤ : Submodule
            (absoluteValueValuationSubring v hnonarch)
            (absoluteValueValuationSubring v hnonarch))]) :
    v ((x : K) - (y : K)) ≤
      v ((π : absoluteValueValuationSubring v hnonarch) : K) ^ n

theorem

principalHausdorff_of_nonzero_mem_maximalIdeal

L128 ↗

AlgebraicNumberTheory.Valuations.principalHausdorff_of_nonzero_mem_maximalIdeal

Documentation

Principal separatedness for the element π chosen in the proof, as soon as π is a nonzero element of the open unit ball.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem principalHausdorff_of_nonzero_mem_maximalIdeal
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {π : absoluteValueValuationSubring v hnonarch}
    (hπne : π ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch)) :
    IsHausdorff (Ideal.span ({π} : Set
      (absoluteValueValuationSubring v hnonarch)))
      (absoluteValueValuationSubring v hnonarch)

theorem

principalPrecomplete_of_complete

L163 ↗

AlgebraicNumberTheory.Valuations.principalPrecomplete_of_complete

Documentation

Principal precompleteness for the element π chosen in the proof, deduced from completeness of the valued field.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem principalPrecomplete_of_complete
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ)
    (hcomplete : IsCompleteForAbsoluteValue v)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {π : absoluteValueValuationSubring v hnonarch}
    (hπne : π ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch)) :
    IsPrecomplete (Ideal.span ({π} : Set
      (absoluteValueValuationSubring v hnonarch)))
      (absoluteValueValuationSubring v hnonarch)

Module documentation

Principal adic filtrations in complete nonarchimedean valuation rings

Declarations

principal_pow_mem_iff_abs_le

principal_smodEq_iff_abs_sub_le

abs_sub_le_of_principal_smodEq

principalHausdorff_of_nonzero_mem_maximalIdeal

principalPrecomplete_of_complete