I-filtrations of modules #
This file contains the definitions and basic results around (stable)
I-filtrations of modules.
Main results #
I-filtration on the module
Mis a sequence of decreasing submodules
N isuch that
I • N ≤ I (i + 1). Note that we do not require the filtration to start from
I-filtration is stable if
I • (N i) = N (i + 1)for large enough
Ideal.Filtration.submodule: The associated module
⨁ Nᵢof a filtration, implemented as a submodule of
F.N iare all finitely generated, then
Ideal.Filtration.Stable.of_le: In a finite module over a noetherian ring, if
F' ≤ F, then
F.Stable → F'.Stable.
Ideal.exists_pow_inf_eq_pow_smul: Artin-Rees lemma. given
N ≤ M, there exists a
IⁿM ⊓ N = Iⁿ⁻ᵏ(IᵏM ⊓ N)for all
n ≥ k.
Ideal.iInf_pow_eq_bot_of_localRing: Krull's intersection theorem (
⨅ i, I ^ i = ⊥) for noetherian local rings.
Ideal.iInf_pow_eq_bot_of_isDomain: Krull's intersection theorem (
⨅ i, I ^ i = ⊥) for noetherian domains.
If the components of a filtration are finitely generated, then the filtration is stable iff its associated submodule of is finitely generated.