feat(category_theory/glue_data): Some more API for glue_data (#10881)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/category_theory/glue_data.lean

@@ -6,6 +6,8 @@ Authors: Andrew Yang
 import tactic.elementwise
 import category_theory.limits.shapes.multiequalizer
 import category_theory.limits.constructions.epi_mono
+import category_theory.limits.preserves.limits
+import category_theory.limits.shapes.types
 
 /-!
 # Gluing data
@@ -152,6 +154,11 @@ lemma glue_condition (i j : D.J) :
   D.t i j ≫ D.f j i ≫ D.ι j = D.f i j ≫ D.ι i :=
 (category.assoc _ _ _).symm.trans (multicoequalizer.condition D.diagram ⟨i, j⟩).symm
 
+/-- The pullback cone spanned by `V i j ⟶ U i` and `V i j ⟶ U j`.
+This will often be a pullback diagram. -/
+ def V_pullback_cone (i j : D.J) : pullback_cone (D.ι i) (D.ι j) :=
+ pullback_cone.mk (D.f i j) (D.t i j ≫ D.f j i) (by simp)
+
 variables [has_colimits C]
 
 /-- The projection `∐ D.U ⟶ D.glued` given by the colimit. -/
@@ -161,6 +168,23 @@ instance π_epi : epi D.π := by { unfold π, apply_instance }
 
 end
 
+lemma types_π_surjective (D : glue_data Type*) :
+  function.surjective D.π := (epi_iff_surjective _).mp infer_instance
+
+lemma types_ι_jointly_surjective (D : glue_data Type*) (x : D.glued) :
+  ∃ i (y : D.U i), D.ι i y = x :=
+begin
+  delta category_theory.glue_data.ι,
+  simp_rw ← multicoequalizer.ι_sigma_π D.diagram,
+  rcases D.types_π_surjective x with ⟨x', rfl⟩,
+  have := colimit.iso_colimit_cocone (types.coproduct_colimit_cocone _),
+  rw ← (show (colimit.iso_colimit_cocone (types.coproduct_colimit_cocone _)).inv _ = x',
+    from concrete_category.congr_hom
+      ((colimit.iso_colimit_cocone (types.coproduct_colimit_cocone _)).hom_inv_id) x'),
+  rcases (colimit.iso_colimit_cocone (types.coproduct_colimit_cocone _)).hom x' with ⟨i, y⟩,
+  exact ⟨i, y, by { simpa [← multicoequalizer.ι_sigma_π, -multicoequalizer.ι_sigma_π] }⟩
+end
+
 variables (F : C ⥤ C') [H : ∀ i j k, preserves_limit (cospan (D.f i j) (D.f i k)) F]
 
 include H
@@ -221,6 +245,75 @@ nat_iso.of_components
 @[simp] lemma diagram_iso_inv_app_right (i : D.J) :
   (D.diagram_iso F).inv.app (walking_multispan.right i) = 𝟙 _ := rfl
 
+variables [has_multicoequalizer D.diagram] [preserves_colimit D.diagram.multispan F]
+
+omit H
+
+lemma has_colimit_multispan_comp : has_colimit (D.diagram.multispan ⋙ F) :=
+⟨⟨⟨_,preserves_colimit.preserves (colimit.is_colimit _)⟩⟩⟩
+
+include H
+
+local attribute [instance] has_colimit_multispan_comp
+
+lemma has_colimit_map_glue_data_diagram : has_multicoequalizer (D.map_glue_data F).diagram :=
+has_colimit_of_iso (D.diagram_iso F).symm
+
+local attribute [instance] has_colimit_map_glue_data_diagram
+
+/-- If `F` preserves the gluing, we obtain an iso between the glued objects. -/
+def glued_iso : F.obj D.glued ≅ (D.map_glue_data F).glued :=
+preserves_colimit_iso F D.diagram.multispan ≪≫
+  (limits.has_colimit.iso_of_nat_iso (D.diagram_iso F))
+
+@[simp, reassoc]
+lemma ι_glued_iso_hom (i : D.J) :
+  F.map (D.ι i) ≫ (D.glued_iso F).hom = (D.map_glue_data F).ι i :=
+by { erw ι_preserves_colimits_iso_hom_assoc, rw has_colimit.iso_of_nat_iso_ι_hom,
+  erw category.id_comp, refl }
+
+@[simp, reassoc]
+lemma ι_glued_iso_inv (i : D.J) :
+  (D.map_glue_data F).ι i ≫ (D.glued_iso F).inv = F.map (D.ι i) :=
+by rw [iso.comp_inv_eq, ι_glued_iso_hom]
+
+/-- If `F` preserves the gluing, and reflects the pullback of `U i ⟶ glued` and `U j ⟶ glued`,
+then `F` reflects the fact that `V_pullback_cone` is a pullback. -/
+def V_pullback_cone_is_limit_of_map (i j : D.J) [reflects_limit (cospan (D.ι i) (D.ι j)) F]
+  (hc : is_limit ((D.map_glue_data F).V_pullback_cone i j)) :
+  is_limit (D.V_pullback_cone i j) :=
+begin
+  apply is_limit_of_reflects F,
+  apply (is_limit_map_cone_pullback_cone_equiv _ _).symm _,
+  let e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅
+    cospan ((D.map_glue_data F).ι i) ((D.map_glue_data F).ι j),
+  exact nat_iso.of_components
+    (λ x, by { cases x, exacts [D.glued_iso F, iso.refl _] })
+    (by rintros (_|_) (_|_) (_|_|_); simp),
+  apply is_limit.postcompose_hom_equiv e _ _,
+  apply hc.of_iso_limit,
+  refine cones.ext (iso.refl _) _,
+  { rintro (_|_|_),
+    change _ = _ ≫ (_ ≫ _) ≫ _,
+    all_goals { change _ = 𝟙 _ ≫ _ ≫ _, simpa } }
+end
+
+omit H
+
+/-- If there is a forgetful functor into `Type` that preserves enough (co)limits, then `D.ι` will
+be jointly surjective. -/
+lemma ι_jointly_surjective (F : C ⥤ Type v) [preserves_colimit D.diagram.multispan F]
+  [Π (i j k : D.J), preserves_limit (cospan (D.f i j) (D.f i k)) F] (x : F.obj (D.glued)) :
+  ∃ i (y : F.obj (D.U i)), F.map (D.ι i) y = x :=
+begin
+  let e := D.glued_iso F,
+  obtain ⟨i, y, eq⟩ := (D.map_glue_data F).types_ι_jointly_surjective (e.hom x),
+  replace eq := congr_arg e.inv eq,
+  change ((D.map_glue_data F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq,
+  rw [e.hom_inv_id, D.ι_glued_iso_inv] at eq,
+  exact ⟨i, y, eq⟩
+end
+
 end glue_data
 
 end category_theory