plusPlusSheaf — Mathlib

English

The sheafification functor is extended to take values in Sheaf, i.e., it assigns to each presheaf its associated sheaf and to morphisms the induced morphisms between sheaves.

Русский

Функтор замыкания-через замыкание определяется как функтор, принимающий прехааз и отправляющий их вAssociated sheaf, и отображает морфизмы соответствующим образом.

LaTeX

$$$\\text{plusPlusSheaf} : (C^{op} \\to D) \\to \\mathrm{Sheaf}\\ J\\ D$$$

Lean4

/-- The sheafification functor, as a functor taking values in `Sheaf`. -/
@[simps]
noncomputable def plusPlusSheaf : (Cᵒᵖ ⥤ D) ⥤ Sheaf J D
    where
  obj P := ⟨J.sheafify P, J.sheafify_isSheaf P⟩
  map η := ⟨J.sheafifyMap η⟩
  map_id _ := Sheaf.Hom.ext <| J.sheafifyMap_id _
  map_comp _ _ := Sheaf.Hom.ext <| J.sheafifyMap_comp _ _

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