English
If M is invertible, the functor - ⊗_R M is an auto-equivalence of the category of R-modules.
Русский
Если M обратим, то функция - ⊗_R M является автоэквивалентой категории R-модулей.
LaTeX
$$$ (P \\to Q) \\mapsto (P \\otimes_R M \\to Q \\otimes_R M) $ is an equivalence$$
Lean4
/-- If there is an `R`-isomorphism between `M ⊗[R] N` and `R`,
the induced map `M → Nᵛ` is an isomorphism. -/
theorem bijective_curry : Function.Bijective (curry e.toLinearMap) :=
by
have :
curry e.toLinearMap =
((TensorProduct.lid R N).congrLeft _ R ≪≫ₗ e.congrRight) ∘ₗ
rTensorHom N ∘ₗ (ringLmapEquivSelf R R M).symm.toLinearMap :=
by
rw [← LinearEquiv.toLinearMap_symm_comp_eq]; ext
simp [LinearEquiv.congrLeft, LinearEquiv.congrRight, LinearEquiv.arrowCongrAddEquiv]
simpa [this] using (rTensorEquiv R M <| TensorProduct.comm R N M ≪≫ₗ e).bijective
