English
A criterion for when AdicCompletion.mk I M f equals zero, given a tail condition implying eventual membership in deeper powers of I.
Русский
Критерий нуля для AdicCompletion.mk I M f при условии, что дальше f монтируется в более глубокие степени I.
LaTeX
$$$ \\forall f, \\exists k, \\forall n \\ge k, \\exists m \\ge n, \\exists l \\ge n, f m \\in (I^l \\cdot \\top) $ implies AdicCompletion.mk I M f = 0 $$$
Lean4
/-- The `I`-adic Cauchy condition can be checked on successive `n`. -/
theorem isAdicCauchy_iff (f : ℕ → M) : IsAdicCauchy I M f ↔ ∀ n, f n ≡ f (n + 1) [SMOD (I ^ n • ⊤ : Submodule R M)] :=
by
constructor
· intro h n
exact h (Nat.le_succ n)
· intro h m n hmn
induction n, hmn using Nat.le_induction with
| base => rfl
| succ n hmn ih =>
trans
· exact ih
· refine SModEq.mono (smul_mono (Ideal.pow_le_pow_right hmn) (by rfl)) (h n)
