English
For Noetherian R and finite R-modules N, AdicCompletion.map I f preserves injectivity when f is injective.
Русский
При отсутствии противоречий в кольцах Р и конечных модулях, инъективность сохраняется под образованием AdicCompletion.map.
LaTeX
$$$\text{map I f is injective}$ under $\text{IsNoetherianRing } R$ and $\text{Module.Finite } R N$ and $f$ injective$$
Lean4
/-- Adic completion preserves injectivity of finite modules over a Noetherian ring. -/
theorem map_injective {f : M →ₗ[R] N} (hf : Function.Injective f) : Function.Injective (map I f) :=
by
obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (range f)
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
intro x
apply AdicCompletion.induction_on I M x (fun a ↦ ?_)
intro hx
refine AdicCompletion.mk_zero_of _ _ _ ⟨42, fun n _ ↦ ⟨n + k, by cutsat, n, by cutsat, ?_⟩⟩
rw [← Submodule.comap_map_eq_of_injective hf (I ^ n • ⊤ : Submodule R M), Submodule.map_smul'', Submodule.map_top]
apply (smul_mono_right _ inf_le_right : I ^ n • (I ^ k • ⊤ ⊓ (range f)) ≤ _)
nth_rw 1 [show n = n + k - k by cutsat]
rw [← hk (n + k) (show n + k ≥ k by cutsat)]
exact ⟨by simpa using congrArg (fun x ↦ x.val (n + k)) hx, ⟨a (n + k), rfl⟩⟩
