mem_grothendieckTopology — Mathlib

English

For a Scheme X and a presieve S on X, S lies in the grothendieckTopology P X iff there exists a covering Presieve (of arrows) bounding S from above.

Русский

Для схемы X и пресевиза S на X, S принадлежит grothendieckTopology P X тогда и только тогда, когда существует покрывающий Presieve (из стрелок), ограничивающий S сверху.

LaTeX

$$$S \\in grothendieckTopology P X \\iff \\exists (\\mathcal{U} : Cover.{u} (precoverage P) X), Presieve.ofArrows \\mathcal{U}.X \\mathcal{U}.f ≤ S$$$

Lean4

@[grind ←]
theorem mem_grothendieckTopology {X : Scheme.{u}} {𝒰 : X.Cover (precoverage P)} :
    Sieve.ofArrows 𝒰.X 𝒰.f ∈ grothendieckTopology P X :=
  by
  rw [Pretopology.mem_toGrothendieck]
  use Presieve.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology
  exact Sieve.le_generate (Presieve.ofArrows 𝒰.X 𝒰.f)

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