English
There is a canonical linear equivalence I ⊗_R J ≃ₗ[R] I * J between invertible submodules I,J.
Русский
Существует каноническое линейное эквивалентное отображение I ⊗_R J ≃ₗ[R] I * J между инвертируемыми подмодулями I и J.
LaTeX
$$$ \\forall (I J : \\mathrm{Units}( \\mathrm{Submodule} R A )),\\; I \\otimes_R J \\simeq_R I * J. $$$
Lean4
/-- Given two invertible `R`-submodules in an `R`-algebra `A`, the `R`-linear map from
`I ⊗[R] J` to `I * J` induced by multiplication is an isomorphism. -/
noncomputable def tensorEquivMul : I ⊗[R] J ≃ₗ[R] I * J :=
.ofBijective (mulMap' ..)
⟨by
have := IsLocalization.flat A S
simpa [mulMap', mulMap_eq_mul'_comp_mapIncl] using
(IsLocalization.bijective_linearMap_mul' S A).1.comp (Flat.tensorProduct_mapIncl_injective_of_left ..),
mulMap'_surjective _ _⟩
