I
-filtrations of modules #
This file contains the definitions and basic results around (stable) I
-filtrations of modules.
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
@[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 (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 : module R M}
(x y : I.filtration M) :
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 : ℕ) :
@[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) :
@[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
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
.
@[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.filtration
s is an I.filtration
.
@[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.filtration
s 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 := _}}
@[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.filtration
s is an I.filtration
.
@[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.filtration
s 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 := _}}
@[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
@[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
@[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) :
@[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)
@[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) :
@[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)
@[simp]
theorem
ideal.filtration.top_N
{R M : Type u}
[comm_ring R]
[add_comm_group M]
[module R M]
{I : ideal R} :
@[simp]
theorem
ideal.filtration.bot_N
{R M : Type u}
[comm_ring R]
[add_comm_group M]
[module R M]
{I : ideal R} :
@[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) :
@[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) :
@[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
@[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
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
.
@[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
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