English
For a surjective f, the minimal primes of I.map f correspond to the image of minimizes primes, with a technical adjustment using the kernel.
Русский
При сюръективном отображении минимальные-primes образа соответствуют изображению минимальных-primes, с учётом ядра.
LaTeX
$$$(J.map f).minimalPrimes = Ideal.map f '' (J \lor \ker f).minimalPrimes$$$
Lean4
theorem minimalPrimes_map_of_surjective {S : Type*} [CommRing S] {f : R →+* S} (hf : Function.Surjective f)
(I : Ideal R) : (I.map f).minimalPrimes = Ideal.map f '' (I ⊔ (RingHom.ker f)).minimalPrimes :=
by
apply Set.image_injective.mpr (Ideal.comap_injective_of_surjective f hf)
rw [← Ideal.comap_minimalPrimes_eq_of_surjective hf, ← Set.image_comp, Ideal.comap_map_of_surjective f hf,
Set.image_congr, Set.image_id, RingHom.ker]
intro x hx
exact (Ideal.comap_map_of_surjective f hf _).trans (sup_eq_left.mpr <| le_sup_right.trans hx.1.2)
