English
If R is Noetherian and M is a finite R-module, the canonical map AdicCompletion I M is bijective with the finite-noetherian tensor construction; i.e., the natural map of tensor is an isomorphism.
Русский
Если R — Нётерово кольцо и M — конечная R-модуля, то естественное отображение через тензорное произведение даёт изоморфность.
LaTeX
$$$\mathrm{ofTensorProduct}_I M : \mathrm{AdicCompletion}_I(R) \otimes_R M \to \mathrm{AdicCompletion}_I M\quad\text{is bijective}$$$
Lean4
/-- If `M` is a finite `R`-module, then the canonical map
`AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
theorem ofTensorProduct_surjective_of_finite [Module.Finite R M] : Function.Surjective (ofTensorProduct I M) :=
by
obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M
let f := ofTensorProduct I M ∘ₗ p.baseChange (AdicCompletion I R)
let g := map I p ∘ₗ ofTensorProduct I (Fin n → R)
have hfg : f = g := by
ext
simp [f, g]
have hf : Function.Surjective f := by
simp only [hfg, LinearMap.coe_comp, g]
apply Function.Surjective.comp
· exact AdicCompletion.map_surjective I hp
· exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective
exact Function.Surjective.of_comp hf
