English
The collection of subsets of the form Set.range (X.affineBasisCover.f a).base, as a ranges over the index set of the affineBasisCover, forms a topological basis for the underlying topological space of X.
Русский
Множество подмножеств вида Set.range (X.affineBasisCover.f a).base, где a пробегает по индексу affineBasisCover, образуют топологическую базу подлежащего пространства X.
LaTeX
$$TopologicalSpace.IsTopologicalBasis {x : Set X | ∃ a : X.affineBasisCover.I₀, x = Set.range (X.affineBasisCover.f a).base}$$
Lean4
theorem affineBasisCover_is_basis (X : Scheme.{u}) :
TopologicalSpace.IsTopologicalBasis
{x : Set X | ∃ a : X.affineBasisCover.I₀, x = Set.range (X.affineBasisCover.f a).base} :=
by
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
· rintro _ ⟨a, rfl⟩
exact IsOpenImmersion.isOpen_range (X.affineBasisCover.f a)
· rintro a U haU hU
rcases X.affineCover.covers a with ⟨x, e⟩
let U' := (X.affineCover.f (X.affineCover.idx a)).base ⁻¹' U
have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
rcases
PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU'
((X.affineCover.f (X.affineCover.idx a)).base.hom.continuous_toFun.isOpen_preimage _ hU) with
⟨_, ⟨_, ⟨s, rfl⟩, rfl⟩, hxV, hVU⟩
refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩ <;> rw [affineBasisCover_map_range]
· exact ⟨x, hxV, e⟩
· rw [Set.image_subset_iff]; exact hVU
