English
In a localization, minimal primes behave compatibly with comap, giving equality with preimage under the localization map.
Русский
При локализации минимальные-primes ведут себя совместно с comap, давая равенство с прообразом локализационной карты.
LaTeX
$$$[IsLocalization S A] (J) : (J.map (algebraMap R A)).minimalPrimes = Ideal.comap (algebraMap R A) \u2032' J.minimalPrimes$$$
Lean4
theorem minimalPrimes_map [IsLocalization S A] (J : Ideal R) :
(J.map (algebraMap R A)).minimalPrimes = Ideal.comap (algebraMap R A) ⁻¹' J.minimalPrimes :=
by
ext p
constructor
· intro hp
haveI := hp.1.1
refine ⟨⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hp.1.2⟩, ?_⟩
rintro I hI e
have hI' : Disjoint (S : Set R) I :=
Set.disjoint_of_subset_right e ((IsLocalization.isPrime_iff_isPrime_disjoint S A _).mp hp.1.1).2
refine (Ideal.comap_mono <| hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_
· exact IsLocalization.isPrime_of_isPrime_disjoint S A I hI.1 hI'
· exact IsLocalization.comap_map_of_isPrime_disjoint S A _ hI.1 hI'
· intro hp
refine ⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.1.2⟩, ?_⟩
· rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_comap_iff S]
refine ⟨hp.1.1, ?_⟩
rintro rfl
exact hp.1.1.ne_top rfl
· intro I hI e
rw [← IsLocalization.map_comap S A I, ← IsLocalization.map_comap S A p]
haveI := hI.1
exact Ideal.map_mono (hp.2 ⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hI.2⟩ (Ideal.comap_mono e))
