feat(CategoryTheory): Grothendieck.map preserves finality (#19073)

Author: javra

Mathlib/CategoryTheory/EqToHom.lean

@@ -51,6 +51,14 @@ theorem eqToHom_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
   cases q
   simp
 
+/-- `eqToHom h` is heterogeneously equal to the identity of its domain. -/
+lemma eqToHom_heq_id_dom (X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 X) := by
+  subst h; rfl
+
+/-- `eqToHom h` is heterogeneously equal to the identity of its codomain. -/
+lemma eqToHom_heq_id_cod (X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 Y) := by
+  subst h; rfl
+
 /-- Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal.
 Note this used to be in the Functor namespace, where it doesn't belong. -/
 theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :

Mathlib/CategoryTheory/Grothendieck.lean

@@ -319,6 +319,7 @@ def compAsSmallFunctorEquivalence :
   counitIso := Iso.refl _
   unitIso := Iso.refl _
 
+variable {F} in
 /-- Mapping a Grothendieck construction along the whiskering of any natural transformation
 `α : F ⟶ G` with the functor `asSmallFunctor : Cat ⥤ Cat` is naturally isomorphic to conjugating
 `map α` with the equivalence between `Grothendieck (F ⋙ asSmallFunctor)` and `Grothendieck F`. -/
@@ -578,6 +579,11 @@ def ιCompFunctorFrom (c : C) : ι F c ⋙ (functorFrom fib hom hom_id hom_comp)
 
 end FunctorFrom
 
+/-- The fiber inclusion `ι F c` composed with `map α` is isomorphic to `α.app c ⋙ ι F' c`. -/
+@[simps!]
+def ιCompMap {F' : C ⥤ Cat} (α : F ⟶ F') (c : C) : ι F c ⋙ map α ≅ α.app c ⋙ ι F' c :=
+  NatIso.ofComponents (fun X => Iso.refl _) (fun f => by simp [map])
+
 end Grothendieck
 
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Final.lean

@@ -1,12 +1,14 @@
 /-
 Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
+Authors: Kim Morrison, Jakob von Raumer
 -/
+import Mathlib.CategoryTheory.Category.Cat.AsSmall
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
 import Mathlib.CategoryTheory.IsConnected
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 import Mathlib.CategoryTheory.Limits.Shapes.Types
+import Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
 import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.PUnit
@@ -42,6 +44,9 @@ From 3., we prove 1. directly in `final_of_colimit_comp_coyoneda_iso_pUnit`.
 Dually, we prove that if a functor `F : C ⥤ D` is initial, then any functor `G : D ⥤ E` has a
 limit if and only if `F ⋙ G` does, and these limits are isomorphic via `limit.pre G F`.
 
+In the end of the file, we characterize the finality of some important induced functors on the
+(co)structured arrow category (`StructuredArrow.pre` and `CostructuredArrow.pre`) and on the
+Grothendieck construction (`Grothendieck.pre` and `Grothendieck.map`).
 
 ## Naming
 There is some discrepancy in the literature about naming; some say 'cofinal' instead of 'final'.
@@ -1017,6 +1022,61 @@ instance Grothendieck.final_pre [hG : Final G] : (Grothendieck.pre F G).Final :=
   exact zigzag_prefunctor_obj_of_zigzag (Grothendieck.structuredArrowToStructuredArrowPre F G d f)
     (isPreconnected_zigzag (.mk gbi) (.mk gbj))
 
+open Limits
+
+/-- A natural transformation `α : F ⟶ G` between functors `F G : C ⥤ Cat` which is is final on each
+fiber `(α.app X)` induces an equivalence of fiberwise colimits of `map α ⋙ H` and `H` for each
+functor `H : Grothendieck G ⥤ Type`. -/
+def Grothendieck.fiberwiseColimitMapCompEquivalence {C : Type u₁} [Category.{v₁} C]
+    {F G : C ⥤ Cat.{v₂, u₂}} (α : F ⟶ G) [∀ X, Final (α.app X)] (H : Grothendieck G ⥤ Type u₂) :
+    fiberwiseColimit (map α ⋙ H) ≅ fiberwiseColimit H :=
+  NatIso.ofComponents
+    (fun X =>
+      HasColimit.isoOfNatIso ((Functor.associator _ _ _).symm ≪≫
+        isoWhiskerRight (ιCompMap α X) H ≪≫  Functor.associator _ _ _) ≪≫
+      Final.colimitIso (α.app X) (ι G X ⋙ H))
+    (fun f => colimit.hom_ext <| fun d => by
+      simp only [map, Cat.comp_obj, comp_obj, ι_obj, fiberwiseColimit_obj, fiberwiseColimit_map,
+        ιNatTrans, ιCompMap, Iso.trans_hom, Category.assoc, ι_colimMap_assoc, NatTrans.comp_app,
+        whiskerRight_app, Functor.comp_map, Cat.eqToHom_app, map_id, Category.comp_id,
+        associator_hom_app, colimit.ι_pre_assoc, HasColimit.isoOfNatIso_ι_hom_assoc, Iso.symm_hom,
+        isoWhiskerRight_hom, associator_inv_app, NatIso.ofComponents_hom_app, Iso.refl_hom,
+        Final.ι_colimitIso_hom, Category.id_comp, Final.ι_colimitIso_hom_assoc, colimit.ι_pre]
+      have := Functor.congr_obj (α.naturality f) d
+      dsimp at this
+      congr
+      apply eqToHom_heq_id_dom)
+
+/-- This is the small version of the more general lemma `Grothendieck.final_map` below. -/
+private lemma Grothendieck.final_map_small {C : Type u₁} [SmallCategory C] {F G : C ⥤ Cat.{u₁, u₁}}
+    (α : F ⟶ G) [hα : ∀ X, Final (α.app X)] : Final (map α) := by
+  rw [final_iff_isIso_colimit_pre]
+  intro H
+  let i := (colimitFiberwiseColimitIso _).symm ≪≫
+    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso _
+  convert Iso.isIso_hom i
+  apply colimit.hom_ext
+  intro X
+  simp [i, fiberwiseColimitMapCompEquivalence]
+
+/-- The functor `Grothendieck.map α` for a natural transformation `α : F ⟶ G`, with
+`F G : C ⥤ Cat`, is final if for each `X : C`, the functor `α.app X` is final. -/
+lemma Grothendieck.final_map {F G : C ⥤ Cat.{v₂, u₂}} (α : F ⟶ G) [hα : ∀ X, Final (α.app X)] :
+    Final (map α) := by
+  let sC : C ≌ AsSmall.{max u₁ u₂ v₁ v₂} C := AsSmall.equiv
+  let F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}
+  let G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}
+  let α' : F' ⟶ G' := whiskerLeft _ (whiskerRight α _)
+  have : ∀ X, Final (α'.app X) := fun X =>
+    inferInstanceAs (AsSmall.equiv.inverse ⋙ _ ⋙ AsSmall.equiv.functor).Final
+  have hα' : (map α').Final := final_map_small _
+  dsimp only [α', ← Equivalence.symm_functor] at hα'
+  have i := mapWhiskerLeftIsoConjPreMap sC.symm (whiskerRight α Cat.asSmallFunctor)
+    ≪≫ isoWhiskerLeft _ (isoWhiskerRight (mapWhiskerRightAsSmallFunctor α) _)
+  have := final_of_natIso i
+  rwa [← final_iff_equivalence_comp, ← final_iff_comp_equivalence,
+    ← final_iff_equivalence_comp, ← final_iff_comp_equivalence] at this
+
 end Grothendieck
 
 section Prod