presieveOfSections — Mathlib

English

The presieve of sections assigns to a presieve P on U the set of global sections s ∈ Γ(X, U.toOpens) for which P(homOfLE(U.basicOpen_le s)) holds.

Русский

PresieveOfSections присваивает перисевью P на U множество глобальных секций s ∈ Γ(X, U.toOpens), для которых выполняется P(homOfLE(U.basicOpen_le s)).

LaTeX

$$$\\text{sectionsOfPresieve}(U)(P) = \\{\, s \\in \\Gamma(X, U^{\\mathrm{toOpens}}) \\mid P(\\mathrm{homOfLE}(U.\\mathrm{basicOpen\\_le}(s))) \\}$$$

Lean4

/-- The presieve associated to a set of sections.
This is a surjection, see `presieveOfSections_surjective`. -/
def presieveOfSections (U : X.AffineZariskiSite) (s : Set Γ(X, U.toOpens)) : Presieve U := fun V _ ↦
  ∃ f ∈ s, X.basicOpen f = V.toOpens

Похожие утверждения