English
Let I be an ideal in a commutative ring R, and let M,N be R-modules with a linear map f: M → N. The canonical construction AdicCompletion I induces a functorial way to tensor with M and N, and the natural map obtained by composing the completion map with f agrees with first mapping M to N via f and then applying the completion.
Русский
Пусть I — идеал кольца R, M и N — R-модули, а f: M → N — линейное отображение. Каноническое построение AdicCompletion I даёт каноническое отображение, связующее умножение на M и N; естественная карта, полученная путём композиции отображений завершения и f, совпадает с сначала отображением через f и затем завершением.
LaTeX
$$$ (\mathrm{map}\ I\ f) \circ (\mathrm{ofTensorProduct}\ I\ M) = (\mathrm{ofTensorProduct}\ I\ N) \circ \big( \mathrm{AlgebraTensorModule.map}(\mathrm{id}_R, f) \big) $$$
Lean4
/-- `ofTensorProduct` is functorial in `M`. -/
theorem ofTensorProduct_naturality (f : M →ₗ[R] N) :
map I f ∘ₗ ofTensorProduct I M = ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f :=
by
ext
simp
