English
If a set s of global sections spans the whole, then the supremum over basic opens of s equals the entire open U.
Русский
Если множество s секций глобальных покрывает всё, тогда объединение базовых открытых, порожденных s, равно всему U.
LaTeX
$$$\operatorname{span}(s) = \top \Rightarrow \bigvee_{f\in s} X.basicOpen f = U$$$
Lean4
/-- Given a spanning set of `Γ(X, U)`, the corresponding basic open sets cover `U`.
See `IsAffineOpen.basicOpen_union_eq_self_iff` for the inverse direction for affine open sets.
-/
theorem iSup_basicOpen_of_span_eq_top {X : Scheme} (U) (s : Set Γ(X, U)) (hs : Ideal.span s = ⊤) :
(⨆ i ∈ s, X.basicOpen i) = U := by
apply le_antisymm
· rw [iSup₂_le_iff]
exact fun i _ ↦ X.basicOpen_le i
· intro x hx
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open hx U.2
refine SetLike.mem_of_subset ?_ hxV
rw [←
(hV.basicOpen_union_eq_self_iff (X.presheaf.map (homOfLE hVU).op '' s)).mpr
(by rw [← Ideal.map_span, hs, Ideal.map_top])]
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image, Set.iUnion_exists,
Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res, Opens.coe_inf, Opens.coe_mk,
Set.iUnion_subset_iff]
exact fun i hi ↦ (Set.inter_subset_right.trans (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))
