range_comap_snd — Mathlib

English

Let R,S be commutative semirings. The primes of R×S that come from primes of S via the second projection snd are exactly the primes containing the kernel of snd; equivalently, they are the primes of the form R × q with q ∈ Spec(S).

Русский

Пусть R и S — коммутативные полукольца. Примитивные идеалы R×S, получаемые из простых идеалов S через вторую проекцию snd, равны тем примитивным идеалам, которые содержат ядро snd; эквивалентно, это такие идеалы вида R × q, где q ∈ Spec(S).

LaTeX

$$$$\\mathrm{range}(\\mathrm{comap}(\\mathrm{snd}_{R,S})) = \\mathrm{zeroLocus}(\\ker(\\mathrm{snd}_{R,S})).$$$$

Lean4

theorem range_comap_snd : Set.range (comap (RingHom.snd R S)) = zeroLocus (RingHom.ker (RingHom.snd 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
  · refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
    simpa [eq] using h (show (1, 0) ∈ RingHom.ker (RingHom.snd R S) by simp)
  · exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩

Похожие утверждения