English
For a finite index, the union over i of the ranges of ((Pi.evalRingHom R i).comp f).specComap equals the range of f.specComap.
Русский
Для конечного индекса объединение по i диапазонов ((Pi.evalRingHom R i).comp f).specComap совпадает с диапазоном f.specComap.
LaTeX
$$$\\bigcup_i \\operatorname{range}((\\Pi.evalRingHom R i).\\operatorname{comp} f).\\operatorname{specComap} = \\operatorname{range} f.{\\rm specComap}$$$
Lean4
theorem iUnion_range_specComap_comp_evalRingHom {ι : Type*} {R : ι → Type*} [∀ i, CommRing (R i)] [Finite ι] {S : Type*}
[CommRing S] (f : S →+* Π i, R i) :
⋃ i, Set.range ((Pi.evalRingHom R i).comp f).specComap = Set.range f.specComap :=
by
simp_rw [specComap_comp]
apply subset_antisymm
· exact Set.iUnion_subset fun _ ↦ Set.range_comp_subset_range _ _
· rintro _ ⟨p, rfl⟩
obtain ⟨i, p, rfl⟩ := exists_comap_evalRingHom_eq p
exact Set.mem_iUnion_of_mem i ⟨p, rfl⟩
