Some results on tensor product of submodules

Linear maps induced by multiplication for submodules

Let R be a commutative ring, S be an R-algebra (not necessarily commutative). Let M and N be R-submodules in S (Submodule R S). We define some linear maps induced by the multiplication in S (see also LinearMap.mul'), which are mainly used in the definition of linearly disjointness (Submodule.LinearDisjoint).

• 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.

There are also Submodule.mulLeftMap and Submodule.mulRightMap, defined in earlier files.

def Submodule.mulMap {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : TensorProduct R ↥M ↥N →ₗ[R] S

If M and N are submodules in an algebra S over R, there is the natural map M ⊗[R] N →ₗ[R] S induced by multiplication in S.

Equations

• M.mulMap N = TensorProduct.lift ((LinearMap.mul R S).domRestrict₁₂ M N)

@[simp]

theorem Submodule.mulMap_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (m : ↥M) (n : ↥N) : (M.mulMap N) (m ⊗ₜ[R] n) = ↑m * ↑n

theorem Submodule.mulMap_op {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : (Submodule.equivOpposite.symm (MulOpposite.op M)).mulMap (Submodule.equivOpposite.symm (MulOpposite.op N)) = ↑(MulOpposite.opLinearEquiv R) ∘ₗ N.mulMap M ∘ₗ ↑(TensorProduct.congr ((MulOpposite.opLinearEquiv R).symm.ofSubmodule' M) ((MulOpposite.opLinearEquiv R).symm.ofSubmodule' N) ≪≫ₗ TensorProduct.comm R ↥M ↥N)

theorem Submodule.mulMap_comm_of_commute {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) (hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n) : N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)

theorem Submodule.mulMap_comp_rTensor {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (N : Submodule R S) {M' : Submodule R S} (hM : M' ≤ M) : M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (Submodule.inclusion hM) = M'.mulMap N

theorem Submodule.mulMap_comp_lTensor {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) {N : Submodule R S} {N' : Submodule R S} (hN : N' ≤ N) : M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (Submodule.inclusion hN) = M.mulMap N'

theorem Submodule.mulMap_comp_map_inclusion {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} {M' : Submodule R S} {N' : Submodule R S} (hM : M' ≤ M) (hN : N' ≤ N) : M.mulMap N ∘ₗ TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN) = M'.mulMap N'

theorem Submodule.mulMap_eq_mul'_comp_mapIncl {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : M.mulMap N = LinearMap.mul' R S ∘ₗ TensorProduct.mapIncl M N

theorem Submodule.mulMap_range {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : LinearMap.range (M.mulMap N) = M * N

def Submodule.mulMap' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : TensorProduct R ↥M ↥N →ₗ[R] ↥(M * N)

If M and N are submodules in an algebra S over R, there is the natural map M ⊗[R] N →ₗ[R] M * N induced by multiplication in S, which is surjective (Submodule.mulMap'_surjective).

Equations

• M.mulMap' N = ↑(LinearEquiv.ofEq (LinearMap.range (M.mulMap N)) (M * N) ⋯) ∘ₗ (M.mulMap N).rangeRestrict

@[simp]

theorem Submodule.val_mulMap'_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} {N : Submodule R S} (m : ↥M) (n : ↥N) : ↑((M.mulMap' N) (m ⊗ₜ[R] n)) = ↑m * ↑n

theorem Submodule.mulMap'_surjective {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : Function.Surjective ⇑(M.mulMap' N)

def Submodule.lTensorOne' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (N : Submodule R S) : TensorProduct R ↥⊥ ↥N →ₗ[R] ↥N

If N is a submodule in an algebra S over R, there is the natural map i(R) ⊗[R] N →ₗ[R] N induced by multiplication in S, here i : R → S is the structure map. This is promoted to an isomorphism as Submodule.lTensorOne. Use that instead.

Equations

• N.lTensorOne' = let_fun this := ↑(LinearEquiv.ofEq (LinearMap.range (Submodule.mulMap 1 N)) N ⋯) ∘ₗ (Submodule.mulMap 1 N).rangeRestrict; this

@[simp]

theorem Submodule.lTensorOne'_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {N : Submodule R S} (y : R) (n : ↥N) : N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • n

@[simp]

theorem Submodule.lTensorOne'_one_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {N : Submodule R S} (n : ↥N) : N.lTensorOne' (1 ⊗ₜ[R] n) = n

def Submodule.lTensorOne {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (N : Submodule R S) : TensorProduct R ↥⊥ ↥N ≃ₗ[R] ↥N

If N is a submodule in an algebra S over R, there is the natural isomorphism between i(R) ⊗[R] N and N induced by multiplication in S, here i : R → S is the structure map. This generalizes TensorProduct.lid as i(R) is not necessarily isomorphic to R.

Equations

• N.lTensorOne = LinearEquiv.ofLinear N.lTensorOne' ((TensorProduct.mk R ↥⊥ ↥N) 1) ⋯ ⋯

@[simp]

theorem Submodule.lTensorOne_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {N : Submodule R S} (y : R) (n : ↥N) : N.lTensorOne ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • n

@[simp]

theorem Submodule.lTensorOne_one_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {N : Submodule R S} (n : ↥N) : N.lTensorOne (1 ⊗ₜ[R] n) = n

@[simp]

theorem Submodule.lTensorOne_symm_apply {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {N : Submodule R S} (n : ↥N) : N.lTensorOne.symm n = 1 ⊗ₜ[R] n

theorem Submodule.mulMap_one_left_eq {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (N : Submodule R S) : Submodule.mulMap 1 N = N.subtype ∘ₗ ↑N.lTensorOne

def Submodule.rTensorOne' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) : TensorProduct R ↥M ↥⊥ →ₗ[R] ↥M

If M is a submodule in an algebra S over R, there is the natural map M ⊗[R] i(R) →ₗ[R] M induced by multiplication in S, here i : R → S is the structure map. This is promoted to an isomorphism as Submodule.rTensorOne. Use that instead.

Equations

• M.rTensorOne' = let_fun this := ↑(LinearEquiv.ofEq (LinearMap.range (M.mulMap 1)) M ⋯) ∘ₗ (M.mulMap 1).rangeRestrict; this

@[simp]

theorem Submodule.rTensorOne'_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (y : R) (m : ↥M) : M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • m

@[simp]

theorem Submodule.rTensorOne'_tmul_one {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (m : ↥M) : M.rTensorOne' (m ⊗ₜ[R] 1) = m

def Submodule.rTensorOne {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) : TensorProduct R ↥M ↥⊥ ≃ₗ[R] ↥M

If M is a submodule in an algebra S over R, there is the natural isomorphism between M ⊗[R] i(R) and M induced by multiplication in S, here i : R → S is the structure map. This generalizes TensorProduct.rid as i(R) is not necessarily isomorphic to R.

Equations

• M.rTensorOne = LinearEquiv.ofLinear M.rTensorOne' (↑(TensorProduct.comm R ↥⊥ ↥M) ∘ₗ (TensorProduct.mk R ↥⊥ ↥M) 1) ⋯ ⋯

@[simp]

theorem Submodule.rTensorOne_tmul {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (y : R) (m : ↥M) : M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • m

@[simp]

theorem Submodule.rTensorOne_tmul_one {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (m : ↥M) : M.rTensorOne (m ⊗ₜ[R] 1) = m

@[simp]

theorem Submodule.rTensorOne_symm_apply {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (m : ↥M) : M.rTensorOne.symm m = m ⊗ₜ[R] 1

theorem Submodule.mulMap_one_right_eq {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) : M.mulMap 1 = M.subtype ∘ₗ ↑M.rTensorOne

@[simp]

theorem Submodule.comm_trans_lTensorOne {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) : TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne

@[simp]

theorem Submodule.comm_trans_rTensorOne {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) : TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne

theorem Submodule.mulLeftMap_eq_mulMap_comp {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_1} [DecidableEq ι] (m : ι → ↥M) : Submodule.mulLeftMap N m = M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (Finsupp.total ι (↥M) R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm

theorem Submodule.mulRightMap_eq_mulMap_comp {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M : Submodule R S) {N : Submodule R S} {ι : Type u_1} [DecidableEq ι] (n : ι → ↥N) : M.mulRightMap n = M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n) ∘ₗ ↑(TensorProduct.finsuppScalarRight R (↥M) ι).symm

theorem Submodule.mulMap_comm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submodule R S) (N : Submodule R S) : N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)