English
The image of a zero locus under specComap equals the zero locus of the comapped ideal; equivalently, f.specComap '' zeroLocus I = zeroLocus (I.comap f).
Русский
Образ нулевой локусы под specComap равен нулевой локусу расширенного идеала; то есть f.specComap '' zeroLocus I = zeroLocus (I.comap f).
LaTeX
$$$f.{\\rm specComap} '' zeroLocus I = zeroLocus(I.{\\rm comap} f)$$$
Lean4
theorem image_specComap_zeroLocus_eq_zeroLocus_comap (hf : Surjective f) (I : Ideal S) :
f.specComap '' zeroLocus I = zeroLocus (I.comap f) :=
by
simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]
refine fun p => ⟨?_, fun h_I_p => ?_⟩
· rintro ⟨p, hp, rfl⟩ a ha
exact hp ha
· have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p
refine ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => ?_, ?_⟩
· obtain ⟨x', rfl⟩ := hf x
exact Ideal.mem_map_of_mem f (h_I_p hx)
· ext x
rw [specComap_asIdeal, Ideal.mem_comap, Ideal.mem_map_iff_of_surjective f hf]
refine ⟨?_, fun hx => ⟨x, hx, rfl⟩⟩
rintro ⟨x', hx', heq⟩
rw [← sub_sub_cancel x' x]
refine p.asIdeal.sub_mem hx' (hp ?_)
rwa [mem_ker, map_sub, sub_eq_zero]
