sheafEquiv — Mathlib

English

Another form of the equality: presieveOfSections U s equals the ofArrows construction with arrows given by basicOpen on sections.

Русский

Еще одна форма равенства: presieveOfSections U s равно конструктору ofArrows со стрелами, заданными через basicOpen на секциях.

LaTeX

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

Lean4

/-- The category of sheaves on `X.AffineZariskiSite` is equivalent to the categories of sheaves
over `X`. -/
abbrev sheafEquiv : Sheaf (grothendieckTopology X) A ≌ TopCat.Sheaf A X :=
  (toOpensFunctor X).sheafInducedTopologyEquivOfIsCoverDense _ _

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