exists_pow_inf_eq_pow_smul — Mathlib

English

For a Noetherian ring R and a finite R-module M, with I an ideal and N a submodule, there exists k ∈ ℕ such that for all n ≥ k, I^n M ∩ N = I^{n-k}(I^k M ∩ N).

Русский

Для кольца Ноера и конечного модуля M, при идеале I и подмодуле N существует k ∈ ℕ, значит для всех n ≥ k выполняется I^n M ∩ N = I^{n-k}(I^k M ∩ N).

LaTeX

$$$\\exists k \\in \\mathbb{N}, \\forall n \\ge k,\\ I^n M \\cap N = I^{n-k}(I^k M \\cap N).$$$

Lean4

/-- **Artin-Rees lemma** -/
theorem exists_pow_inf_eq_pow_smul [IsNoetherianRing R] [Module.Finite R M] (N : Submodule R M) :
    ∃ k : ℕ, ∀ n ≥ k, I ^ n • ⊤ ⊓ N = I ^ (n - k) • (I ^ k • ⊤ ⊓ N) :=
  ((I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)).exists_pow_smul_eq_of_ge

Похожие утверждения