presieveOfSections_eq_ofArrows — Mathlib

English

Same idea as 38777; the presieve of sections equals a presieve built from arrows given by basicOpen on sections.

Русский

Аналогично 38777; presieveOfSections равен presieve, построенному из стрел, заданных через basicOpen на секции.

LaTeX

$$$presieveOfSections\_U s = .ofArrows _ (fun i => U.basicOpen i.1) (fun i => homOfLE \ldots)$$$

Lean4

theorem presieveOfSections_eq_ofArrows (U : X.AffineZariskiSite) (s : Set Γ(X, U.toOpens)) :
    presieveOfSections U s = .ofArrows _ (fun i : s ↦ homOfLE (U.basicOpen_le i.1)) :=
  by
  refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
  · rintro ⟨f, hfs, rfl⟩
    exact .mk (ι := s) ⟨f, hfs⟩
  · rintro ⟨⟨f, hfs⟩⟩
    exact ⟨f, hfs, rfl⟩

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