Module

IdealAdicComplete.lean

Nyll.EtaleFundamentalGroups.Purity.Local.IdealAdicComplete

1 declaration indexed from sourceView source ↗

Module documentation

Adic completeness for ideals in a complete Noetherian local ring

A finite module over a Noetherian local ring that is complete for the maximal-ideal filtration is complete for every finer ideal-adic filtration. The key point is that the submodules I ^ n • M are closed for the maximal-adic topology: their quotients are finite modules and hence maximal-adically Hausdorff.

Imports1

Mathlib.RingTheory.AdicCompletion.Noetherian

Imported by3

theorem

isAdicComplete_of_le_maximalIdeal

L29 ↗

EtaleFundamentalGroups.Purity.isAdicComplete_of_le_maximalIdeal

Documentation

A finite module over a Noetherian local ring, complete for the maximal ideal, is complete for every ideal contained in the maximal ideal.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace EtaleFundamentalGroups.Purity
universe u v

Lean source · statement

theorem isAdicComplete_of_le_maximalIdeal
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (I : Ideal R) (hI : I ≤ maximalIdeal R)
    [IsAdicComplete (maximalIdeal R) M] :
    IsAdicComplete I M

Module documentation

Adic completeness for ideals in a complete Noetherian local ring

Declarations

isAdicComplete_of_le_maximalIdeal