mem_pretopology — Mathlib

English

For a fixed Scheme X and a presieve R on X, R lies in the pretopology defined by P iff there exists a cover by arrows whose Presieve.ofArrows equals R.

Русский

Для данного X и пресевиза R на X, R принадлежит предопокрытию, определяемому P, тогда и только тогда, существует покрытие стрелками, такое что Presieve.ofArrows равно R.

LaTeX

$$$R \\in pretopology P X \\iff \\exists (\\mathcal{U} : Cover.{u+1} (precoverage P) X), R = Presieve.ofArrows \\mathcal{U}.X \\mathcal{U}.f$$$

Lean4

@[grind ←]
theorem mem_pretopology {X : Scheme.{u}} {𝒰 : X.Cover (precoverage P)} : Presieve.ofArrows 𝒰.X 𝒰.f ∈ pretopology P X :=
  by
  rw [pretopology, Precoverage.toPretopology_toPrecoverage, ofArrows_mem_precoverage_iff]
  exact ⟨fun x ↦ ⟨𝒰.idx x, 𝒰.covers x⟩, 𝒰.map_prop⟩

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