English
The map descCApp is natural with respect to morphisms i between opens, i.e., the naturality square commutes.
Русский
DescCApp Натурально по отношению к отображениям между открытыми множествами; диаграмма натуральности коммутирует.
LaTeX
$$$\\text{desc\_c\_naturality}(F,s,i) : s.pt.presheaf.map i ≃\\to \\text{descCApp} F s V$$$
Lean4
/-- Given a diagram of `PresheafedSpace C`s, its colimit is computed by pushing the sheaves onto
the colimit of the underlying spaces, and taking componentwise limit.
This is the componentwise diagram for an open set `U` of the colimit of the underlying spaces.
-/
@[simps]
def componentwiseDiagram (F : J ⥤ PresheafedSpace.{_, _, v} C) [HasColimit F] (U : Opens (Limits.colimit F).carrier) :
Jᵒᵖ ⥤ C
where
obj j := (F.obj (unop j)).presheaf.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U))
map {j k}
f := (F.map f.unop).c.app _ ≫ (F.obj (unop k)).presheaf.map (eqToHom (by rw [← colimit.w F f.unop, comp_base]; rfl))
map_comp {i j k} f
g := by
simp only [assoc, CategoryTheory.NatTrans.naturality_assoc]
simp
