Lean4
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
-/
def colimitCoconeIsColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) : IsColimit (colimitCocone F)
where
desc s := desc F s
fac s := desc_fac F s
uniq s m
w := by
-- We need to use the identity on the continuous maps twice, so we prepare that first:
have t : m.base = colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) :=
by
dsimp
-- `colimit.hom_ext` used to be automatically applied by `ext` before https://github.com/leanprover-community/mathlib4/pull/21302
apply colimit.hom_ext fun j => ?_
ext
rw [colimit.ι_desc, mapCocone_ι_app, ← w j]
simp
ext : 1
· exact t
· refine NatTrans.ext (funext fun U => limit_obj_ext fun j => ?_)
simp [desc, descCApp, PresheafedSpace.congr_app (w (unop j)).symm U,
NatTrans.congr (limit.π (pushforwardDiagramToColimit F).leftOp j)
(congr_arg op (Functor.congr_obj (congr_arg Opens.map t) (unop U)))]
