equivTensorProduct_symm_apply_tmul_one

English

There is a canonical linear equivalence between LocalizedModule.equivTensorProduct S M and the appropriate tensor product modules, with the symmetry expressed by the inverse map.

Русский

Существует каноническое линейное эквивалентное отображение между LocalizedModule.equivTensorProduct S M и соответствующими модулями тензорного произведения, с симметрией через обратное отображение.

LaTeX

$$$(\text{equivTensorProduct } S M) : \text{LocalizedModule } S M \cong_\text{lin} (Localization S) \otimes_R M$$$

Lean4

@[simp]
theorem equivTensorProduct_symm_apply_tmul_one (x : M) : (equivTensorProduct S M).symm (1 ⊗ₜ[R] x) = mk x 1 := by
  simp [← Localization.mk_one]

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