feat(algebraic_geometry): Explicit description of the colimit of presheafed spaces. (#10466)

Co-authored-by: erd1 <the.erd.one@gmail.com>

Author: erdOne

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -292,6 +292,89 @@ instance forget_preserves_colimits : preserves_colimits (PresheafedSpace.forget
       { intro j, dsimp, simp, }
     end } }
 
+/--
+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 componentwise_diagram (F : J ⥤ PresheafedSpace C)
+  (U : opens (limits.colimit F).carrier) : Jᵒᵖ ⥤ C :=
+{ 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
+    (eq_to_hom (by { rw [← colimit.w F f.unop, comp_base], refl })),
+  map_comp' := λ i j k f g,
+  begin
+    cases U,
+    dsimp,
+    simp_rw [map_comp_c_app, category.assoc],
+    congr' 1,
+    rw [Top.presheaf.pushforward.comp_inv_app, Top.presheaf.pushforward_eq_hom_app,
+      category_theory.nat_trans.naturality_assoc, Top.presheaf.pushforward_map_app],
+    congr' 1,
+    rw [category.id_comp, ← (F.obj (unop k)).presheaf.map_comp],
+    erw ← (F.obj (unop k)).presheaf.map_comp,
+    congr
+  end }
+
+/--
+The components of the colimit of a diagram of `PresheafedSpace C` is obtained
+via taking componentwise limits.
+-/
+def colimit_presheaf_obj_iso_componentwise_limit (F : J ⥤ PresheafedSpace C)
+  (U : opens (limits.colimit F).carrier) :
+  (limits.colimit F).presheaf.obj (op U) ≅ limit (componentwise_diagram F U) :=
+begin
+  refine ((sheaf_iso_of_iso (colimit.iso_colimit_cocone
+    ⟨_, colimit_cocone_is_colimit F⟩).symm).app (op U)).trans _,
+  refine (limit_obj_iso_limit_comp_evaluation _ _).trans (limits.lim.map_iso _),
+  fapply nat_iso.of_components,
+  { intro X,
+    refine ((F.obj (unop X)).presheaf.map_iso (eq_to_iso _)),
+    dsimp only [functor.op, unop_op, opens.map],
+    congr' 2,
+    rw set.preimage_preimage,
+    simp_rw ← comp_app,
+    congr' 2,
+    exact ι_preserves_colimits_iso_inv (forget C) F (unop X) },
+  { intros X Y f,
+    change ((F.map f.unop).c.app _ ≫ _ ≫ _) ≫ (F.obj (unop Y)).presheaf.map _ = _ ≫ _,
+    rw Top.presheaf.pushforward.comp_inv_app,
+    erw category.id_comp,
+    rw category.assoc,
+    erw [← (F.obj (unop Y)).presheaf.map_comp, (F.map f.unop).c.naturality_assoc,
+      ← (F.obj (unop Y)).presheaf.map_comp],
+    congr }
+end
+
+@[simp]
+lemma colimit_presheaf_obj_iso_componentwise_limit_inv_ι_app (F : J ⥤ PresheafedSpace C)
+  (U : opens (limits.colimit F).carrier) (j : J) :
+  (colimit_presheaf_obj_iso_componentwise_limit F U).inv ≫ (colimit.ι F j).c.app (op U) =
+    limit.π _ (op j) :=
+begin
+  delta colimit_presheaf_obj_iso_componentwise_limit,
+  rw [iso.trans_inv, iso.trans_inv, iso.app_inv, sheaf_iso_of_iso_inv, pushforward_to_of_iso_app,
+    congr_app (iso.symm_inv _)],
+  simp_rw category.assoc,
+  rw [← functor.map_comp_assoc, nat_trans.naturality],
+  erw ← comp_c_app_assoc,
+  rw congr_app (colimit.iso_colimit_cocone_ι_hom _ _),
+  simp_rw category.assoc,
+  erw [limit_obj_iso_limit_comp_evaluation_inv_π_app_assoc, lim_map_π_assoc],
+  convert category.comp_id _,
+  erw ← (F.obj j).presheaf.map_id,
+  iterate 2 { erw ← (F.obj j).presheaf.map_comp },
+  congr
+end
+
+@[simp]
+lemma colimit_presheaf_obj_iso_componentwise_limit_hom_π (F : J ⥤ PresheafedSpace C)
+  (U : opens (limits.colimit F).carrier) (j : J) :
+    (colimit_presheaf_obj_iso_componentwise_limit F U).hom ≫ limit.π _ (op j) =
+      (colimit.ι F j).c.app (op U) :=
+by rw [← iso.eq_inv_comp, colimit_presheaf_obj_iso_componentwise_limit_inv_ι_app]
+
 end PresheafedSpace
 
 end algebraic_geometry