English
The construction descCApp realizes the universal property of the colimit cocone in the presheaf setting, yielding a colimit.
Русский
Конструкция descCApp реализует универсальное свойство колимитного кокона в настройке пресшеаф, образуя колимит.
LaTeX
$$$\\text{descCApp} : F \\to \\mathrm{colimitDesc}$$$
Lean4
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit`.
-/
def descCApp (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (U : (Opens s.pt.carrier)ᵒᵖ) :
s.pt.presheaf.obj U ⟶
(colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) _*
limit (pushforwardDiagramToColimit F).leftOp).obj
U :=
by
refine
limit.lift _
{ pt := s.pt.presheaf.obj U
π :=
{ app := fun j => ?_
naturality := fun j j' f => ?_ } } ≫
(limitObjIsoLimitCompEvaluation _ _).inv
· refine (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ?_)
dsimp
rw [← Opens.map_comp_obj]
simp
· dsimp
rw [PresheafedSpace.congr_app (s.w f.unop).symm U]
have w :=
Functor.congr_obj (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j)))
(unop U)
simp only [Opens.map_comp_obj_unop] at w
replace w := congr_arg op w
have w' := NatTrans.congr (F.map f.unop).c w
rw [w']
simp
