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 : CommRing R} {I : Ideal R} {M : Type u} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (x y : Ideal.Filtration I M), x.N = y.N → x = y

theorem Ideal.Filtration.ext_iff {R : Type u} : ∀ {inst : CommRing R} {I : Ideal R} {M : Type u} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (x y : Ideal.Filtration I M), x = y ↔ x.N = y.N

structure Ideal.Filtration {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup 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) ≤ N (i + 1). Note that we do not require the filtration to start from ⊤.

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

theorem Ideal.Filtration.pow_smul_le {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (i : ℕ) (j : ℕ) : I ^ i • F.N j ≤ F.N (i + j)

theorem Ideal.Filtration.pow_smul_le_pow_smul {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (i : ℕ) (j : ℕ) (k : ℕ) : I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

theorem Ideal.Filtration.antitone {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) : Antitone F.N

@[simp]

theorem Ideal.trivialFiltration_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) : ∀ (x : ℕ), (Ideal.trivialFiltration I N).N x = N

def Ideal.trivialFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) : Ideal.Filtration I M

The trivial I-filtration of N.

Equations

• Ideal.trivialFiltration I N = { N := fun (x : ℕ) => N, mono := ⋯, smul_le := ⋯ }

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

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

Equations

• Ideal.Filtration.instSupFiltration = { sup := fun (F F' : Ideal.Filtration I M) => { N := F.N ⊔ F'.N, mono := ⋯, smul_le := ⋯ } }

instance Ideal.Filtration.instSupSetFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : SupSet (Ideal.Filtration I M)

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

Equations

• Ideal.Filtration.instSupSetFiltration = { sSup := fun (S : Set (Ideal.Filtration I M)) => { N := sSup (Ideal.Filtration.N '' S), mono := ⋯, smul_le := ⋯ } }

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

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

Equations

• Ideal.Filtration.instInfFiltration = { inf := fun (F F' : Ideal.Filtration I M) => { N := F.N ⊓ F'.N, mono := ⋯, smul_le := ⋯ } }

instance Ideal.Filtration.instInfSetFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : InfSet (Ideal.Filtration I M)

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

Equations

• Ideal.Filtration.instInfSetFiltration = { sInf := fun (S : Set (Ideal.Filtration I M)) => { N := sInf (Ideal.Filtration.N '' S), mono := ⋯, smul_le := ⋯ } }

instance Ideal.Filtration.instTopFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : Top (Ideal.Filtration I M)

Equations

• Ideal.Filtration.instTopFiltration = { top := Ideal.trivialFiltration I ⊤ }

instance Ideal.Filtration.instBotFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : Bot (Ideal.Filtration I M)

Equations

• Ideal.Filtration.instBotFiltration = { bot := Ideal.trivialFiltration I ⊥ }

@[simp]

theorem Ideal.Filtration.sup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (F' : Ideal.Filtration I M) : (F ⊔ F').N = F.N ⊔ F'.N

@[simp]

theorem Ideal.Filtration.sSup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (S : Set (Ideal.Filtration I M)) : (sSup S).N = sSup (Ideal.Filtration.N '' S)

@[simp]

theorem Ideal.Filtration.inf_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (F' : Ideal.Filtration I M) : (F ⊓ F').N = F.N ⊓ F'.N

@[simp]

theorem Ideal.Filtration.sInf_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (S : Set (Ideal.Filtration I M)) : (sInf S).N = sInf (Ideal.Filtration.N '' S)

@[simp]

theorem Ideal.Filtration.top_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : ⊤.N = ⊤

@[simp]

theorem Ideal.Filtration.bot_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : ⊥.N = ⊥

@[simp]

theorem Ideal.Filtration.iSup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {ι : Sort u_1} (f : ι → Ideal.Filtration I M) : (iSup f).N = ⨆ (i : ι), (f i).N

@[simp]

theorem Ideal.Filtration.iInf_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {ι : Sort u_1} (f : ι → Ideal.Filtration I M) : (iInf f).N = ⨅ (i : ι), (f i).N

instance Ideal.Filtration.instCompleteLatticeFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : CompleteLattice (Ideal.Filtration I M)

Equations

• Ideal.Filtration.instCompleteLatticeFiltration = Function.Injective.completeLattice Ideal.Filtration.N ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Ideal.Filtration.instInhabitedFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} : Inhabited (Ideal.Filtration I M)

Equations

• Ideal.Filtration.instInhabitedFiltration = { default := ⊥ }

def Ideal.Filtration.Stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) : Prop

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

Equations

• Ideal.Filtration.Stable F = ∃ (n₀ : ℕ), ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

@[simp]

theorem Ideal.stableFiltration_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (i : ℕ) : (Ideal.stableFiltration I N).N i = I ^ i • N

def Ideal.stableFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) : Ideal.Filtration I M

The trivial stable I-filtration of N.

Equations

• Ideal.stableFiltration I N = { N := fun (i : ℕ) => I ^ i • N, mono := ⋯, smul_le := ⋯ }

theorem Ideal.stableFiltration_stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) : Ideal.Filtration.Stable (Ideal.stableFiltration I N)

theorem Ideal.Filtration.Stable.exists_pow_smul_eq {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} (h : Ideal.Filtration.Stable F) : ∃ (n₀ : ℕ), ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀

theorem Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} (h : Ideal.Filtration.Stable F) : ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

theorem Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} : Ideal.Filtration.Stable F ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

theorem Ideal.Filtration.Stable.exists_forall_le {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} {F' : Ideal.Filtration I M} (h : Ideal.Filtration.Stable F) (e : F.N 0 ≤ F'.N 0) : ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n

theorem Ideal.Filtration.Stable.bounded_difference {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} {F' : Ideal.Filtration I M} (h : Ideal.Filtration.Stable F) (h' : Ideal.Filtration.Stable F') (e : F.N 0 = F'.N 0) : ∃ (n₀ : ℕ), ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

def Ideal.Filtration.submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) : Submodule (↥(reesAlgebra I)) (PolynomialModule R M)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.Filtration.mem_submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (f : PolynomialModule R M) : f ∈ Ideal.Filtration.submodule F ↔ ∀ (i : ℕ), f i ∈ F.N i

theorem Ideal.Filtration.inf_submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (F' : Ideal.Filtration I M) : Ideal.Filtration.submodule (F ⊓ F') = Ideal.Filtration.submodule F ⊓ Ideal.Filtration.submodule F'

def Ideal.Filtration.submoduleInfHom {R : Type u} (M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : InfHom (Ideal.Filtration I M) (Submodule (↥(reesAlgebra I)) (PolynomialModule R M))

Ideal.Filtration.submodule as an InfHom.

Equations

• Ideal.Filtration.submoduleInfHom M I = { toFun := Ideal.Filtration.submodule, map_inf' := ⋯ }

theorem Ideal.Filtration.submodule_closure_single {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) : AddSubmonoid.closure (⋃ (i : ℕ), ⇑(PolynomialModule.single R i) '' ↑(F.N i)) = (Ideal.Filtration.submodule F).toAddSubmonoid

theorem Ideal.Filtration.submodule_span_single {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) : Submodule.span (↥(reesAlgebra I)) (⋃ (i : ℕ), ⇑(PolynomialModule.single R i) '' ↑(F.N i)) = Ideal.Filtration.submodule F

theorem Ideal.Filtration.submodule_eq_span_le_iff_stable_ge {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (n₀ : ℕ) : Ideal.Filtration.submodule F = Submodule.span (↥(reesAlgebra I)) (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), ⇑(PolynomialModule.single R i) '' ↑(F.N i)) ↔ ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

theorem Ideal.Filtration.submodule_fg_iff_stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (hF' : ∀ (i : ℕ), Submodule.FG (F.N i)) : Submodule.FG (Ideal.Filtration.submodule F) ↔ Ideal.Filtration.Stable F

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} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} [IsNoetherianRing R] [Module.Finite R M] (hF : Ideal.Filtration.Stable F) {F' : Ideal.Filtration I M} (hf : F' ≤ F) : Ideal.Filtration.Stable F'

theorem Ideal.Filtration.Stable.inter_right {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} (F' : Ideal.Filtration I M) [IsNoetherianRing R] [Module.Finite R M] (hF : Ideal.Filtration.Stable F) : Ideal.Filtration.Stable (F ⊓ F')

theorem Ideal.Filtration.Stable.inter_left {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} (F' : Ideal.Filtration I M) [IsNoetherianRing R] [Module.Finite R M] (hF : Ideal.Filtration.Stable F) : Ideal.Filtration.Stable (F' ⊓ F)

theorem Ideal.exists_pow_inf_eq_pow_smul {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) [IsNoetherianRing R] [Module.Finite R M] (N : Submodule R M) : ∃ (k : ℕ), ∀ n ≥ k, I ^ 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} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) [IsNoetherianRing R] [Module.Finite R M] (x : M) : x ∈ ⨅ (i : ℕ), I ^ i • ⊤ ↔ ∃ (r : ↥I), ↑r • x = x

theorem Ideal.iInf_pow_smul_eq_bot_of_localRing {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) [IsNoetherianRing R] [LocalRing R] [Module.Finite R M] (h : I ≠ ⊤) : ⨅ (i : ℕ), I ^ i • ⊤ = ⊥

theorem Ideal.iInf_pow_eq_bot_of_localRing {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] [LocalRing R] (h : I ≠ ⊤) : ⨅ (i : ℕ), I ^ i = ⊥

Krull's intersection theorem for noetherian local rings.

theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [LocalRing R] (I : Ideal R) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Also see Ideal.isIdempotentElem_iff_eq_bot_or_top for integral domains.

theorem Ideal.iInf_pow_eq_bot_of_isDomain {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsDomain R] (h : I ≠ ⊤) : ⨅ (i : ℕ), I ^ i = ⊥

Krull's intersection theorem for noetherian domains.