English
For a family of rings R i, the map that selects the i-th component from the product preserves membership via a projection: map (Pi.evalRingHom R i) (Ideal.pi I) equals I i.
Русский
Для семейства колец R_i отображение выбора i-й компоненты сохраняет членство: map (Pi.evalRingHom R i) (Ideal.pi I) = I i.
LaTeX
$$$I : \Pi i, \mathrm{Ideal}(R i)\; (i : \iota) \Rightarrow (\mathrm{Ideal.map} (\Pi.evalRingHom R i) (\mathrm{Ideal.pi} I)) = I i$$$
Lean4
theorem map_evalRingHom_pi {I : Π i, Ideal (R i)} (i : ι) : (pi I).map (Pi.evalRingHom R i) = I i :=
by
ext r
rw [mem_map_iff_of_surjective (Pi.evalRingHom R i) (Function.surjective_eval _)]
classical refine ⟨?_, fun hr ↦ ⟨_, single_mem_pi hr, by simp⟩⟩
rintro ⟨r, hr, rfl⟩
exact hr i
