rTensorEquiv — Mathlib

English

If there exists an R-isomorphism M ⊗ N ≃ R, the curry map M → N^∨ is bijective.

Русский

Если существует изоморфизм M ⊗ N ≃ R, то карри-функция M → N^∨ является биективной.

LaTeX

$$If M ⊗_R N ≃_R R then M ≃_R N^∨$$

Lean4

/-- If `M` is an invertible `R`-module, `(· ⊗[R] M)` is an auto-equivalence of the category
of `R`-modules. -/
@[simps!]
noncomputable def rTensorEquiv : (P →ₗ[R] Q) ≃ₗ[R] (P ⊗[R] M →ₗ[R] Q ⊗[R] M)
    where
  __ := LinearMap.rTensorHom M
  invFun := rTensorInv P Q e
  left_inv := rTensorInv_leftInverse P Q e
  right_inv _ := rTensorInv_injective P Q e (by rw [LinearMap.toFun_eq_coe, rTensorInv_leftInverse])

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