presieveOfSections_sectionsOfPresieve

English

The presieveOfSections is equal to an arrow-based presieve description: the presieve generated by sections corresponds to arrows given by basicOpen of sections.

Русский

PresieveOfSections совпадает с описанием через стрелы: порожденный разделами заново описывает стрелы через basicOpen секций.

LaTeX

$$$presieveOfSections U s = .ofArrows _ (\!\! i \mapsto homOfLE (U.basicOpen_le i.1))$$$

Lean4

theorem presieveOfSections_sectionsOfPresieve {U : X.AffineZariskiSite} (P : Presieve U) :
    presieveOfSections U (sectionsOfPresieve P) = P :=
  by
  refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
  · rintro ⟨_, H, rfl⟩
    exact H
  · intro H
    obtain rfl : _ = V := hf
    exact ⟨_, H, rfl⟩

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