English
For any ideal I of S, the closure of comap f applied to zeroLocus I equals zeroLocus of the comap of I; i.e., closure (comap f '' zeroLocus I) = zeroLocus (I.comap f).
Русский
Для любого идеала I в S замыкание образа comap f от zeroLocus I равно zeroLocus от I.comap f.
LaTeX
$$$$ \overline{\operatorname{comap} f '' \operatorname{zeroLocus} I} = \operatorname{zeroLocus}(I^{\comap f}). $$$$
Lean4
theorem closure_image_comap_zeroLocus (I : Ideal S) : closure (comap f '' zeroLocus I) = zeroLocus (I.comap f) :=
by
apply subset_antisymm
· rw [(isClosed_zeroLocus _).closure_subset_iff, Set.image_subset_iff, preimage_comap_zeroLocus]
exact zeroLocus_anti_mono (Set.image_preimage_subset _ _)
· rintro x (hx : I.comap f ≤ x.asIdeal)
obtain ⟨q, hq₁, hq₂⟩ := Ideal.exists_minimalPrimes_le hx
obtain ⟨p', hp', hp'', rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f _ hq₁
let p'' : PrimeSpectrum S := ⟨p', hp'⟩
apply
isClosed_closure.stableUnderSpecialization ((le_iff_specializes (comap f ⟨p', hp'⟩) x).mp hq₂)
(subset_closure (by exact ⟨_, hp'', rfl⟩))
