English
Corollary of Pi quotient: the kernel of the Pi quotient map equals the infimum of the ideals.
Русский
Следствие для ядра квадриаты: кер соответствующего отображения равен полному пересечению идеалов.
LaTeX
$$$\ker(\Pi\text{-quotient}) = \bigcap_i I_i$$$
Lean4
/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then the canonical map `R → ∏ (R ⧸ Iᵢ)` is surjective. -/
theorem pi_quotient_surjective {I : ι → Ideal R} (hf : Pairwise fun i j ↦ IsCoprime (I i) (I j))
(x : (i : ι) → R ⧸ I i) : ∃ r : R, ∀ i, r = x i :=
by
obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y
exact
⟨r, fun i ↦ rfl⟩
-- variant of `IsDedekindDomain.exists_forall_sub_mem_ideal` which doesn't assume Dedekind domain!
