English
There is a canonical A-linear basis of A ⊗R M induced by an R-basis of M, described via the isomorphism basisAux; the basis and the isomorphism interact with tensoring and scalar multiplication in a natural way.
Русский
Существует канонический базис по алгебре над A для A ⊗R M, порожденный базисом по R в M, и этот изоморфизм согласован с тензорированием и умножением на скаляры.
LaTeX
$$$\text{basisAux}: A ⊗R M \cong ι \to_0 A \ ,\; (basis_A b).repr = basisAux_A b$$$
Lean4
instance base_change [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M]
[h : Module.Finite R M] : Module.Finite A (TensorProduct R A M) := by
classical
obtain ⟨s, hs⟩ := h.fg_top
refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
rintro x -
induction x with
| zero => exact zero_mem _
| tmul x
y =>
rw [Finset.coe_image, ← Submodule.span_span_of_tower R, Submodule.span_image, hs, Submodule.map_top,
LinearMap.coe_range, ← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul']
exact Submodule.smul_mem _ x (Submodule.subset_span <| Set.mem_range_self y)
| add x y hx hy => exact Submodule.add_mem _ hx hy
