ofTensorProduct_bijective_of_finite_of_isNoetherian

English

If R is Noetherian and M is finite, then the canonical completion map is bijective.

Русский

Если R Нётерово и M конечна, то каноническое отображение завершения биективно.

LaTeX

$$$\mathrm{ofTensorProduct}_I M\ \text{ is bijective for finite } M$$$

Lean4

/-- If `R` is a Noetherian ring and `M` is a finite `R`-module, then the natural map
given by `AdicCompletion.ofTensorProduct` is an isomorphism. -/
theorem ofTensorProduct_bijective_of_finite_of_isNoetherian [Module.Finite R M] :
    Function.Bijective (ofTensorProduct I M) :=
  by
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  exact ofTensorProduct_bijective_of_map_from_fin I M f hf

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