English
The same identity compatibility as map_id_c_app in a broader gluing context: the c-app for the identity is given by pushforward id and pushforward equality.
Русский
Та же совместимость тождественного отображения с примером map_id_c_app в более широкой контексте склейки: c-app для тождественного отображения задается через pushforward id и pushforward equality.
LaTeX
$$$\\text{map\_id\_c\_app}(F,j,U) : (F.map(\\mathrm{id} j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq ...).hom.app U$$$
Lean4
theorem desc_c_naturality (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) {U V : (Opens s.pt.carrier)ᵒᵖ}
(i : U ⟶ V) :
s.pt.presheaf.map i ≫ descCApp F s V =
descCApp F s U ≫ (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s) _* (colimitCocone F).pt.presheaf).map i :=
by
dsimp [descCApp]
refine limit_obj_ext (fun j => ?_)
have w :=
Functor.congr_hom (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j))) i.unop
simp only [Opens.map_comp_map] at w
simp [congr_arg Quiver.Hom.op w]
