English
Let F and F' be filtrations of a module M over an ideal-filtered ring I, with F and F' stable. If their 0-th levels coincide, F.N(0) = F'.N(0), then there exists an n0 ∈ ℕ such that for every n ∈ ℕ, F.N(n + n0) ⊆ F'.N(n) and F'.N(n + n0) ⊆ F.N(n). In words, the two filtrations become comparable after a fixed shift.
Русский
Пусть F и F' — фильтрации модуля M над кольцом с идеал-фильтрацией, оба стабильны. Если нулевые уровни совпадают, F.N(0) = F'.N(0), то существует n0 ∈ ℕ such that для любого n ∈ ℕ выполняются включения F.N(n + n0) ⊆ F'.N(n) и F'.N(n + n0) ⊆ F.N(n). Иными словами, после фиксации сдвига две фильтрации становятся сравнимыми.
LaTeX
$$$\\exists n_0 \\in \\mathbb{N}, \\forall n \\in \\mathbb{N},\\ F.N(n+n_0) \\le F'.N(n) \\land F'.N(n+n_0) \\le F.N(n).$$$
Lean4
theorem bounded_difference (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 :=
by
obtain ⟨n₁, h₁⟩ := h.exists_forall_le (le_of_eq e)
obtain ⟨n₂, h₂⟩ := h'.exists_forall_le (le_of_eq e.symm)
use max n₁ n₂
intro n
refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩ <;> simp
