Commit 2024-06-26 11:25 a1cb4f2c

feat(LinearAlgebra/TensorProduct/Submodule): add some linear maps induced by multiplication for submodules (#12498) ... used in the definition of linearly disjointness. Let R be a commutative ring, S be an R-algebra (not necessarily commutative). Let M and N be R-submodules in S.

• Submodule.mulMap: the natural R-linear map M ⊗[R] N →ₗ[R] S induced by the multiplication in S, whose image is M * N (Submodule.mulMap_range).
• Submodule.mulMap': the natural map M ⊗[R] N →ₗ[R] M * N induced by multiplication in S, which is surjective (Submodule.mulMap'_surjective).
• Submodule.lTensorOne, Submodule.rTensorOne: the natural isomorphism between i(R) ⊗[R] N and N, resp. M ⊗[R] i(R) and M, induced by multiplication in S, here i : R → S is the structure map. They generalize TensorProduct.lid and TensorProduct.rid, as i(R) is not necessarily isomorphic to R. Note that we use ⊥ : Subalgebra R S instead of 1 : Submodule R S, since the map R →ₗ[R] (1 : Submodule R S) is not defined directly in mathlib yet.
• Submodule.mulLeftMap: if m : ι → M is a family of elements, then there is an R-linear map from ι →₀ N to S which maps { n_i } to the sum of m_i * n_i.
• Submodule.mulRightMap: if n : ι → N is a family of elements, then there is an R-linear map from ι →₀ M to S which maps { m_i } to the sum of m_i * n_i.