English
Let f: R →+* S be a ring hom between commutative semirings. The dense range of comap f is equivalent to the condition that every minimal prime I of R is the contraction of some prime of S; more precisely, for every I in the set of minimal primes of R, there exists p ∈ Spec(S) with comap f(p) = I.
Русский
Пусть f: R →+* S — гомоморфизм колец. Плотный образ comap f эквивалентен тому, что каждый минимальный приматовский идеал I в R является сокращением некоторого примитова в S; точнее, для каждого минимального пprime I R найдется p ∈ Spec(S) такое, что comap f(p) = I.
LaTeX
$$$$ \operatorname{DenseRange}(\operatorname{comap} f) \iff \forall I \in \operatorname{minimalPrimes}(R), \exists p \in \operatorname{Spec}(S), \operatorname{comap} f(p) = I. $$$$
Lean4
@[stacks 00FL]
theorem denseRange_comap_iff_minimalPrimes :
DenseRange (comap f) ↔ ∀ I (h : I ∈ minimalPrimes R), ⟨I, h.1.1⟩ ∈ Set.range (comap f) :=
by
constructor
· intro H I hI
have : I ∈ (RingHom.ker f).minimalPrimes :=
by
rw [denseRange_comap_iff_ker_le_nilRadical] at H
simp only [minimalPrimes, Ideal.minimalPrimes, Set.mem_setOf] at hI ⊢
convert hI using 2 with p
exact ⟨fun h ↦ ⟨h.1, bot_le⟩, fun h ↦ ⟨h.1, H.trans (h.1.radical_le_iff.mpr bot_le)⟩⟩
obtain ⟨p, hp, _, rfl⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f (I := ⊥) I this
exact ⟨⟨p, hp⟩, rfl⟩
· intro H p
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
exact ((le_iff_specializes ⟨q, hq.1.1⟩ p).mp hq').mem_closed isClosed_closure (subset_closure (H q hq))
