Interaction between Quotients and Tensor Products

This file contains constructions that relate quotients and tensor products. Let M, N be R-modules, m ≤ M and n ≤ N be an R-submodules and I ≤ R an ideal. We prove the following isomorphisms:

Main results

• TensorProduct.quotientTensorQuotientEquiv: (M ⧸ m) ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N ⊔ M ⊗ n)
• TensorProduct.quotientTensorEquiv: (M ⧸ m) ⊗[R] N ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N)
• TensorProduct.tensorQuotientEquiv: M ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (M ⊗ n)
• TensorProduct.quotTensorEquivQuotSMul: (R ⧸ I) ⊗[R] M ≃ₗ[R] M ⧸ (I • M)
• TensorProduct.tensorQuotEquivQuotSMul: M ⊗[R] (R ⧸ I) ≃ₗ[R] M ⧸ (I • M)

Tags

Quotient, Tensor Product

noncomputable def TensorProduct.quotientTensorQuotientEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (n : Submodule R N) : TensorProduct R (M ⧸ m) (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)

Let M, N be R-modules, m ≤ M and n ≤ N be an R-submodules. Then we have a linear isomorphism between tensor products of the quotients and the quotient of the tensor product: (M ⧸ m) ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N ⊔ M ⊗ n).

@[simp]

theorem TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (n : Submodule R N) (x : M) (y : N) : (quotientTensorQuotientEquiv m n) (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)

@[simp]

theorem TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (n : Submodule R N) (x : M) (y : N) : (quotientTensorQuotientEquiv m n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y

noncomputable def TensorProduct.quotientTensorEquiv {R : Type u_1} {M : Type u_2} (N : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) : TensorProduct R (M ⧸ m) N ≃ₗ[R] TensorProduct R M N ⧸ LinearMap.range (map m.subtype LinearMap.id)

Let M, N be R-modules, m ≤ M be an R-submodule. Then we have a linear isomorphism between tensor products of the quotient and the quotient of the tensor product: (M ⧸ m) ⊗[R] N ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N).

@[simp]

theorem TensorProduct.quotientTensorEquiv_apply_tmul_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (x : M) (y : N) : (quotientTensorEquiv N m) (Submodule.Quotient.mk x ⊗ₜ[R] y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)

@[simp]

theorem TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (x : M) (y : N) : (quotientTensorEquiv N m).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] y

noncomputable def TensorProduct.tensorQuotientEquiv {R : Type u_1} (M : Type u_2) {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) : TensorProduct R M (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ LinearMap.range (map LinearMap.id n.subtype)

Let M, N be R-modules, n ≤ N be an R-submodule. Then we have a linear isomorphism between tensor products of the quotient and the quotient of the tensor product: M ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (M ⊗ n).

@[simp]

theorem TensorProduct.tensorQuotientEquiv_apply_mk_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) (x : M) (y : N) : (tensorQuotientEquiv M n) (x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)

@[simp]

theorem TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) (x : M) (y : N) : (tensorQuotientEquiv M n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = x ⊗ₜ[R] Submodule.Quotient.mk y

noncomputable def TensorProduct.quotTensorEquivQuotSMul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : TensorProduct R (R ⧸ I) M ≃ₗ[R] M ⧸ I • ⊤

Left tensoring a module with a quotient of the ring is the same as quotienting that module by the corresponding submodule.

noncomputable def TensorProduct.tensorQuotEquivQuotSMul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : TensorProduct R M (R ⧸ I) ≃ₗ[R] M ⧸ I • ⊤

Right tensoring a module with a quotient of the ring is the same as quotienting that module by the corresponding submodule.

@[simp]

theorem TensorProduct.quotTensorEquivQuotSMul_mk_tmul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (r : R) (x : M) : (quotTensorEquivQuotSMul M I) ((Ideal.Quotient.mk I) r ⊗ₜ[R] x) = Submodule.Quotient.mk (r • x)

theorem TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ↑(quotTensorEquivQuotSMul M I) ∘ₗ LinearMap.rTensor M (Submodule.mkQ I) = (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.lid R M)

@[simp]

theorem TensorProduct.quotTensorEquivQuotSMul_symm_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) : (quotTensorEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = 1 ⊗ₜ[R] x

theorem TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ↑(quotTensorEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (mk R (R ⧸ I) M) 1

theorem TensorProduct.quotTensorEquivQuotSMul_comp_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ↑(quotTensorEquivQuotSMul M I) ∘ₗ (mk R (R ⧸ I) M) 1 = (I • ⊤).mkQ

@[simp]

theorem TensorProduct.tensorQuotEquivQuotSMul_tmul_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) (r : R) : (tensorQuotEquivQuotSMul M I) (x ⊗ₜ[R] (Ideal.Quotient.mk I) r) = Submodule.Quotient.mk (r • x)

theorem TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ↑(tensorQuotEquivQuotSMul M I) ∘ₗ LinearMap.lTensor M (Submodule.mkQ I) = (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.rid R M)

@[simp]

theorem TensorProduct.tensorQuotEquivQuotSMul_symm_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) : (tensorQuotEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = x ⊗ₜ[R] 1

theorem TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ↑(tensorQuotEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (mk R M (R ⧸ I)).flip 1

theorem TensorProduct.tensorQuotEquivQuotSMul_comp_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) : ↑(tensorQuotEquivQuotSMul M I) ∘ₗ (mk R M (R ⧸ I)).flip 1 = (I • ⊤).mkQ

noncomputable def Ideal.qoutMapEquivTensorQout {R : Type u_1} [CommRing R] (S : Type u_4) [CommRing S] [Algebra R S] {I : Ideal R} : (S ⧸ map (algebraMap R S) I) ≃ₗ[S] TensorProduct R S (R ⧸ I)

Let R be a commutative ring, S be an R-algebra, I is be ideal of R, then S ⧸ IS is isomorphic to S ⊗[R] (R ⧸ I) as S modules.

noncomputable def TensorProduct.tensorQuotMapSMulEquivTensorQuot {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_4) [CommRing S] [Algebra R S] (I : Ideal R) : (TensorProduct R S M ⧸ Ideal.map (algebraMap R S) I • ⊤) ≃ₗ[S] TensorProduct R S (M ⧸ I • ⊤)

Let R be a commutative ring, S be an R-algebra, I is be ideal of R, then S ⊗[R] M ⧸ I(S ⊗[R] M) is isomorphic to S ⊗[R] (M ⧸ IM) as S modules.