# Documentation

Mathlib.RingTheory.Filtration

# I-filtrations of modules #

This file contains the definitions and basic results around (stable) I-filtrations of modules.

## Main results #

• Ideal.Filtration: An I-filtration on the module M is a sequence of decreasing submodules N i such that I • N ≤ I (i + 1). Note that we do not require the filtration to start from ⊤.
• Ideal.Filtration.Stable: An I-filtration is stable if I • (N i) = N (i + 1) for large enough i.
• Ideal.Filtration.submodule: The associated module ⨁ Nᵢ of a filtration, implemented as a submodule of M[X].
• Ideal.Filtration.submodule_fg_iff_stable: If F.N i are all finitely generated, then F.Stable iff F.submodule.FG.
• 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 k such that 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.
theorem Ideal.Filtration.ext {R : Type u} :
∀ {inst : } {I : } {M : Type u} {inst_1 : } {inst_2 : Module R M} (x y : ), x.N = y.Nx = y
theorem Ideal.Filtration.ext_iff {R : Type u} :
∀ {inst : } {I : } {M : Type u} {inst_1 : } {inst_2 : Module R M} (x y : ), x = y x.N = y.N
structure Ideal.Filtration {R : Type u} [] (I : ) (M : Type u) [] [Module R M] :

An I-filtration on the module M is a sequence of decreasing submodules N i such that I • (N i) ≤ N (i + 1). Note that we do not require the filtration to start from ⊤.

Instances For
theorem Ideal.Filtration.pow_smul_le {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (i : ) (j : ) :
theorem Ideal.Filtration.pow_smul_le_pow_smul {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (i : ) (j : ) (k : ) :
I ^ (i + k) I ^ k Ideal.Filtration.N F (i + j)
theorem Ideal.Filtration.antitone {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) :
@[simp]
theorem Ideal.trivialFiltration_N {R : Type u} {M : Type u} [] [] [Module R M] (I : ) (N : ) :
∀ (x : ),
def Ideal.trivialFiltration {R : Type u} {M : Type u} [] [] [Module R M] (I : ) (N : ) :

The trivial I-filtration of N.

Instances For
instance Ideal.Filtration.instSupFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
Sup ()

The sup of two I.Filtrations is an I.Filtration.

instance Ideal.Filtration.instSupSetFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :

The sSup of a family of I.Filtrations is an I.Filtration.

instance Ideal.Filtration.instInfFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
Inf ()

The inf of two I.Filtrations is an I.Filtration.

instance Ideal.Filtration.instInfSetFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :

The sInf of a family of I.Filtrations is an I.Filtration.

instance Ideal.Filtration.instTopFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
Top ()
instance Ideal.Filtration.instBotFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
Bot ()
@[simp]
theorem Ideal.Filtration.sup_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (F' : ) :
(F F').N = F.N F'.N
@[simp]
theorem Ideal.Filtration.sSup_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } (S : Set ()) :
(sSup S).N = sSup (Ideal.Filtration.N '' S)
@[simp]
theorem Ideal.Filtration.inf_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (F' : ) :
(F F').N = F.N F'.N
@[simp]
theorem Ideal.Filtration.sInf_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } (S : Set ()) :
(sInf S).N = sInf (Ideal.Filtration.N '' S)
@[simp]
theorem Ideal.Filtration.top_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
@[simp]
theorem Ideal.Filtration.bot_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
@[simp]
theorem Ideal.Filtration.iSup_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } {ι : Sort u_1} (f : ι) :
(iSup f).N = ⨆ (i : ι), (f i).N
@[simp]
theorem Ideal.Filtration.iInf_N {R : Type u} {M : Type u} [] [] [Module R M] {I : } {ι : Sort u_1} (f : ι) :
(iInf f).N = ⨅ (i : ι), (f i).N
instance Ideal.Filtration.instCompleteLatticeFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
instance Ideal.Filtration.instInhabitedFiltration {R : Type u} {M : Type u} [] [] [Module R M] {I : } :
def Ideal.Filtration.Stable {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) :

An I filtration is stable if I • F.N n = F.N (n+1) for large enough n.

Instances For
@[simp]
theorem Ideal.stableFiltration_N {R : Type u} {M : Type u} [] [] [Module R M] (I : ) (N : ) (i : ) :
= I ^ i N
def Ideal.stableFiltration {R : Type u} {M : Type u} [] [] [Module R M] (I : ) (N : ) :

The trivial stable I-filtration of N.

Instances For
theorem Ideal.stableFiltration_stable {R : Type u} {M : Type u} [] [] [Module R M] (I : ) (N : ) :
theorem Ideal.Filtration.Stable.exists_pow_smul_eq {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } (h : ) :
n₀, ∀ (k : ), Ideal.Filtration.N F (n₀ + k) = I ^ k
theorem Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } (h : ) :
n₀, ∀ (n : ), n n₀ = I ^ (n - n₀)
theorem Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } :
n₀, ∀ (n : ), n n₀ = I ^ (n - n₀)
theorem Ideal.Filtration.Stable.exists_forall_le {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } {F' : } (h : ) (e : ) :
n₀, ∀ (n : ), Ideal.Filtration.N F (n + n₀)
theorem Ideal.Filtration.Stable.bounded_difference {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } {F' : } (h : ) (h' : ) (e : ) :
n₀, ∀ (n : ), Ideal.Filtration.N F (n + n₀) Ideal.Filtration.N F' (n + n₀)
def Ideal.Filtration.submodule {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) :
Submodule { x // x } ()

The R[IX]-submodule of M[X] associated with an I-filtration.

Instances For
@[simp]
theorem Ideal.Filtration.mem_submodule {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (f : ) :
∀ (i : ), f i
theorem Ideal.Filtration.inf_submodule {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (F' : ) :
def Ideal.Filtration.submoduleInfHom {R : Type u} (M : Type u) [] [] [Module R M] (I : ) :
InfHom () (Submodule { x // x } ())

Ideal.Filtration.submodule as an InfHom.

Instances For
theorem Ideal.Filtration.submodule_closure_single {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) :
theorem Ideal.Filtration.submodule_span_single {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) :
Submodule.span { x // x } (⋃ (i : ), ↑() '' ↑()) =
theorem Ideal.Filtration.submodule_eq_span_le_iff_stable_ge {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (n₀ : ) :
= Submodule.span { x // x } (⋃ (i : ) (_ : i n₀), ↑() '' ↑()) ∀ (n : ), n n₀I = Ideal.Filtration.N F (n + 1)
theorem Ideal.Filtration.submodule_fg_iff_stable {R : Type u} {M : Type u} [] [] [Module R M] {I : } (F : ) (hF' : ∀ (i : ), ) :

If the components of a filtration are finitely generated, then the filtration is stable iff its associated submodule of is finitely generated.

theorem Ideal.Filtration.Stable.of_le {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } [] [] (hF : ) {F' : } (hf : F' F) :
theorem Ideal.Filtration.Stable.inter_right {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } (F' : ) [] [] (hF : ) :
theorem Ideal.Filtration.Stable.inter_left {R : Type u} {M : Type u} [] [] [Module R M] {I : } {F : } (F' : ) [] [] (hF : ) :
theorem Ideal.exists_pow_inf_eq_pow_smul {R : Type u} {M : Type u} [] [] [Module R M] (I : ) [] [] (N : ) :
k, ∀ (n : ), n kI ^ n N = I ^ (n - k) (I ^ k N)

Artin-Rees lemma

theorem Ideal.mem_iInf_smul_pow_eq_bot_iff {R : Type u} {M : Type u} [] [] [Module R M] (I : ) [] [] (x : M) :
x ⨅ (i : ), I ^ i r, r x = x
theorem Ideal.iInf_pow_smul_eq_bot_of_localRing {R : Type u} {M : Type u} [] [] [Module R M] (I : ) [] [] [] (h : I ) :
⨅ (i : ), I ^ i =
theorem Ideal.iInf_pow_eq_bot_of_localRing {R : Type u} [] (I : ) [] [] (h : I ) :
⨅ (i : ), I ^ i =

Krull's intersection theorem for noetherian local rings.

theorem Ideal.iInf_pow_eq_bot_of_isDomain {R : Type u} [] (I : ) [] [] (h : I ) :
⨅ (i : ), I ^ i =

Krull's intersection theorem for noetherian domains.