`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 : module R M} (x y : I.filtration M) (h : x.N = y.N) :

x = y

source

@[ext]

structure ideal.filtration {R : Type u} [comm_ring R] (I : ideal R) (M : Type u) [add_comm_group M] [module R M] :

Type u

N : ℕ → submodule R M
mono : ∀ (i : ℕ), self.N (i + 1) ≤ self.N i
smul_le : ∀ (i : ℕ), I • self.N i ≤ self.N (i + 1)

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

source

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 : module R M} (x y : I.filtration M) :

x = y ↔ x.N = y.N

source

theorem ideal.filtration.pow_smul_le {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) (i j : ℕ) :

I ^ i • F.N j ≤ F.N (i + j)

source

theorem ideal.filtration.pow_smul_le_pow_smul {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) (i j k : ℕ) :

I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

source

@[protected]

theorem ideal.filtration.antitone {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) :

antitone F.N

source

@[simp]

theorem ideal.trivial_filtration_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) (i : ℕ) :

(I.trivial_filtration N).N i = N

source

def ideal.trivial_filtration {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) :

I.filtration M

The trivial I-filtration of N.

Equations

I.trivial_filtration N = {N := λ (i : ℕ), N, mono := _, smul_le := _}

source

@[protected, instance]

def ideal.filtration.has_sup {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

has_sup (I.filtration M)

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

Equations

ideal.filtration.has_sup = {sup := λ (F F' : I.filtration M), {N := F.N ⊔ F'.N, mono := _, smul_le := _}}

source

@[protected, instance]

def ideal.filtration.has_Sup {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

has_Sup (I.filtration M)

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

Equations

ideal.filtration.has_Sup = {Sup := λ (S : set (I.filtration M)), {N := has_Sup.Sup (ideal.filtration.N '' S), mono := _, smul_le := _}}

source

@[protected, instance]

def ideal.filtration.has_inf {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

has_inf (I.filtration M)

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

Equations

ideal.filtration.has_inf = {inf := λ (F F' : I.filtration M), {N := F.N ⊓ F'.N, mono := _, smul_le := _}}

source

@[protected, instance]

def ideal.filtration.has_Inf {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

has_Inf (I.filtration M)

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

Equations

ideal.filtration.has_Inf = {Inf := λ (S : set (I.filtration M)), {N := has_Inf.Inf (ideal.filtration.N '' S), mono := _, smul_le := _}}

source

@[protected, instance]

def ideal.filtration.has_top {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

has_top (I.filtration M)

Equations

ideal.filtration.has_top = {top := I.trivial_filtration ⊤}

source

@[protected, instance]

def ideal.filtration.has_bot {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

has_bot (I.filtration M)

Equations

ideal.filtration.has_bot = {bot := I.trivial_filtration ⊥}

source

@[simp]

theorem ideal.filtration.sup_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F F' : I.filtration M) :

(F ⊔ F').N = F.N ⊔ F'.N

source

@[simp]

theorem ideal.filtration.Sup_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (S : set (I.filtration M)) :

(has_Sup.Sup S).N = has_Sup.Sup (ideal.filtration.N '' S)

source

@[simp]

theorem ideal.filtration.inf_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F F' : I.filtration M) :

(F ⊓ F').N = F.N ⊓ F'.N

source

@[simp]

theorem ideal.filtration.Inf_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (S : set (I.filtration M)) :

(has_Inf.Inf S).N = has_Inf.Inf (ideal.filtration.N '' S)

source

@[simp]

theorem ideal.filtration.top_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

⊤.N = ⊤

source

@[simp]

theorem ideal.filtration.bot_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

⊥.N = ⊥

source

@[simp]

theorem ideal.filtration.supr_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {ι : Sort u_1} (f : ι → I.filtration M) :

(supr f).N = ⨆ (i : ι), (f i).N

source

@[simp]

theorem ideal.filtration.infi_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {ι : Sort u_1} (f : ι → I.filtration M) :

(infi f).N = ⨅ (i : ι), (f i).N

source

@[protected, instance]

def ideal.filtration.complete_lattice {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

complete_lattice (I.filtration M)

Equations

ideal.filtration.complete_lattice = function.injective.complete_lattice ideal.filtration.N ideal.filtration.ext ideal.filtration.sup_N ideal.filtration.inf_N ideal.filtration.complete_lattice._proof_1 ideal.filtration.complete_lattice._proof_2 ideal.filtration.top_N ideal.filtration.bot_N

source

@[protected, instance]

def ideal.filtration.inhabited {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} :

inhabited (I.filtration M)

Equations

ideal.filtration.inhabited = {default := ⊥}

source

def ideal.filtration.stable {R M : Type u} [comm_ring R] [add_comm_group M] [module 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

F.stable = ∃ (n₀ : ℕ), ∀ (n : ℕ), n ≥ n₀ → I • F.N n = F.N (n + 1)

source

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

I.filtration M

The trivial stable I-filtration of N.

Equations

I.stable_filtration N = {N := λ (i : ℕ), I ^ i • N, mono := _, smul_le := _}

source

@[simp]

theorem ideal.stable_filtration_N {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) (i : ℕ) :

(I.stable_filtration N).N i = I ^ i • N

source

theorem ideal.stable_filtration_stable {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) :

(I.stable_filtration N).stable

source

theorem ideal.filtration.stable.exists_pow_smul_eq {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {F : I.filtration M} (h : F.stable) :

∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀

source

theorem ideal.filtration.stable.exists_pow_smul_eq_of_ge {R M : Type u} [comm_ring R] [add_comm_group M] [module 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₀

source

theorem ideal.filtration.stable_iff_exists_pow_smul_eq_of_ge {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {F : I.filtration M} :

F.stable ↔ ∃ (n₀ : ℕ), ∀ (n : ℕ), n ≥ n₀ → F.N n = I ^ (n - n₀) • F.N n₀

source

theorem ideal.filtration.stable.exists_forall_le {R M : Type u} [comm_ring R] [add_comm_group M] [module 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

source

theorem ideal.filtration.stable.bounded_difference {R M : Type u} [comm_ring R] [add_comm_group M] [module 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

source

@[protected]

def ideal.filtration.submodule {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) :

submodule ↥(rees_algebra I) (polynomial_module R M)

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

Equations

F.submodule = {carrier := {f : polynomial_module R M | ∀ (i : ℕ), ⇑f i ∈ F.N i}, add_mem' := _, zero_mem' := _, smul_mem' := _}

source

@[simp]

theorem ideal.filtration.mem_submodule {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) (f : polynomial_module R M) :

f ∈ F.submodule ↔ ∀ (i : ℕ), ⇑f i ∈ F.N i

source

theorem ideal.filtration.inf_submodule {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F F' : I.filtration M) :

(F ⊓ F').submodule = F.submodule ⊓ F'.submodule

source

def ideal.filtration.submodule_inf_hom {R : Type u} (M : Type u) [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) :

inf_hom (I.filtration M) (submodule ↥(rees_algebra I) (polynomial_module R M))

ideal.filtration.submodule as an inf_hom

Equations

ideal.filtration.submodule_inf_hom M I = {to_fun := ideal.filtration.submodule I, map_inf' := _}

source

theorem ideal.filtration.submodule_closure_single {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) :

add_submonoid.closure (⋃ (i : ℕ), ⇑(polynomial_module.single R i) '' ↑(F.N i)) = F.submodule.to_add_submonoid

source

theorem ideal.filtration.submodule_span_single {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) :

submodule.span ↥(rees_algebra I) (⋃ (i : ℕ), ⇑(polynomial_module.single R i) '' ↑(F.N i)) = F.submodule

source

theorem ideal.filtration.submodule_eq_span_le_iff_stable_ge {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) (n₀ : ℕ) :

F.submodule = submodule.span ↥(rees_algebra I) (⋃ (i : ℕ) (H : i ≤ n₀), ⇑(polynomial_module.single R i) '' ↑(F.N i)) ↔ ∀ (n : ℕ), n ≥ n₀ → I • F.N n = F.N (n + 1)

source

theorem ideal.filtration.submodule_fg_iff_stable {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} (F : I.filtration M) (hF' : ∀ (i : ℕ), (F.N i).fg) :

F.submodule.fg ↔ F.stable

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

source

theorem ideal.filtration.stable.of_le {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {F : I.filtration M} [is_noetherian_ring R] [h : module.finite R M] (hF : F.stable) {F' : I.filtration M} (hf : F' ≤ F) :

F'.stable

source

theorem ideal.filtration.stable.inter_right {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {F : I.filtration M} (F' : I.filtration M) [is_noetherian_ring R] [h : module.finite R M] (hF : F.stable) :

(F ⊓ F').stable

source

theorem ideal.filtration.stable.inter_left {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {F : I.filtration M} (F' : I.filtration M) [is_noetherian_ring R] [h : module.finite R M] (hF : F.stable) :

(F' ⊓ F).stable

source

theorem ideal.exists_pow_inf_eq_pow_smul {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) [is_noetherian_ring R] [h : module.finite R M] (N : submodule R M) :

∃ (k : ℕ), ∀ (n : ℕ), n ≥ k → I ^ n • ⊤ ⊓ N = I ^ (n - k) • (I ^ k • ⊤ ⊓ N)

Artin-Rees lemma

source

theorem ideal.mem_infi_smul_pow_eq_bot_iff {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) [is_noetherian_ring R] [hM : module.finite R M] (x : M) :

(x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ (r : ↥I), ↑r • x = x

source

theorem ideal.infi_pow_smul_eq_bot_of_local_ring {R M : Type u} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) [is_noetherian_ring R] [local_ring R] [module.finite R M] (h : I ≠ ⊤) :

(⨅ (i : ℕ), I ^ i • ⊤) = ⊥

source

theorem ideal.infi_pow_eq_bot_of_local_ring {R : Type u} [comm_ring R] (I : ideal R) [is_noetherian_ring R] [local_ring R] (h : I ≠ ⊤) :

(⨅ (i : ℕ), I ^ i) = ⊥

Krull's intersection theorem for noetherian local rings.

source

theorem ideal.infi_pow_eq_bot_of_is_domain {R : Type u} [comm_ring R] (I : ideal R) [is_noetherian_ring R] [is_domain R] (h : I ≠ ⊤) :

(⨅ (i : ℕ), I ^ i) = ⊥

Krull's intersection theorem for noetherian domains.

I-filtrations of modules #

Main results #

`I`-filtrations of modules #