From 2e0b67b8e495c0c8b7162686b6b639101a7afef8 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Sat, 26 Oct 2024 14:30:59 +0000
Subject: [PATCH] feat(CategoryTheory/Grothendieck): `Grothendieck.pre` for
 Grothendieck construction base change (#18044)

Needed in order to use the Grothendieck construction as a way to express dependent double colimits. This also makes the following changes:
* Improves `Grothendieck.comp_base` to trigger without using `erw` (by deriving it manually instead of by `@[simps]`
* Generalizes `IsConnected.zigzag_obj_of_zigzag` from functors to prefunctors since proving functoriality at use sites makes no sense (since we throw away the data anyway and just keep a disjunction of a `Nonempty` of morphism types.
---
 Mathlib/CategoryTheory/Grothendieck.lean | 32 +++++++++++++-----
 Mathlib/CategoryTheory/IsConnected.lean  |  9 ++++-
 Mathlib/CategoryTheory/Limits/Final.lean | 43 ++++++++++++++++++++++++
 3 files changed, 74 insertions(+), 10 deletions(-)

diff --git a/Mathlib/CategoryTheory/Grothendieck.lean b/Mathlib/CategoryTheory/Grothendieck.lean
index 5a361423ddbc9..a6af93f1d5667 100644
--- a/Mathlib/CategoryTheory/Grothendieck.lean
+++ b/Mathlib/CategoryTheory/Grothendieck.lean
@@ -94,7 +94,6 @@ instance (X : Grothendieck F) : Inhabited (Hom X X) :=
 
 /-- Composition of morphisms in the Grothendieck category.
 -/
-@[simps]
 def comp {X Y Z : Grothendieck F} (f : Hom X Y) (g : Hom Y Z) : Hom X Z where
   base := f.base ≫ g.base
   fiber :=
@@ -108,15 +107,15 @@ instance : Category (Grothendieck F) where
   comp := @fun _ _ _ f g => Grothendieck.comp f g
   comp_id := @fun X Y f => by
     dsimp; ext
-    · simp
-    · dsimp
+    · simp [comp]
+    · dsimp [comp]
       rw [← NatIso.naturality_2 (eqToIso (F.map_id Y.base)) f.fiber]
       simp
-  id_comp := @fun X Y f => by dsimp; ext <;> simp
+  id_comp := @fun X Y f => by dsimp; ext <;> simp [comp]
   assoc := @fun W X Y Z f g h => by
     dsimp; ext
-    · simp
-    · dsimp
+    · simp [comp]
+    · dsimp [comp]
       rw [← NatIso.naturality_2 (eqToIso (F.map_comp _ _)) f.fiber]
       simp
 
@@ -126,11 +125,16 @@ theorem id_fiber' (X : Grothendieck F) :
   id_fiber X
 
 @[simp]
-theorem comp_fiber' {X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) :
+theorem comp_base {X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).base = f.base ≫ g.base :=
+  rfl
+
+@[simp]
+theorem comp_fiber {X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) :
     Hom.fiber (f ≫ g) =
     eqToHom (by erw [Functor.map_comp, Functor.comp_obj]) ≫
     (F.map g.base).map f.fiber ≫ g.fiber :=
-  comp_fiber f g
+  rfl
 
 
 theorem congr {X Y : Grothendieck F} {f g : X ⟶ Y} (h : f = g) :
@@ -170,7 +174,7 @@ def map (α : F ⟶ G) : Grothendieck F ⥤ Grothendieck G where
   map_comp {X Y Z} f g := by
     dsimp
     congr 1
-    simp only [comp_fiber' f g, ← Category.assoc, Functor.map_comp, eqToHom_map]
+    simp only [comp_fiber f g, ← Category.assoc, Functor.map_comp, eqToHom_map]
     congr 1
     simp only [Cat.eqToHom_app, Cat.comp_obj, eqToHom_trans, eqToHom_map, Category.assoc]
     erw [Functor.congr_hom (α.naturality g.base).symm f.fiber]
@@ -292,6 +296,16 @@ def grothendieckTypeToCat : Grothendieck (G ⋙ typeToCat) ≌ G.Elements where
     simp
     rfl
 
+variable (F) in
+/-- Applying a functor `G : D ⥤ C` to the base of the Grothendieck construction induces a functor
+`Grothendieck (G ⋙ F) ⥤ Grothendieck F`. -/
+@[simps]
+def pre (G : D ⥤ C) : Grothendieck (G ⋙ F) ⥤ Grothendieck F where
+  obj X := ⟨G.obj X.base, X.fiber⟩
+  map f := ⟨G.map f.base, f.fiber⟩
+  map_id X := Grothendieck.ext _ _ (G.map_id _) (by simp)
+  map_comp f g := Grothendieck.ext _ _ (G.map_comp _ _) (by simp)
+
 end Grothendieck
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/IsConnected.lean b/Mathlib/CategoryTheory/IsConnected.lean
index c6b21cf4cbce6..fc0e0c664675e 100644
--- a/Mathlib/CategoryTheory/IsConnected.lean
+++ b/Mathlib/CategoryTheory/IsConnected.lean
@@ -324,12 +324,19 @@ def Zigzag.setoid (J : Type u₂) [Category.{v₁} J] : Setoid J where
   r := Zigzag
   iseqv := zigzag_equivalence
 
+/-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
+`F j₂` as long as `F` is a prefunctor.
+-/
+theorem zigzag_prefunctor_obj_of_zigzag (F : J ⥤q K) {j₁ j₂ : J} (h : Zigzag j₁ j₂) :
+    Zigzag (F.obj j₁) (F.obj j₂) :=
+  h.lift _ fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)
+
 /-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
 `F j₂` as long as `F` is a functor.
 -/
 theorem zigzag_obj_of_zigzag (F : J ⥤ K) {j₁ j₂ : J} (h : Zigzag j₁ j₂) :
     Zigzag (F.obj j₁) (F.obj j₂) :=
-  h.lift _ fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)
+  zigzag_prefunctor_obj_of_zigzag F.toPrefunctor h
 
 /-- A Zag in a discrete category entails an equality of its extremities -/
 lemma eq_of_zag (X) {a b : Discrete X} (h : Zag a b) : a.as = b.as :=
diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index 6390aaa372617..2cd80eb36a4f4 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -10,6 +10,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Types
 import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.PUnit
+import Mathlib.CategoryTheory.Grothendieck
 
 /-!
 # Final and initial functors
@@ -848,4 +849,46 @@ instance CostructuredArrow.initial_pre (T : C ⥤ D) [Initial T] (S : D ⥤ E) (
 
 end
 
+section Grothendieck
+
+variable {C : Type u₁} [Category.{v₁} C]
+variable {D : Type u₂} [Category.{v₂} D]
+variable (F : D ⥤ Cat) (G : C ⥤ D)
+
+open Functor
+
+/-- A prefunctor mapping structured arrows on `G` to structured arrows on `pre F G` with their
+action on fibers being the identity. -/
+def Grothendieck.structuredArrowToStructuredArrowPre (d : D) (f : F.obj d) :
+    StructuredArrow d G ⥤q StructuredArrow ⟨d, f⟩ (pre F G) where
+  obj := fun X => StructuredArrow.mk (Y := ⟨X.right, (F.map X.hom).obj f⟩)
+    (Grothendieck.Hom.mk (by exact X.hom) (by dsimp; exact 𝟙 _))
+  map := fun g => StructuredArrow.homMk
+    (Grothendieck.Hom.mk (by exact g.right)
+      (eqToHom (by dsimp; rw [← StructuredArrow.w g, map_comp, Cat.comp_obj])))
+    (by simp only [StructuredArrow.mk_right]
+        apply Grothendieck.ext <;> simp)
+
+instance Grothendieck.final_pre [hG : Final G] : (Grothendieck.pre F G).Final := by
+  constructor
+  rintro ⟨d, f⟩
+  let ⟨u, c, g⟩ : Nonempty (StructuredArrow d G) := inferInstance
+  letI :  Nonempty (StructuredArrow ⟨d, f⟩ (pre F G)) :=
+    ⟨u, ⟨c, (F.map g).obj f⟩, ⟨(by exact g), (by exact 𝟙 _)⟩⟩
+  apply zigzag_isConnected
+  rintro ⟨⟨⟨⟩⟩, ⟨bi, fi⟩, ⟨gbi, gfi⟩⟩ ⟨⟨⟨⟩⟩, ⟨bj, fj⟩, ⟨gbj, gfj⟩⟩
+  dsimp at fj fi gfi gbi gbj gfj
+  apply Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bi, ((F.map gbi).obj f)⟩)
+      (Grothendieck.Hom.mk gbi (𝟙 _)))
+    (.of_zag (.inr ⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _)
+      (eqToHom (by simp) ≫ gfi)) (by apply Grothendieck.ext <;> simp)⟩))
+  refine Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bj, ((F.map gbj).obj f)⟩)
+      (Grothendieck.Hom.mk gbj (𝟙 _))) ?_
+    (.of_zag (.inl ⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _)
+      (eqToHom (by simp) ≫ gfj)) (by apply Grothendieck.ext <;> simp)⟩))
+  exact zigzag_prefunctor_obj_of_zigzag (Grothendieck.structuredArrowToStructuredArrowPre F G d f)
+    (isPreconnected_zigzag (.mk gbi) (.mk gbj))
+
+end Grothendieck
+
 end CategoryTheory