English
The generated sieve from presieveOfSections equals the arrow extension of basic opens: an arrow f is in the generated sieve iff there exist f1 in s and g with X.basicOpen(f1 g) = V.toOpens.
Русский
Порождение сита из presieveOfSections совпадает с расширением стрел через basicOpen: стрелка f принадлежит соругенному сорту тогда и только тогда, существует f1 в s и g с X.basicOpen(f1 g) = V.toOpens.
LaTeX
$$$\text{Sieve.generate}(presieveOfSections U s) f \iff \exists f_1\in s, \exists g, X.basicOpen(f_1 g) = V.toOpens$$$
Lean4
theorem generate_presieveOfSections {U V : X.AffineZariskiSite} {s : Set Γ(X, U.toOpens)} {f : V ⟶ U} :
Sieve.generate (presieveOfSections U s) f ↔ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens :=
by
obtain ⟨V, hV⟩ := V
constructor
· rintro ⟨⟨W, hW⟩, ⟨f₁, hf₁⟩, -, ⟨f₂, hf₂s, rfl⟩, rfl⟩
subst hf₁
obtain ⟨f₃, hf₃⟩ := U.2.basicOpen_basicOpen_is_basicOpen f₂ f₁
refine ⟨f₂, hf₂s, f₃, ?_⟩
rw [X.basicOpen_mul, hf₃, inf_eq_right]
exact X.basicOpen_le _
· rintro ⟨f₁, hf₁s, f₂, rfl⟩
refine ⟨U.basicOpen f₁, ⟨f₂ |_ _, ?_⟩, ⟨f₁, rfl⟩, ⟨f₁, hf₁s, rfl⟩, rfl⟩
exact (X.basicOpen_res _ _).trans (X.basicOpen_mul _ _).symm
