Tensor products of submodules as intersections

Let P ≤ M and Q ≤ N be submodules. Inside M ⊗[R] N the image of P ⊗[R] Q is always contained in both the image of M ⊗[R] Q and the image of P ⊗[R] N. Over a field the three images satisfy

P ⊗ Q = (M ⊗ Q) ∩ (P ⊗ N),

and the same holds over any commutative ring as soon as M ⧸ P is flat. This is the step that upgrades a submodule of a coalgebra whose comultiplication lands in both one-sided tensor products to a subcoalgebra.

Main results

• Submodule.range_map_subtype_subtype: the image of P ⊗[R] Q in M ⊗[R] N is the intersection of the images of M ⊗[R] Q and P ⊗[R] N, when M ⧸ P is flat.

References

• [N. Bourbaki, Algebra I, Chapters 1-3][bourbaki1989], Chapter II, §3, n°7, for the corresponding statement for vector spaces.

theorem Submodule.range_map_subtype_subtype {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) [Module.Flat R (M ⧸ P)] : (TensorProduct.map P.subtype Q.subtype).range = (LinearMap.lTensor M Q.subtype).range ⊓ (LinearMap.rTensor N P.subtype).range

If M ⧸ P is flat, the image of P ⊗[R] Q in M ⊗[R] N is the intersection of the images of M ⊗[R] Q and P ⊗[R] N. Over a field this holds for all submodules P and Q.