English
Let f: M → N and g: N → P be linear maps between modules over a commutative semiring R, with the sequence M --f--> N --g--> P exact (i.e., im f = ker g). For every R-module Q, tensoring on the left by Q (f ⊗ Q, g ⊗ Q) has the same exactness property as tensoring on the right by Q (f ⊗_R Q, g ⊗_R Q): the pair (f.rTensor Q, g.rTensor Q) is exact if and only if the pair (f.lTensor Q, g.lTensor Q) is exact.
Русский
Пусть R – кольцо, M, N, P – R-модули и f: M → N, g: N → P – линейные отображения, образ которых образует точную последовательность M → N → P (то есть im f = ker g). Для любого R-модуля Q пары отображений f и g допускают тензорирование слева и справа таким образом, что точность сохраняется: точность последовательности после правого тензорирования равна точности после левого тензорирования.
LaTeX
$$$\\operatorname{Exact}(f \\otimes_R Q,\\ g \\otimes_R Q) \\;\\iff\\; \\operatorname{Exact}(Q \\otimes_R f,\\ Q \\otimes_R g)$$$
Lean4
theorem rTensor_exact_iff_lTensor_exact :
Function.Exact (f.rTensor Q) (g.rTensor Q) ↔ Function.Exact (f.lTensor Q) (g.lTensor Q) :=
Function.Exact.iff_of_ladder_linearEquiv (e₁ := TensorProduct.comm _ _ _) (e₂ := TensorProduct.comm _ _ _) (e₃ :=
TensorProduct.comm _ _ _) (by ext; simp) (by ext; simp)
