mathlib documentation

ring_theory.filtration

I-filtrations of modules #

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

source
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

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 ⊤.

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
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
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
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
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
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
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
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
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
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
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
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