English
The toPresheaf functor intertwines with equivalences arising from pushforward/sheafification constructions
Русский
toPresheaf согласуется с эквивалентностями, возникающими из построения pushforward и sheafification
LaTeX
$$$\\text{toPresheaf }(R) \\circ \\mathrm{sheafification}(\\alpha) \\cong \\mathrm{sheafification}(\\alpha) \\circ \\text{toPresheaf }(R_0)$$$
Lean4
/-- Given a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
and `R` a sheaf of rings (i.e. `R` identifies to the sheafification of `R₀`), this is
the associated sheaf of modules functor `PresheafOfModules.{v} R₀ ⥤ SheafOfModules.{v} R`. -/
@[simps! -isSimp map]
noncomputable def sheafification : PresheafOfModules.{v} R₀ ⥤ SheafOfModules.{v} R
where
obj M₀ := sheafify α (CategoryTheory.toSheafify J M₀.presheaf)
map
f := sheafifyMap _ _ _ f ((toPresheaf R₀ ⋙ presheafToSheaf J AddCommGrpCat).map f) (by apply toSheafify_naturality)
map_id
M₀ := by
ext1
apply (toPresheaf _).map_injective
simp
rfl
map_comp _
_ := by
ext1
apply (toPresheaf _).map_injective
simp
rfl
