English
The family of basicOpen(𝒜 r) as r ranges over A forms a topological basis for the Zariski topology on ProjectiveSpectrum 𝒜.
Русский
family базовых открытых множеств basicOpen(𝒜 r) образуют топологическую базисную систему для Зари-топологии на ProjectiveSpectrum 𝒜.
LaTeX
$$$\text{IsTopologicalBasis}(\{ \mathrm{basicOpen}_{\mathcal{A}}(r) : r \in A \})$$$
Lean4
theorem isTopologicalBasis_basic_opens :
TopologicalSpace.IsTopologicalBasis (Set.range fun r : A => (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜))) :=
by
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
· rintro _ ⟨r, rfl⟩
exact isOpen_basicOpen 𝒜
· rintro p U hp ⟨s, hs⟩
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
obtain ⟨f, hfs, hfp⟩ := hp
refine ⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, ?_⟩
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
exact zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)
