Theorems · Theorem · commutative algebra

Ideal.ker_tensorProductMk_quotient

∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (I : ι → Ideal R),
  Pairwise (Function.onFun IsCoprime I) →
    ∀ [Finite ι], (LinearMap.pi fun i => (TensorProduct.mk R (R ⧸ I i) M) 1).ker = (⨅ 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.

Defined in

Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Cited by

0 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleFinite