English
Every ideal I of R × S is the product of the images of I under the two projection maps, i.e., I = map fst(I) × map snd(I).
Русский
Каждый идеал I в R × S является произведением образов I при двух проекциях; то есть I = map fst(I) × map snd(I).
LaTeX
$$$I = (\\operatorname{map} (\\text{fst}) I) \\mathrm{prod} (\\operatorname{map} (\\text{snd}) I)$$$
Lean4
/-- Every ideal of the product ring is of the form `I × J`, where `I` and `J` can be explicitly
given as the image under the projection maps. -/
theorem ideal_prod_eq (I : Ideal (R × S)) :
I = Ideal.prod (map (RingHom.fst R S) I : Ideal R) (map (RingHom.snd R S) I) :=
by
apply Ideal.ext
rintro ⟨r, s⟩
rw [mem_prod, mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective,
mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
refine ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, ?_⟩
rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩
simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)
