# mathlib3documentation

ring_theory.filtration

# I-filtrations of modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.infi_pow_eq_bot_of_local_ring: Krull's intersection theorem (⨅ i, I ^ i = ⊥) for noetherian local rings.
• ideal.infi_pow_eq_bot_of_is_domain: Krull's intersection theorem (⨅ i, I ^ i = ⊥) for noetherian domains.
theorem ideal.filtration.ext {R : Type u} {_inst_1 : comm_ring R} {I : ideal R} {M : Type u} {_inst_4 : add_comm_group M} {_inst_5 : M} (x y : I.filtration M) (h : x.N = y.N) :
x = y
@[ext]
structure ideal.filtration {R : Type u} [comm_ring R] (I : ideal R) (M : Type u) [ 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 ideal.filtration
theorem ideal.filtration.ext_iff {R : Type u} {_inst_1 : comm_ring R} {I : ideal R} {M : Type u} {_inst_4 : add_comm_group M} {_inst_5 : M} (x y : I.filtration M) :
x = y x.N = y.N
theorem ideal.filtration.pow_smul_le {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) (i j : ) :
I ^ i F.N j F.N (i + j)
theorem ideal.filtration.pow_smul_le_pow_smul {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) (i j k : ) :
I ^ (i + k) F.N j I ^ k F.N (i + j)
@[protected]
theorem ideal.filtration.antitone {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) :
@[simp]
theorem ideal.trivial_filtration_N {R M : Type u} [comm_ring R] [ M] (I : ideal R) (N : M) (i : ) :
def ideal.trivial_filtration {R M : Type u} [comm_ring R] [ M] (I : ideal R) (N : M) :

The trivial I-filtration of N.

Equations
@[protected, instance]
def ideal.filtration.has_sup {R M : Type u} [comm_ring R] [ M] {I : ideal R} :

The sup of two I.filtrations is an I.filtration.

Equations
@[protected, instance]
def ideal.filtration.has_Sup {R M : Type u} [comm_ring R] [ M] {I : ideal R} :

The Sup of a family of I.filtrations is an I.filtration.

Equations
@[protected, instance]
def ideal.filtration.has_inf {R M : Type u} [comm_ring R] [ M] {I : ideal R} :

The inf of two I.filtrations is an I.filtration.

Equations
@[protected, instance]
def ideal.filtration.has_Inf {R M : Type u} [comm_ring R] [ M] {I : ideal R} :

The Inf of a family of I.filtrations is an I.filtration.

Equations
@[protected, instance]
def ideal.filtration.has_top {R M : Type u} [comm_ring R] [ M] {I : ideal R} :
Equations
@[protected, instance]
def ideal.filtration.has_bot {R M : Type u} [comm_ring R] [ M] {I : ideal R} :
Equations
@[simp]
theorem ideal.filtration.sup_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F F' : I.filtration M) :
(F F').N = F.N F'.N
@[simp]
theorem ideal.filtration.Sup_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} (S : set (I.filtration M)) :
@[simp]
theorem ideal.filtration.inf_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F F' : I.filtration M) :
(F F').N = F.N F'.N
@[simp]
theorem ideal.filtration.Inf_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} (S : set (I.filtration M)) :
@[simp]
theorem ideal.filtration.top_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} :
@[simp]
theorem ideal.filtration.bot_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} :
@[simp]
theorem ideal.filtration.supr_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} {ι : Sort u_1} (f : ι I.filtration M) :
(supr f).N = (i : ι), (f i).N
@[simp]
theorem ideal.filtration.infi_N {R M : Type u} [comm_ring R] [ M] {I : ideal R} {ι : Sort u_1} (f : ι I.filtration M) :
(infi f).N = (i : ι), (f i).N
@[protected, instance]
def ideal.filtration.complete_lattice {R M : Type u} [comm_ring R] [ M] {I : ideal R} :
Equations
@[protected, instance]
def ideal.filtration.inhabited {R M : Type u} [comm_ring R] [ M] {I : ideal R} :
Equations
def ideal.filtration.stable {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) :
Prop

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

Equations
def ideal.stable_filtration {R M : Type u} [comm_ring R] [ M] (I : ideal R) (N : M) :

The trivial stable I-filtration of N.

Equations
@[simp]
theorem ideal.stable_filtration_N {R M : Type u} [comm_ring R] [ M] (I : ideal R) (N : M) (i : ) :
(I.stable_filtration N).N i = I ^ i N
theorem ideal.stable_filtration_stable {R M : Type u} [comm_ring R] [ M] (I : ideal R) (N : M) :
theorem ideal.filtration.stable.exists_pow_smul_eq {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F : I.filtration M} (h : F.stable) :
(n₀ : ), (k : ), F.N (n₀ + k) = I ^ k F.N n₀
theorem ideal.filtration.stable.exists_pow_smul_eq_of_ge {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F : I.filtration M} (h : F.stable) :
(n₀ : ), (n : ), n n₀ F.N n = I ^ (n - n₀) F.N n₀
theorem ideal.filtration.stable_iff_exists_pow_smul_eq_of_ge {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F : I.filtration M} :
F.stable (n₀ : ), (n : ), n n₀ F.N n = I ^ (n - n₀) F.N n₀
theorem ideal.filtration.stable.exists_forall_le {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F F' : I.filtration M} (h : F.stable) (e : F.N 0 F'.N 0) :
(n₀ : ), (n : ), F.N (n + n₀) F'.N n
theorem ideal.filtration.stable.bounded_difference {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F F' : I.filtration M} (h : F.stable) (h' : F'.stable) (e : F.N 0 = F'.N 0) :
(n₀ : ), (n : ), F.N (n + n₀) F'.N n F'.N (n + n₀) F.N n
@[protected]
def ideal.filtration.submodule {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) :
M)

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

Equations
@[simp]
theorem ideal.filtration.mem_submodule {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) (f : M) :
f F.submodule (i : ), f i F.N i
theorem ideal.filtration.inf_submodule {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F F' : I.filtration M) :
def ideal.filtration.submodule_inf_hom {R : Type u} (M : Type u) [comm_ring R] [ M] (I : ideal R) :

ideal.filtration.submodule as an inf_hom

Equations
theorem ideal.filtration.submodule_span_single {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) :
( (i : ), '' (F.N i)) = F.submodule
theorem ideal.filtration.submodule_eq_span_le_iff_stable_ge {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) (n₀ : ) :
F.submodule = ( (i : ) (H : i n₀), '' (F.N i)) (n : ), n n₀ I F.N n = F.N (n + 1)
theorem ideal.filtration.submodule_fg_iff_stable {R M : Type u} [comm_ring R] [ M] {I : ideal R} (F : I.filtration M) (hF' : (i : ), (F.N i).fg) :

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 M : Type u} [comm_ring R] [ M] {I : ideal R} {F : I.filtration M} [h : M] (hF : F.stable) {F' : I.filtration M} (hf : F' F) :
theorem ideal.filtration.stable.inter_right {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F : I.filtration M} (F' : I.filtration M) [h : M] (hF : F.stable) :
(F F').stable
theorem ideal.filtration.stable.inter_left {R M : Type u} [comm_ring R] [ M] {I : ideal R} {F : I.filtration M} (F' : I.filtration M) [h : M] (hF : F.stable) :
(F' F).stable
theorem ideal.exists_pow_inf_eq_pow_smul {R M : Type u} [comm_ring R] [ M] (I : ideal R) [h : M] (N : M) :
(k : ), (n : ), n k I ^ n N = I ^ (n - k) (I ^ k N)

Artin-Rees lemma

theorem ideal.mem_infi_smul_pow_eq_bot_iff {R M : Type u} [comm_ring R] [ M] (I : ideal R) [hM : M] (x : M) :
(x (i : ), I ^ i ) (r : I), r x = x
theorem ideal.infi_pow_smul_eq_bot_of_local_ring {R M : Type u} [comm_ring R] [ M] (I : ideal R) [local_ring R] [ M] (h : I ) :
( (i : ), I ^ i ) =
theorem ideal.infi_pow_eq_bot_of_local_ring {R : Type u} [comm_ring R] (I : ideal R) [local_ring R] (h : I ) :
( (i : ), I ^ i) =

Krull's intersection theorem for noetherian local rings.

theorem ideal.infi_pow_eq_bot_of_is_domain {R : Type u} [comm_ring R] (I : ideal R) [is_domain R] (h : I ) :
( (i : ), I ^ i) =

Krull's intersection theorem for noetherian domains.