English
If b and c are bases of M and N, then the map i ↦ b(i1) ⊗ c(i2) defines a basis of the tensor product M ⊗_R N over S.
Русский
Пусть b и c — базы модулей M и N; отображение i ↦ b(i1) ⊗ c(i2) задаёт базис тензорного произведения M ⊗_R N над S.
LaTeX
$$$\text{If } b: \Basis_{ι} S M \text{ and } c: \Basis_{κ} R N, \text{ then } (i,j) \mapsto b_i \otimes c_j \text{ is a basis of } M \otimes_R N$$$
Lean4
/-- If `b : ι → M` and `c : κ → N` are bases then so is `fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N`. -/
def tensorProduct (b : Basis ι S M) (c : Basis κ R N) : Basis (ι × κ) S (M ⊗[R] N) :=
Finsupp.basisSingleOne.map
((TensorProduct.AlgebraTensorModule.congr b.repr c.repr).trans <|
(finsuppTensorFinsupp R S _ _ _ _).trans <|
Finsupp.lcongr (Equiv.refl _) (TensorProduct.AlgebraTensorModule.rid R S S)).symm
