English
There is an R-linear isomorphism basisAux that identifies A ⊗R M with the finitely supported functions from an index set to A, provided an R-basis of M.
Русский
Существует изоморфизм по базису, который идентифицирует A ⊗R M с пространством конечной поддержки функций из множества индексов в A, если дан базис M над R.
LaTeX
$$$\text{basisAux}: A ⊗R M \cong ι \to_0 A$$$
Lean4
/-- Given an `R`-algebra `A` and an `R`-basis of `M`, this is an `R`-linear isomorphism
`A ⊗[R] M ≃ (ι →₀ A)` (which is in fact `A`-linear). -/
noncomputable def basisAux : A ⊗[R] M ≃ₗ[R] ι →₀ A :=
_root_.TensorProduct.congr (Finsupp.LinearEquiv.finsuppUnique R A PUnit.{uι + 1}).symm b.repr ≪≫ₗ
(finsuppTensorFinsupp R R A R PUnit ι).trans
(Finsupp.lcongr (Equiv.uniqueProd ι PUnit) (_root_.TensorProduct.rid R A))
