map_ext'' — Mathlib

English

Exactness is preserved by AdicCompletion map for Noetherian rings and finite modules: if f,g are exact and f injective, then map I f and map I g are exact.

Русский

Точность сохраняется отображением адического завершения: если f,g точны и f инъективен, то map I f, map I g образуют точную последовательность.

LaTeX

$$$\text{Exact} (\mathrm{map}\ I\ f) (\mathrm{map}\ I\ g)$$$

Lean4

/-- Equality of linear maps out of an adic completion can be checked on Cauchy sequences. -/
@[ext]
theorem map_ext'' {f g : AdicCompletion I M →ₗ[R] N}
    (h : f.comp (AdicCompletion.mk I M) = g.comp (AdicCompletion.mk I M)) : f = g :=
  by
  ext x
  apply induction_on I M x (fun a ↦ LinearMap.ext_iff.mp h a)

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