English
Let U be an open subset in a spectrum built from a product of rings; if V is a compact subset containing the opens-range of sigmaSpec, and V is contained in U, then U is the whole space.
Русский
Пусть U — открытое подмножество спектра, построенного как произведение колец; если V — компактное подмножество, содержащее открытое множество sigmaSpec, и V ⊆ U, то U=полное пространство.
LaTeX
$$$U=\top$ given: V \subseteq U, IsCompact(V) and V \supseteq opensRange(sigmaSpec).$$$
Lean4
theorem eq_top_of_sigmaSpec_subset_of_isCompact (U : (Spec <| .of <| Π i, R i).Opens)
(V : Set (Spec <| .of <| Π i, R i)) (hV : ↑(sigmaSpec R).opensRange ⊆ V)
(hV' : IsCompact (X := Spec (.of <| Π i, R i)) V) (hVU : V ⊆ U) : U = ⊤ :=
by
obtain ⟨s, hs⟩ := (PrimeSpectrum.isOpen_iff _).mp U.2
obtain ⟨t, hts, ht, ht'⟩ : ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).1 :=
by
obtain ⟨t, ht⟩ :=
hV'.elim_finite_subcover (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
(by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])
exact ⟨t.map (Function.Embedding.subtype _), by simp, Finset.finite_toSet _, by simpa using ht⟩
replace ht' : V ⊆ (zeroLocus t)ᶜ := by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ t))] using ht'
have (i : _) : Ideal.span (Pi.evalRingHom (R ·) i '' t) = ⊤ :=
by
rw [← zeroLocus_empty_iff_eq_top, zeroLocus_span, ← preimage_comap_zeroLocus, ← Set.compl_univ_iff, ←
Set.preimage_compl, Set.preimage_eq_univ_iff]
trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1
· simp; rfl
· rw [Scheme.Hom.opensRange_comp]
exact (Set.image_subset_range _ _).trans (hV.trans ht')
have : Ideal.span s = ⊤ :=
top_le_iff.mp ((Ideal.span_eq_top_of_span_image_evalRingHom _ ht this).ge.trans (Ideal.span_mono hts))
simpa [← zeroLocus_span s, zeroLocus_empty_iff_eq_top.mpr this] using hs
