refactor: move morphisms in StructuredArrow to a lower universe (#6397)

This PR changes the definition
```lean
abbrev fromPUnit (X : C) : Discrete PUnit.{v + 1} ⥤ C :=
  (Functor.const _).obj X
```
to
```lean
abbrev fromPUnit (X : C) : Discrete PUnit.{w + 1} ⥤ C :=
  (Functor.const _).obj X
```
and then redefines
```lean
def StructuredArrow (S : D) (T : C ⥤ D) :=
  Comma (Functor.fromPUnit S) T
```
to
```lean
def StructuredArrow (S : D) (T : C ⥤ D) :=
  Comma (Functor.fromPUnit.{0} S) T
```

The effect of this is that given `{C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (S : D) (T : C ⥤ D)`, the morphisms of `StructuredArrow S T` no longer live in `max v₁ v₂`, but in `v₁`, as they should. Thus, this PR is basically a better version of #6388.

My guess for why we used to have the larger universe is that back in the day, the universes for limits were much more restricted, so stating the results of `Limits/Comma.lean` was not possible if the morphisms of `StructuredArrow` live in `v₁`. Luckily, by now it is possible to state everything correctly, and this PR adjusts `Limits/Comma.lean` and `Limits/Over.lean` accordingly.

Author: TwoFX

Mathlib/CategoryTheory/Closed/Zero.lean

@@ -23,7 +23,7 @@ object and one morphism.
 -/
 
 
-universe v u
+universe w v u
 
 noncomputable section
 
@@ -60,7 +60,7 @@ attribute [local instance] uniqueHomsetOfZero
 /-- A cartesian closed category with a zero object is equivalent to the category with one object and
 one morphism.
 -/
-def equivPUnit [HasZeroObject C] : C ≌ Discrete PUnit :=
+def equivPUnit [HasZeroObject C] : C ≌ Discrete PUnit.{w + 1} :=
   Equivalence.mk (Functor.star C) (Functor.fromPUnit 0)
     (NatIso.ofComponents
       (fun X =>

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -27,15 +27,15 @@ namespace CategoryTheory
 
 open Category Limits
 
-universe w' w v u₁ u₂ u₃
+universe w' w v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {J : Type w} [Category.{w'} J]
 
-variable {A : Type u₁} [Category.{v} A]
+variable {A : Type u₁} [Category.{v₁} A]
 
-variable {B : Type u₂} [Category.{v} B]
+variable {B : Type u₂} [Category.{v₂} B]
 
-variable {T : Type u₃} [Category.{v} T]
+variable {T : Type u₃} [Category.{v₃} T]
 
 namespace Comma
 
@@ -153,9 +153,10 @@ instance hasLimitsOfShape [HasLimitsOfShape J A] [HasLimitsOfShape J B]
     [PreservesLimitsOfShape J R] : HasLimitsOfShape J (Comma L R) where
 #align category_theory.comma.has_limits_of_shape CategoryTheory.Comma.hasLimitsOfShape
 
-instance hasLimits [HasLimits A] [HasLimits B] [PreservesLimits R] : HasLimits (Comma L R) :=
+instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} A] [HasLimitsOfSize.{w, w'} B]
+    [PreservesLimitsOfSize.{w, w'} R] : HasLimitsOfSize.{w, w'} (Comma L R) :=
   ⟨fun _ _ => inferInstance⟩
-#align category_theory.comma.has_limits CategoryTheory.Comma.hasLimits
+#align category_theory.comma.has_limits CategoryTheory.Comma.hasLimitsOfSize
 
 instance hasColimit (F : J ⥤ Comma L R) [HasColimit (F ⋙ fst L R)] [HasColimit (F ⋙ snd L R)]
     [PreservesColimit (F ⋙ fst L R) L] : HasColimit F :=
@@ -166,10 +167,10 @@ instance hasColimitsOfShape [HasColimitsOfShape J A] [HasColimitsOfShape J B]
     [PreservesColimitsOfShape J L] : HasColimitsOfShape J (Comma L R) where
 #align category_theory.comma.has_colimits_of_shape CategoryTheory.Comma.hasColimitsOfShape
 
-instance hasColimits [HasColimits A] [HasColimits B] [PreservesColimits L] :
-    HasColimits (Comma L R) :=
+instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [HasColimitsOfSize.{w, w'} B]
+    [PreservesColimitsOfSize.{w, w'} L] : HasColimitsOfSize.{w, w'} (Comma L R) :=
   ⟨fun _ _ => inferInstance⟩
-#align category_theory.comma.has_colimits CategoryTheory.Comma.hasColimits
+#align category_theory.comma.has_colimits CategoryTheory.Comma.hasColimitsOfSize
 
 end Comma
 
@@ -220,9 +221,10 @@ instance hasLimitsOfShape [HasLimitsOfShape J A] [PreservesLimitsOfShape J G] :
     HasLimitsOfShape J (StructuredArrow X G) where
 #align category_theory.structured_arrow.has_limits_of_shape CategoryTheory.StructuredArrow.hasLimitsOfShape
 
-instance hasLimits [HasLimits A] [PreservesLimits G] : HasLimits (StructuredArrow X G) :=
+instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} A] [PreservesLimitsOfSize.{w, w'} G] :
+    HasLimitsOfSize.{w, w'} (StructuredArrow X G) :=
   ⟨fun J hJ => by infer_instance⟩
-#align category_theory.structured_arrow.has_limits CategoryTheory.StructuredArrow.hasLimits
+#align category_theory.structured_arrow.has_limits CategoryTheory.StructuredArrow.hasLimitsOfSize
 
 noncomputable instance createsLimit [i : PreservesLimit (F ⋙ proj X G) G] :
     CreatesLimit F (proj X G) :=
@@ -237,8 +239,9 @@ noncomputable instance createsLimitsOfShape [PreservesLimitsOfShape J G] :
     CreatesLimitsOfShape J (proj X G) where
 #align category_theory.structured_arrow.creates_limits_of_shape CategoryTheory.StructuredArrow.createsLimitsOfShape
 
-noncomputable instance createsLimits [PreservesLimits G] : CreatesLimits (proj X G : _) where
-#align category_theory.structured_arrow.creates_limits CategoryTheory.StructuredArrow.createsLimits
+noncomputable instance createsLimitsOfSize [PreservesLimitsOfSize.{w, w'} G] :
+    CreatesLimitsOfSize.{w, w'} (proj X G : _) where
+#align category_theory.structured_arrow.creates_limits CategoryTheory.StructuredArrow.createsLimitsOfSize
 
 instance mono_right_of_mono [HasPullbacks A] [PreservesLimitsOfShape WalkingCospan G]
     {Y Z : StructuredArrow X G} (f : Y ⟶ Z) [Mono f] : Mono f.right :=
@@ -267,9 +270,10 @@ instance hasColimitsOfShape [HasColimitsOfShape J A] [PreservesColimitsOfShape J
     HasColimitsOfShape J (CostructuredArrow G X) where
 #align category_theory.costructured_arrow.has_colimits_of_shape CategoryTheory.CostructuredArrow.hasColimitsOfShape
 
-instance hasColimits [HasColimits A] [PreservesColimits G] : HasColimits (CostructuredArrow G X) :=
+instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [PreservesColimitsOfSize.{w, w'} G] :
+    HasColimitsOfSize.{w, w'} (CostructuredArrow G X) :=
   ⟨fun _ _ => inferInstance⟩
-#align category_theory.costructured_arrow.has_colimits CategoryTheory.CostructuredArrow.hasColimits
+#align category_theory.costructured_arrow.has_colimits CategoryTheory.CostructuredArrow.hasColimitsOfSize
 
 noncomputable instance createsColimit [i : PreservesColimit (F ⋙ proj G X) G] :
     CreatesColimit F (proj G X) :=
@@ -284,8 +288,9 @@ noncomputable instance createsColimitsOfShape [PreservesColimitsOfShape J G] :
     CreatesColimitsOfShape J (proj G X) where
 #align category_theory.costructured_arrow.creates_colimits_of_shape CategoryTheory.CostructuredArrow.createsColimitsOfShape
 
-noncomputable instance createsColimits [PreservesColimits G] : CreatesColimits (proj G X : _) where
-#align category_theory.costructured_arrow.creates_colimits CategoryTheory.CostructuredArrow.createsColimits
+noncomputable instance createsColimitsOfSize [PreservesColimitsOfSize.{w, w'} G] :
+    CreatesColimitsOfSize.{w, w'} (proj G X : _) where
+#align category_theory.costructured_arrow.creates_colimits CategoryTheory.CostructuredArrow.createsColimitsOfSize
 
 instance epi_left_of_epi [HasPushouts A] [PreservesColimitsOfShape WalkingSpan G]
     {Y Z : CostructuredArrow G X} (f : Y ⟶ Z) [Epi f] : Epi f.left :=

Mathlib/CategoryTheory/Limits/Over.lean

@@ -29,11 +29,11 @@ TODO: If `C` has binary products, then `forget X : Over X ⥤ C` has a right adj
 noncomputable section
 
 -- morphism levels before object levels. See note [category_theory universes].
-universe v u
+universe w' w v u
 
 open CategoryTheory CategoryTheory.Limits
 
-variable {J : Type v} [SmallCategory J]
+variable {J : Type w} [Category.{w'} J]
 
 variable {C : Type u} [Category.{v} C]
 
@@ -51,9 +51,9 @@ instance [HasColimitsOfShape J C] : HasColimitsOfShape J (Over X) where
 instance [HasColimits C] : HasColimits (Over X) :=
   ⟨inferInstance⟩
 
-instance createsColimits : CreatesColimits (forget X) :=
-  CostructuredArrow.createsColimits
-#align category_theory.over.creates_colimits CategoryTheory.Over.createsColimits
+instance createsColimitsOfSize : CreatesColimitsOfSize.{w, w'} (forget X) :=
+  CostructuredArrow.createsColimitsOfSize
+#align category_theory.over.creates_colimits CategoryTheory.Over.createsColimitsOfSize
 
 -- We can automatically infer that the forgetful functor preserves and reflects colimits.
 example [HasColimits C] : PreservesColimits (forget X) :=
@@ -150,9 +150,9 @@ theorem mono_iff_mono_right [HasPullbacks C] {f g : Under X} (h : f ⟶ g) : Mon
   StructuredArrow.mono_iff_mono_right _
 #align category_theory.under.mono_iff_mono_right CategoryTheory.Under.mono_iff_mono_right
 
-instance createsLimits : CreatesLimits (forget X) :=
-  StructuredArrow.createsLimits
-#align category_theory.under.creates_limits CategoryTheory.Under.createsLimits
+instance createsLimitsOfSize : CreatesLimitsOfSize.{w, w'} (forget X) :=
+  StructuredArrow.createsLimitsOfSize
+#align category_theory.under.creates_limits CategoryTheory.Under.createsLimitsOfSize
 
 -- We can automatically infer that the forgetful functor preserves and reflects limits.
 example [HasLimits C] : PreservesLimits (forget X) :=

Mathlib/CategoryTheory/PUnit.lean

@@ -17,7 +17,7 @@ and construct the equivalence `(Discrete PUnit ⥤ C) ≌ C`.
 -/
 
 
-universe v u
+universe w v u
 
 -- morphism levels before object levels. See note [CategoryTheory universes].
 namespace CategoryTheory
@@ -28,7 +28,7 @@ namespace Functor
 
 /-- The constant functor sending everything to `PUnit.star`. -/
 @[simps!]
-def star : C ⥤ Discrete PUnit :=
+def star : C ⥤ Discrete PUnit.{w + 1} :=
   (Functor.const _).obj ⟨⟨⟩⟩
 #align category_theory.functor.star CategoryTheory.Functor.star
 -- Porting note: simp can simplify this
@@ -37,26 +37,26 @@ variable {C}
 
 /-- Any two functors to `Discrete PUnit` are isomorphic. -/
 @[simps!]
-def punitExt (F G : C ⥤ Discrete PUnit) : F ≅ G :=
+def punitExt (F G : C ⥤ Discrete PUnit.{w + 1}) : F ≅ G :=
   NatIso.ofComponents fun X => eqToIso (by simp only [eq_iff_true_of_subsingleton])
 #align category_theory.functor.punit_ext CategoryTheory.Functor.punitExt
 -- Porting note: simp does indeed fire for these despite the linter warning
 attribute [nolint simpNF] punitExt_hom_app_down_down punitExt_inv_app_down_down
 
 /-- Any two functors to `Discrete PUnit` are *equal*.
 You probably want to use `punitExt` instead of this. -/
-theorem punit_ext' (F G : C ⥤ Discrete PUnit) : F = G :=
+theorem punit_ext' (F G : C ⥤ Discrete PUnit.{w + 1}) : F = G :=
   Functor.ext fun X => by simp only [eq_iff_true_of_subsingleton]
 #align category_theory.functor.punit_ext' CategoryTheory.Functor.punit_ext'
 
 /-- The functor from `Discrete PUnit` sending everything to the given object. -/
-abbrev fromPUnit (X : C) : Discrete PUnit.{v + 1} ⥤ C :=
+abbrev fromPUnit (X : C) : Discrete PUnit.{w + 1} ⥤ C :=
   (Functor.const _).obj X
 #align category_theory.functor.from_punit CategoryTheory.Functor.fromPUnit
 
 /-- Functors from `Discrete PUnit` are equivalent to the category itself. -/
 @[simps]
-def equiv : Discrete PUnit ⥤ C ≌ C where
+def equiv : Discrete PUnit.{w + 1} ⥤ C ≌ C where
   functor :=
     { obj := fun F => F.obj ⟨⟨⟩⟩
       map := fun θ => θ.app ⟨⟨⟩⟩ }
@@ -71,7 +71,7 @@ end Functor
   any two objects. (In fact, such a category is also a groupoid;
   see `CategoryTheory.Groupoid.ofHomUnique`) -/
 theorem equiv_punit_iff_unique :
-    Nonempty (C ≌ Discrete PUnit) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y) := by
+    Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y) := by
   constructor
   · rintro ⟨h⟩
     refine' ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro _⟩

Mathlib/CategoryTheory/StructuredArrow.lean

@@ -33,9 +33,11 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 has as its objects `D`-morphisms of the form `S ⟶ T Y`, for some `Y : C`,
 and morphisms `C`-morphisms `Y ⟶ Y'` making the obvious triangle commute.
 -/
+-- We explicitly come from `PUnit.{1}` here to obtain the correct universe for morphisms of
+-- structured arrows.
 -- @[nolint has_nonempty_instance]
 def StructuredArrow (S : D) (T : C ⥤ D) :=
-  Comma (Functor.fromPUnit S) T
+  Comma (Functor.fromPUnit.{0} S) T
 #align category_theory.structured_arrow CategoryTheory.StructuredArrow
 
 -- Porting note: not found by inferInstance
@@ -173,9 +175,6 @@ instance proj_faithful : Faithful (proj S T) where
   map_injective {_ _} := ext
 #align category_theory.structured_arrow.proj_faithful CategoryTheory.StructuredArrow.proj_faithful
 
-instance : LocallySmall.{v₁} (StructuredArrow S T) where
-  hom_small _ _ := small_of_injective ext
-
 /-- The converse of this is true with additional assumptions, see `mono_iff_mono_right`. -/
 theorem mono_of_mono_right {A B : StructuredArrow S T} (f : A ⟶ B) [h : Mono f.right] : Mono f :=
   (proj S T).mono_of_mono_map h
@@ -368,9 +367,11 @@ end StructuredArrow
 has as its objects `D`-morphisms of the form `S Y ⟶ T`, for some `Y : C`,
 and morphisms `C`-morphisms `Y ⟶ Y'` making the obvious triangle commute.
 -/
+-- We explicitly come from `PUnit.{1}` here to obtain the correct universe for morphisms of
+-- costructured arrows.
 -- @[nolint has_nonempty_instance] -- Porting note: removed
 def CostructuredArrow (S : C ⥤ D) (T : D) :=
-  Comma S (Functor.fromPUnit T)
+  Comma S (Functor.fromPUnit.{0} T)
 #align category_theory.costructured_arrow CategoryTheory.CostructuredArrow
 
 instance (S : C ⥤ D) (T : D) : Category (CostructuredArrow S T) := commaCategory
@@ -502,9 +503,6 @@ theorem ext_iff {A B : CostructuredArrow S T} (f g : A ⟶ B) : f = g ↔ f.left
 instance proj_faithful : Faithful (proj S T) where map_injective {_ _} := ext
 #align category_theory.costructured_arrow.proj_faithful CategoryTheory.CostructuredArrow.proj_faithful
 
-instance : LocallySmall.{v₁} (CostructuredArrow S T) where
-  hom_small _ _ := small_of_injective ext
-
 theorem mono_of_mono_left {A B : CostructuredArrow S T} (f : A ⟶ B) [h : Mono f.left] : Mono f :=
   (proj S T).mono_of_mono_map h
 #align category_theory.costructured_arrow.mono_of_mono_left CategoryTheory.CostructuredArrow.mono_of_mono_left