Lean4
/-- Given a diagram of presheafed spaces,
we can push all the presheaves forward to the colimit `X` of the underlying topological spaces,
obtaining a diagram in `(Presheaf C X)ᵒᵖ`.
-/
@[simps]
def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
J ⥤ (Presheaf C (colimit (F ⋙ PresheafedSpace.forget C)))ᵒᵖ
where
obj j := op (colimit.ι (F ⋙ PresheafedSpace.forget C) j _* (F.obj j).presheaf)
map {j j'}
f :=
((pushforward C (colimit.ι (F ⋙ PresheafedSpace.forget C) j')).map (F.map f).c ≫
(Pushforward.comp ((F ⋙ PresheafedSpace.forget C).map f) (colimit.ι (F ⋙ PresheafedSpace.forget C) j')
(F.obj j).presheaf).inv ≫
(pushforwardEq (colimit.w (F ⋙ PresheafedSpace.forget C) f) (F.obj j).presheaf).hom).op
map_id
j := by
apply (opEquiv _ _).injective
refine NatTrans.ext (funext fun U => ?_)
induction U with
| op U =>
simp [opEquiv]
rfl
map_comp {j₁ j₂ j₃} f
g := by
apply (opEquiv _ _).injective
refine NatTrans.ext (funext fun U => ?_)
dsimp [opEquiv]
have :
op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj U.unop)) =
op ((Opens.map (colimit.ι (F ⋙ PresheafedSpace.forget C) j₂)).obj (unop U)) :=
by
apply unop_injective
rw [← Opens.map_comp_obj]
congr
exact colimit.w (F ⋙ PresheafedSpace.forget C) g
simp only [map_comp_c_app, pushforward_obj_obj, pushforward_map_app, comp_base, pushforwardEq_hom_app, op_obj,
Opens.map_comp_obj, id_comp, assoc, eqToHom_map_comp, NatTrans.naturality_assoc, pushforward_obj_map,
eqToHom_unop]
simp [NatTrans.congr (α := (F.map f).c) this]
