NYLL
Module

AdicPower.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.AdicPower
14 declarations indexed from sourceView source ↗

Module documentation

Adic completeness and positive powers of an ideal

This file contains small generic source lemmas used to pass from completeness for a positive power I ^ n back to completeness for I.

Imports1
  • Mathlib.RingTheory.AdicCompletion.Functoriality
Imported by5

Declarations

theorem

isAdicComplete_of_linearEquiv

L28 ↗
ValuationTheory.DiscreteValuationField.isAdicComplete_of_linearEquiv
Documentation

Adic completeness is preserved by a linear equivalence of modules over the same base ring and with respect to the same ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isAdicComplete_of_linearEquiv
    (I : Ideal R) (e : M ≃ₗ[R] N) [IsAdicComplete I M] :
    IsAdicComplete I N
theorem

mem_map_algebraMap_pow_iff_mem_pow_smul_top

L56 ↗
ValuationTheory.DiscreteValuationField.mem_map_algebraMap_pow_iff_mem_pow_smul_top
Documentation

Membership in a power of the extended ideal is the same as membership in the corresponding base-adic submodule after restricting scalars.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem mem_map_algebraMap_pow_iff_mem_pow_smul_top
    {S : Type*} [CommRing S] [Algebra R S] (I : Ideal R)
    (n : ℕ) {x : S} :
    x ∈ (I.map (algebraMap R S)) ^ n ↔
      x ∈ I ^ n • (⊤ : Submodule R S)
theorem

mem_map_algebraMap_pow_smul_top_iff

L65 ↗
ValuationTheory.DiscreteValuationField.mem_map_algebraMap_pow_smul_top_iff
Documentation

The same scalar-restriction comparison as a submodule-membership statement.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem mem_map_algebraMap_pow_smul_top_iff
    {S : Type*} [CommRing S] [Algebra R S] (I : Ideal R)
    (n : ℕ) {x : S} :
    x ∈ ((I.map (algebraMap R S)) ^ n • ⊤ : Submodule S S) ↔
      x ∈ I ^ n • (⊤ : Submodule R S)
theorem

smodEq_map_algebraMap_pow_smul_top_iff

L76 ↗
ValuationTheory.DiscreteValuationField.smodEq_map_algebraMap_pow_smul_top_iff
Documentation

Congruence modulo powers of an extended ideal is unchanged after restricting scalars to the base ring.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem smodEq_map_algebraMap_pow_smul_top_iff
    {S : Type*} [CommRing S] [Algebra R S] (I : Ideal R)
    {x y : S} (n : ℕ) :
    x ≡ y [SMOD ((I.map (algebraMap R S)) ^ n • ⊤ : Submodule S S)] ↔
      x ≡ y [SMOD (I ^ n • ⊤ : Submodule R S)]
theorem

isPrecomplete_map_algebraMap_iff

L86 ↗
ValuationTheory.DiscreteValuationField.isPrecomplete_map_algebraMap_iff
Documentation

Restricting scalars along an algebra map does not change precompleteness for the ideal generated by the base ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isPrecomplete_map_algebraMap_iff
    {S : Type*} [CommRing S] [Algebra R S] (I : Ideal R) :
    IsPrecomplete (I.map (algebraMap R S)) S ↔ IsPrecomplete I S
theorem

isAdicComplete_map_algebraMap_iff

L114 ↗
ValuationTheory.DiscreteValuationField.isAdicComplete_map_algebraMap_iff
Documentation

Restricting scalars along an algebra map does not change adic completeness for the ideal generated by the base ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isAdicComplete_map_algebraMap_iff
    {S : Type*} [CommRing S] [Algebra R S] (I : Ideal R) :
    IsAdicComplete (I.map (algebraMap R S)) S ↔ IsAdicComplete I S
theorem

isAdicComplete_map_ringEquiv

L131 ↗
ValuationTheory.DiscreteValuationField.isAdicComplete_map_ringEquiv
Documentation

Adic completeness is preserved by transporting the ring and ideal across a ring equivalence.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isAdicComplete_map_ringEquiv
    {S : Type*} [CommRing S] (I : Ideal R) (e : R ≃+* S)
    [IsAdicComplete I R] :
    IsAdicComplete (I.map (e : R →+* S)) S
theorem

isHausdorff_pow_of_isHausdorff

L152 ↗
ValuationTheory.DiscreteValuationField.isHausdorff_pow_of_isHausdorff
Documentation

If a module is Hausdorff for an ideal, then it is Hausdorff for every positive power of that ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isHausdorff_pow_of_isHausdorff
    (I : Ideal R) {n : ℕ} (hn : 0 < n)
    [IsHausdorff I M] :
    IsHausdorff (I ^ n) M
theorem

isPrecomplete_pow_of_isPrecomplete

L166 ↗
ValuationTheory.DiscreteValuationField.isPrecomplete_pow_of_isPrecomplete
Documentation

If a module is precomplete for an ideal, then it is precomplete for every positive power of that ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isPrecomplete_pow_of_isPrecomplete
    (I : Ideal R) {n : ℕ} (hn : 0 < n)
    [IsPrecomplete I M] :
    IsPrecomplete (I ^ n) M
theorem

isAdicComplete_pow_of_isAdicComplete

L197 ↗
ValuationTheory.DiscreteValuationField.isAdicComplete_pow_of_isAdicComplete
Documentation

If a module is complete for an ideal, then it is complete for every positive power of that ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · full declaration
theorem isAdicComplete_pow_of_isAdicComplete
    (I : Ideal R) {n : ℕ} (hn : 0 < n)
    [IsAdicComplete I M] :
    IsAdicComplete (I ^ n) M where
  toIsHausdorff := isHausdorff_pow_of_isHausdorff (M := M) I hn
  toIsPrecomplete := isPrecomplete_pow_of_isPrecomplete (M := M) I hn
theorem

isHausdorff_of_isHausdorff_pow

L206 ↗
ValuationTheory.DiscreteValuationField.isHausdorff_of_isHausdorff_pow
Documentation

If a module is Hausdorff for a positive power of an ideal, then it is Hausdorff for the ideal itself.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isHausdorff_of_isHausdorff_pow
    (I : Ideal R) {n : ℕ} (_hn : 0 < n)
    [IsHausdorff (I ^ n) M] :
    IsHausdorff I M
theorem

isPrecomplete_of_isPrecomplete_pow

L217 ↗
ValuationTheory.DiscreteValuationField.isPrecomplete_of_isPrecomplete_pow
Documentation

If a module is precomplete for a positive power of an ideal, then it is precomplete for the ideal itself.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isPrecomplete_of_isPrecomplete_pow
    (I : Ideal R) {n : ℕ} (hn : 0 < n)
    [IsPrecomplete (I ^ n) M] :
    IsPrecomplete I M
theorem

isAdicComplete_of_isAdicComplete_pow

L247 ↗
ValuationTheory.DiscreteValuationField.isAdicComplete_of_isAdicComplete_pow
Documentation

If a module is complete for a positive power of an ideal, then it is complete for the ideal itself.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · full declaration
theorem isAdicComplete_of_isAdicComplete_pow
    (I : Ideal R) {n : ℕ} (hn : 0 < n)
    [IsAdicComplete (I ^ n) M] :
    IsAdicComplete I M where
  toIsHausdorff := isHausdorff_of_isHausdorff_pow (M := M) I hn
  toIsPrecomplete := isPrecomplete_of_isPrecomplete_pow (M := M) I hn
theorem

isAdicComplete_of_le_of_pow_le

L259 ↗
ValuationTheory.DiscreteValuationField.isAdicComplete_of_le_of_pow_le
Documentation

Adic completeness is unchanged when two ideals define cofinal power filtrations. The hypotheses I ≤ J and J ^ n ≤ I, with n > 0, are the asymmetric form convenient for finite integral extensions: the extended base ideal lies in the maximal ideal upstairs, while a positive power of that maximal ideal lies back in the extended ideal.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {N : Type*} [AddCommGroup N] [Module R N]
Lean source · statement
theorem isAdicComplete_of_le_of_pow_le
    (I J : Ideal R) {n : ℕ} (hn : 0 < n)
    (hIJ : I ≤ J) (hJI : J ^ n ≤ I)
    [IsAdicComplete I M] :
    IsAdicComplete J M

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