chore(category_theory): switch ulift and filtered in import hierarchy (…

…#13302)

Many files require `ulift` but not `filtered`, so `ulift` should be lower in the import hierarchy. This avoids needing all of `data/` up to `data/fintype/basic` before we can start defining categorical limits.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/category/ulift.lean

@@ -5,7 +5,7 @@ Authors: Adam Topaz
 -/
 import category_theory.category.basic
 import category_theory.equivalence
-import category_theory.filtered
+import category_theory.eq_to_hom
 
 /-!
 # Basic API for ulift
@@ -74,12 +74,6 @@ def ulift.equivalence : C ≌ (ulift.{u₂} C) :=
   inv_hom_id' := by {ext, change (𝟙 _) ≫ (𝟙 _) = 𝟙 _, simp} },
   functor_unit_iso_comp' := λ X, by {change (𝟙 X) ≫ (𝟙 X) = 𝟙 X, simp} }
 
-instance [is_filtered C] : is_filtered (ulift.{u₂} C) :=
-is_filtered.of_equivalence ulift.equivalence
-
-instance [is_cofiltered C] : is_cofiltered (ulift.{u₂} C) :=
-is_cofiltered.of_equivalence ulift.equivalence
-
 section ulift_hom
 
 /-- `ulift_hom.{w} C` is an alias for `C`, which is endowed with a category instance
@@ -122,12 +116,6 @@ def ulift_hom.equiv : C ≌ ulift_hom C :=
   unit_iso := nat_iso.of_components (λ A, eq_to_iso rfl) (by tidy),
   counit_iso := nat_iso.of_components (λ A, eq_to_iso rfl) (by tidy) }
 
-instance [is_filtered C] : is_filtered (ulift_hom C) :=
-is_filtered.of_equivalence ulift_hom.equiv
-
-instance [is_cofiltered C] : is_cofiltered (ulift_hom C) :=
-is_cofiltered.of_equivalence ulift_hom.equiv
-
 end ulift_hom
 
 /-- `as_small C` is a small category equivalent to `C`.
@@ -170,12 +158,6 @@ def as_small.equiv : C ≌ as_small C :=
 
 instance [inhabited C] : inhabited (as_small C) := ⟨⟨arbitrary _⟩⟩
 
-instance [is_filtered C] : is_filtered (as_small C) :=
-is_filtered.of_equivalence as_small.equiv
-
-instance [is_cofiltered C] : is_cofiltered (as_small C) :=
-is_cofiltered.of_equivalence as_small.equiv
-
 /-- The equivalence between `C` and `ulift_hom (ulift C)`. -/
 def {v' u' v u} ulift_hom_ulift_category.equiv (C : Type u) [category.{v} C] :
   C ≌ ulift_hom.{v'} (ulift.{u'} C) :=

src/category_theory/filtered.lean

@@ -7,6 +7,7 @@ import category_theory.fin_category
 import category_theory.limits.cones
 import category_theory.adjunction.basic
 import category_theory.category.preorder
+import category_theory.category.ulift
 import order.bounded_order
 
 /-!
@@ -50,7 +51,7 @@ commute with finite limits.
 
 open function
 
-universes v v₁ u u₁-- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v v₁ u u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
 namespace category_theory
 
@@ -712,4 +713,26 @@ instance is_filtered_op_of_is_cofiltered [is_cofiltered C] : is_filtered Cᵒᵖ
 
 end opposite
 
+section ulift
+
+instance [is_filtered C] : is_filtered (ulift.{u₂} C) :=
+is_filtered.of_equivalence ulift.equivalence
+
+instance [is_cofiltered C] : is_cofiltered (ulift.{u₂} C) :=
+is_cofiltered.of_equivalence ulift.equivalence
+
+instance [is_filtered C] : is_filtered (ulift_hom C) :=
+is_filtered.of_equivalence ulift_hom.equiv
+
+instance [is_cofiltered C] : is_cofiltered (ulift_hom C) :=
+is_cofiltered.of_equivalence ulift_hom.equiv
+
+instance [is_filtered C] : is_filtered (as_small C) :=
+is_filtered.of_equivalence as_small.equiv
+
+instance [is_cofiltered C] : is_cofiltered (as_small C) :=
+is_cofiltered.of_equivalence as_small.equiv
+
+end ulift
+
 end category_theory