English
Let f be a family of elements of a commutative ring R indexed by ι. The smallest open set (in the Zariski topology of PrimeSpectrum(R)) containing all basic opens defined by these elements equals the whole space if and only if the ideal generated by all the f(i) (i in ι) is the unit ideal.
Русский
Пусть {f i}_{i∈ι} — семейство элементов кольца R. Наименьшая открытая подпространство спектра PrimeSpectrum(R), содержащая все базовые открытые D(f i), равна всему спектру тогда и только когда порождающее множество {f(i) : i∈ι} образует единичный идеал в R.
LaTeX
$$$$ \bigvee_{i \in \iota} \mathrm{basicOpen}(f(i)) = \top \quad\Longleftrightarrow\quad \operatorname{span}(\operatorname{range} f) = \top. $$$$
Lean4
theorem iSup_basicOpen_eq_top_iff {ι : Type*} {f : ι → R} :
(⨆ i : ι, PrimeSpectrum.basicOpen (f i)) = ⊤ ↔ Ideal.span (Set.range f) = ⊤ :=
by
rw [SetLike.ext'_iff, Opens.coe_iSup]
simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Opens.coe_top, ← Set.compl_iInter,
← PrimeSpectrum.zeroLocus_iUnion]
rw [← PrimeSpectrum.zeroLocus_empty_iff_eq_top, compl_involutive.eq_iff]
simp only [Set.iUnion_singleton_eq_range, Set.compl_univ, PrimeSpectrum.zeroLocus_span]
