Module version of Chinese remainder theorem

theorem Ideal.pi_mkQ_rTensor {R : Type u_1} [CommRing R] {ι : Type u_2} (M : Type u_3) [AddCommGroup M] [Module R M] (I : ι → Ideal R) [Fintype ι] [DecidableEq ι] : LinearMap.rTensor M (LinearMap.pi fun (i : ι) => Submodule.mkQ (I i)) = ↑(TensorProduct.piLeft R M fun (i : ι) => R ⧸ I i).symm ∘ₗ (LinearMap.pi fun (i : ι) => (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M)

theorem Ideal.pi_tensorProductMk_quotient_surjective {R : Type u_1} [CommRing R] {ι : Type u_2} (M : Type u_3) [AddCommGroup M] [Module R M] (I : ι → Ideal R) (hI : Pairwise (Function.onFun IsCoprime I)) [Finite ι] : Function.Surjective ⇑(LinearMap.pi fun (i : ι) => (TensorProduct.mk R (R ⧸ I i) M) 1)

A form of Chinese remainder theorem for modules, part I: if ideals Iᵢ of R are pairwise coprime, then for any R-module M, the natural map M → Πᵢ (R ⧸ Iᵢ) ⊗[R] M is surjective.

theorem Ideal.ker_tensorProductMk_quotient {R : Type u_1} [CommRing R] {ι : Type u_2} (M : Type u_3) [AddCommGroup M] [Module R M] (I : ι → Ideal R) (hI : Pairwise (Function.onFun IsCoprime I)) [Finite ι] : LinearMap.ker (LinearMap.pi fun (i : ι) => (TensorProduct.mk R (R ⧸ I i) M) 1) = (⨅ (i : ι), I i) • ⊤

A form of Chinese remainder theorem for modules, part II: if ideals Iᵢ of R are pairwise coprime, then for any R-module M, the kernel of M → Πᵢ (R ⧸ Iᵢ) ⊗[R] M equals (⋂ᵢ Iᵢ) • M.