English
The membership of a generated presieve in the Grothendieck topology corresponds to a span condition in the span of basic opens via generating arrows.
Русский
Принадлежность сгенерированного presieve в Grothendieck topology эквивалентна условию векторного расширения через базовые открытия.
LaTeX
$$$(\text{Sieve.generate}(presieveOfSections U s)) \in grothendieckTopology X U \iff \mathrm{span}(s)=\top$$$
Lean4
theorem generate_presieveOfSections_mem_grothendieckTopology {U : X.AffineZariskiSite} {s : Set Γ(X, U.toOpens)} :
Sieve.generate (presieveOfSections U s) ∈ grothendieckTopology X U ↔ Ideal.span s = ⊤ :=
by
rw [← U.2.self_le_basicOpen_union_iff, mem_grothendieckTopology, SetLike.le_def]
refine forall₂_congr fun x hx ↦ ?_
simp only [exists_and_left, TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe, Set.iUnion_coe_set,
TopologicalSpace.Opens.mem_mk, Set.mem_iUnion, SetLike.mem_coe, exists_prop, generate_presieveOfSections]
constructor
· simp only [basicOpen_mul]
rintro ⟨⟨V, hV⟩, ⟨f, hfs, g, rfl⟩, -, hxV⟩
exact ⟨f, hfs, hxV.1⟩
· rintro ⟨f, hfs, hxf⟩
refine ⟨U.basicOpen _, ⟨f, hfs, 1, rfl⟩, ⟨_, rfl⟩, by simpa using hxf⟩
