English
Let R and S be commutative semirings. The primes of R×S that come from primes of R via the first projection fst are exactly the primes containing the kernel of fst; equivalently, they are the primes of the form p × S with p ∈ Spec(R).
Русский
Пусть R и S - коммутативные полукольца. Непрерывные идеалыprime-спектра R×S, получаемые из простых идеалов R через первую проекцию fst, совпадают с множествами prime-идеалов, содержащих ядро fst; эквивалентно, это именно такие идеалы вида p × S, где p ∈ Spec(R).
LaTeX
$$$$\\mathrm{range}(\\mathrm{comap}(\\mathrm{fst}_{R,S})) = \\mathrm{zeroLocus}(\\ker(\\mathrm{fst}_{R,S})).$$$$
Lean4
theorem range_comap_fst : Set.range (comap (RingHom.fst R S)) = zeroLocus (RingHom.ker (RingHom.fst R S)) :=
by
refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩
· rintro ⟨I, hI, rfl⟩; exact Ideal.comap_mono bot_le
obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
· exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩
· refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
simpa [eq] using h (show (0, 1) ∈ RingHom.ker (RingHom.fst R S) by simp)
