English
For a family of opens U: J → X.opens, the construction iSupOpenCover(U) yields an open cover of the supremum ⨆ i, U(i) by the pieces coming from each U(i).
Русский
Для семейства открытых подмножеств U: J → X.opens конструкция iSupOpenCover(U) задаёт открытое покрытие множества верхнего дерева ⨆ i, U(i) плитами, соответствующими каждому U(i).
LaTeX
$$$i\\mathrm{SupOpenCover}(U) : (\\bigsqcup i, U(i)).\\text{toScheme}.OpenCover$, i.e. \\text{open cover of } \\big(\\bigvee_i U(i)\\big)\\, \\text{by } U(i).$$
Lean4
/-- The open cover of `⋃ Vᵢ` by `Vᵢ`. -/
def iSupOpenCover {J : Type*} {X : Scheme} (U : J → X.Opens) : (⨆ i, U i).toScheme.OpenCover
where
I₀ := J
X i := U i
f j := X.homOfLE (le_iSup _ _)
mem₀ := by
rw [presieve₀_mem_precoverage_iff]
refine ⟨fun x ↦ ?_, inferInstance⟩
obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp x.2
use i, ⟨x.1, hi⟩
apply Subtype.ext
simp
