feat(CategoryTheory): Relation between the Grothendieck construction …

…and `AsSmall` (#19539)

Mathlib.lean

@@ -1624,6 +1624,7 @@ import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Category.Bipointed
 import Mathlib.CategoryTheory.Category.Cat
 import Mathlib.CategoryTheory.Category.Cat.Adjunction
+import Mathlib.CategoryTheory.Category.Cat.AsSmall
 import Mathlib.CategoryTheory.Category.Cat.Limit
 import Mathlib.CategoryTheory.Category.Factorisation
 import Mathlib.CategoryTheory.Category.GaloisConnection

Mathlib/CategoryTheory/Category/Cat/AsSmall.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2024 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jakob von Raumer
+-/
+import Mathlib.CategoryTheory.Category.Cat
+import Mathlib.CategoryTheory.Category.ULift
+
+/-!
+# Functorially embedding `Cat` into the category of small categories
+
+There is a canonical functor `asSmallFunctor` between the category of categories of any size and
+any larger category of small categories.
+
+## Future Work
+
+Show that `asSmallFunctor` is faithful.
+-/
+
+universe w v u
+
+namespace CategoryTheory
+
+namespace Cat
+
+/-- Assigning to each category `C` the small category `AsSmall C` induces a functor `Cat ⥤ Cat`. -/
+@[simps]
+def asSmallFunctor : Cat.{v, u} ⥤ Cat.{max w v u, max w v u} where
+  obj C := .of <| AsSmall C
+  map F := AsSmall.down ⋙ F ⋙ AsSmall.up
+
+end Cat
+
+end CategoryTheory

Mathlib/CategoryTheory/Category/ULift.lean

@@ -174,6 +174,16 @@ def AsSmall.down : AsSmall C ⥤ C where
   obj X := ULift.down X
   map f := f.down
 
+@[reassoc]
+theorem down_comp {X Y Z : AsSmall C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).down = f.down ≫ g.down :=
+  rfl
+
+@[simp]
+theorem eqToHom_down {X Y : AsSmall C} (h : X = Y) :
+    (eqToHom h).down = eqToHom (congrArg ULift.down h) := by
+  subst h
+  rfl
+
 /-- The equivalence between `C` and `AsSmall C`. -/
 @[simps]
 def AsSmall.equiv : C ≌ AsSmall C where

Mathlib/CategoryTheory/Grothendieck.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Sina Hazratpour
 -/
-import Mathlib.CategoryTheory.Category.Cat
+import Mathlib.CategoryTheory.Category.Cat.AsSmall
 import Mathlib.CategoryTheory.Elements
 import Mathlib.CategoryTheory.Comma.Over
 
@@ -38,12 +38,13 @@ See also `CategoryTheory.Functor.Elements` for the category of elements of funct
 -/
 
 
-universe u
+universe w u v u₁ v₁ u₂ v₂
 
 namespace CategoryTheory
 
-variable {C D : Type*} [Category C] [Category D]
-variable (F : C ⥤ Cat)
+variable {C : Type u} [Category.{v} C]
+variable {D : Type u₁} [Category.{v₁} D]
+variable (F : C ⥤ Cat.{v₂, u₂})
 
 /--
 The Grothendieck construction (often written as `∫ F` in mathematics) for a functor `F : C ⥤ Cat`
@@ -229,9 +230,65 @@ theorem map_comp_eq (α : F ⟶ G) (β : G ⟶ H) :
 if possible, and we should prefer `map_comp_iso` to `map_comp_eq` whenever we can. -/
 def mapCompIso (α : F ⟶ G) (β : G ⟶ H) : map (α ≫ β) ≅ map α ⋙ map β := eqToIso (map_comp_eq α β)
 
-end
+variable (F)
 
-universe v
+/-- The inverse functor to build the equivalence `compAsSmallFunctorEquivalence`. -/
+@[simps]
+def compAsSmallFunctorEquivalenceInverse :
+    Grothendieck F ⥤ Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) where
+  obj X := ⟨X.base, AsSmall.up.obj X.fiber⟩
+  map f := ⟨f.base, AsSmall.up.map f.fiber⟩
+
+/-- The functor to build the equivalence `compAsSmallFunctorEquivalence`. -/
+@[simps]
+def compAsSmallFunctorEquivalenceFunctor :
+    Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) ⥤ Grothendieck F where
+  obj X := ⟨X.base, AsSmall.down.obj X.fiber⟩
+  map f := ⟨f.base, AsSmall.down.map f.fiber⟩
+  map_id _ := by apply Grothendieck.ext <;> simp
+  map_comp _ _ := by apply Grothendieck.ext <;> simp [down_comp]
+
+/-- Taking the Grothendieck construction on `F ⋙ asSmallFunctor`, where
+`asSmallFunctor : Cat ⥤ Cat` is the functor which turns each category into a small category of a
+(potentiall) larger universe, is equivalent to the Grothendieck construction on `F` itself. -/
+@[simps]
+def compAsSmallFunctorEquivalence :
+    Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) ≌ Grothendieck F where
+  functor := compAsSmallFunctorEquivalenceFunctor F
+  inverse := compAsSmallFunctorEquivalenceInverse F
+  counitIso := Iso.refl _
+  unitIso := Iso.refl _
+
+/-- 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`. -/
+def mapWhiskerRightAsSmallFunctor (α : F ⟶ G) :
+    map (whiskerRight α Cat.asSmallFunctor.{w}) ≅
+    (compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙
+      (compAsSmallFunctorEquivalence G).inverse :=
+  NatIso.ofComponents
+    (fun X => Iso.refl _)
+    (fun f => by
+      fapply Grothendieck.ext
+      · simp [compAsSmallFunctorEquivalenceInverse]
+      · simp only [compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse,
+          Functor.comp_obj, compAsSmallFunctorEquivalenceInverse_obj_base, map_obj_base,
+          compAsSmallFunctorEquivalenceFunctor_obj_base, Cat.asSmallFunctor_obj, Cat.of_α,
+          Iso.refl_hom, Functor.comp_map, comp_base, id_base,
+          compAsSmallFunctorEquivalenceInverse_map_base, map_map_base,
+          compAsSmallFunctorEquivalenceFunctor_map_base, Cat.asSmallFunctor_map, map_obj_fiber,
+          whiskerRight_app, AsSmall.down_obj, AsSmall.up_obj_down,
+          compAsSmallFunctorEquivalenceInverse_obj_fiber,
+          compAsSmallFunctorEquivalenceFunctor_obj_fiber, comp_fiber, map_map_fiber,
+          AsSmall.down_map, down_comp, eqToHom_down, AsSmall.up_map_down, Functor.map_comp,
+          eqToHom_map, id_fiber, Category.assoc, eqToHom_trans_assoc,
+          compAsSmallFunctorEquivalenceInverse_map_fiber,
+          compAsSmallFunctorEquivalenceFunctor_map_fiber, eqToHom_comp_iff, comp_eqToHom_iff]
+        simp only [eqToHom_trans_assoc, Category.assoc, conj_eqToHom_iff_heq']
+        rw [G.map_id]
+        simp )
+
+end
 
 /-- The Grothendieck construction as a functor from the functor category `E ⥤ Cat` to the
 over category `Over E`. -/
@@ -245,8 +302,6 @@ def functor {E : Cat.{v,u}} : (E ⥤ Cat.{v,u}) ⥤ Over (T := Cat.{v,u}) E wher
     simp [Grothendieck.map_comp_eq α β]
     rfl
 
-universe w
-
 variable (G : C ⥤ Type w)
 
 /-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration. -/