English
There exists a surjective map from R/(⋂ I_i) onto ∏ R/I_i when the I_i are pairwise coprime.
Русский
Существует сюръективный отображение из R/(⋂ I_i) в ∏ R/I_i при попарной взаимной простоте I_i.
LaTeX
$$$\text{quotientInfToPiQuotientSurj } I$$$
Lean4
theorem quotientInfToPiQuotient_surj {I : ι → Ideal R} (hI : Pairwise (IsCoprime on I)) :
Surjective (quotientInfToPiQuotient I) := by
classical
cases nonempty_fintype ι
intro g
choose f hf using fun i ↦ mk_surjective (g i)
have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 :=
by
intro i
have hI' : ∀ j ∈ ({ i } : Finset ι)ᶜ, IsCoprime (I i) (I j) :=
by
intro j hj
exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩
replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
refine ⟨e, ?_, ?_⟩
· simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
· exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
choose e he using key
use mk _ (∑ i, f i * e i)
ext i
rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]
· simp [(he i).1, hf]
· intro j hj
simp [(he j).2 i hj.symm]
