feat(category_theory): remove nearly all universe annotations (#3221)

Due to some recent changes to mathlib (does someone know the relevant versions/commits?) most of the universe annotations `.{v}` and `include 𝒞` statements that were previously needed in the category_theory library are no longer necessary.

This PR removes them!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/category/Algebra/basic.lean

@@ -27,12 +27,12 @@ namespace Algebra
 instance : has_coe_to_sort (Algebra R) :=
 { S := Type u, coe := Algebra.carrier }
 
-instance : category (Algebra.{u} R) :=
+instance : category (Algebra R) :=
 { hom   := λ A B, A →ₐ[R] B,
   id    := λ A, alg_hom.id R A,
   comp  := λ A B C f g, g.comp f }
 
-instance : concrete_category (Algebra.{u} R) :=
+instance : concrete_category (Algebra R) :=
 { forget := { obj := λ R, R, map := λ R S f, (f : R → S) },
   forget_faithful := { } }
 
@@ -88,7 +88,7 @@ namespace category_theory.iso
 
 /-- Build a `alg_equiv` from an isomorphism in the category `Algebra R`. -/
 @[simps]
-def to_alg_equiv {X Y : Algebra.{u} R} (i : X ≅ Y) : X ≃ₐ[R] Y :=
+def to_alg_equiv {X Y : Algebra R} (i : X ≅ Y) : X ≃ₐ[R] Y :=
 { to_fun    := i.hom,
   inv_fun   := i.inv,
   left_inv  := by tidy,

src/algebra/category/CommRing/adjunctions.lean

@@ -23,10 +23,10 @@ namespace CommRing
 open_locale classical
 
 /--
-The free functor `Type u ⥤ CommRing.{u}` sending a type `X` to the multivariable (commutative)
+The free functor `Type u ⥤ CommRing` sending a type `X` to the multivariable (commutative)
 polynomials with variables `x : X`.
 -/
-def free : Type u ⥤ CommRing.{u} :=
+def free : Type u ⥤ CommRing :=
 { obj := λ α, of (mv_polynomial α ℤ),
   -- TODO this should just be `ring_hom.of (rename f)`, but this causes a mysterious deterministic timeout!
   map := λ X Y f, @ring_hom.of _ _ _ _ (rename f) (by apply_instance),

src/algebra/category/CommRing/basic.lean

@@ -174,7 +174,7 @@ end ring_equiv
 namespace category_theory.iso
 
 /-- Build a `ring_equiv` from an isomorphism in the category `Ring`. -/
-def Ring_iso_to_ring_equiv {X Y : Ring.{u}} (i : X ≅ Y) : X ≃+* Y :=
+def Ring_iso_to_ring_equiv {X Y : Ring} (i : X ≅ Y) : X ≃+* Y :=
 { to_fun    := i.hom,
   inv_fun   := i.inv,
   left_inv  := by tidy,
@@ -183,7 +183,7 @@ def Ring_iso_to_ring_equiv {X Y : Ring.{u}} (i : X ≅ Y) : X ≃+* Y :=
   map_mul'  := by tidy }.
 
 /-- Build a `ring_equiv` from an isomorphism in the category `CommRing`. -/
-def CommRing_iso_to_ring_equiv {X Y : CommRing.{u}} (i : X ≅ Y) : X ≃+* Y :=
+def CommRing_iso_to_ring_equiv {X Y : CommRing} (i : X ≅ Y) : X ≃+* Y :=
 { to_fun    := i.hom,
   inv_fun   := i.inv,
   left_inv  := by tidy,

src/algebra/category/CommRing/colimits.lean

@@ -47,9 +47,9 @@ comm_ring.right_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), (
 
 namespace CommRing.colimits
 /-!
-We build the colimit of a diagram in `Mon` by constructing the
-free monoid on the disjoint union of all the monoids in the diagram,
-then taking the quotient by the monoid laws within each monoid,
+We build the colimit of a diagram in `CommRing` by constructing the
+free commutative ring on the disjoint union of all the commutative rings in the diagram,
+then taking the quotient by the commutative ring laws within each commutative ring,
 and the identifications given by the morphisms in the diagram.
 -/
 
@@ -422,7 +422,7 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
     refl
   end }.
 
-instance has_colimits_CommRing : has_colimits.{v} CommRing.{v} :=
+instance has_colimits_CommRing : has_colimits CommRing :=
 { has_colimits_of_shape := λ J 𝒥,
   { has_colimit := λ F, by exactI
     { cocone := colimit_cocone F,

src/algebra/category/CommRing/limits.lean

@@ -25,11 +25,11 @@ namespace CommRing
 
 variables {J : Type u} [small_category J]
 
-instance comm_ring_obj (F : J ⥤ CommRing.{u}) (j) :
+instance comm_ring_obj (F : J ⥤ CommRing) (j) :
   comm_ring ((F ⋙ forget CommRing).obj j) :=
 by { change comm_ring (F.obj j), apply_instance }
 
-instance sections_submonoid (F : J ⥤ CommRing.{u}) :
+instance sections_submonoid (F : J ⥤ CommRing) :
   is_submonoid (F ⋙ forget CommRing).sections :=
 { one_mem := λ j j' f,
   begin
@@ -46,7 +46,7 @@ instance sections_submonoid (F : J ⥤ CommRing.{u}) :
     refl,
   end }
 
-instance sections_add_submonoid (F : J ⥤ CommRing.{u}) :
+instance sections_add_submonoid (F : J ⥤ CommRing) :
   is_add_submonoid (F ⋙ forget CommRing).sections :=
 { zero_mem := λ j j' f,
   begin
@@ -63,7 +63,7 @@ instance sections_add_submonoid (F : J ⥤ CommRing.{u}) :
     refl,
   end }
 
-instance sections_add_subgroup (F : J ⥤ CommRing.{u}) :
+instance sections_add_subgroup (F : J ⥤ CommRing) :
   is_add_subgroup (F ⋙ forget CommRing).sections :=
 { neg_mem := λ a ah j j' f,
   begin
@@ -74,18 +74,18 @@ instance sections_add_subgroup (F : J ⥤ CommRing.{u}) :
   end,
   ..(CommRing.sections_add_submonoid F) }
 
-instance sections_subring (F : J ⥤ CommRing.{u}) :
+instance sections_subring (F : J ⥤ CommRing) :
   is_subring (F ⋙ forget CommRing).sections :=
 { ..(CommRing.sections_submonoid F),
   ..(CommRing.sections_add_subgroup F) }
 
-instance limit_comm_ring (F : J ⥤ CommRing.{u}) :
+instance limit_comm_ring (F : J ⥤ CommRing) :
   comm_ring (limit (F ⋙ forget CommRing)) :=
 @subtype.comm_ring ((Π (j : J), (F ⋙ forget _).obj j)) (by apply_instance) _
   (by convert (CommRing.sections_subring F))
 
 /-- `limit.π (F ⋙ forget CommRing) j` as a `ring_hom`. -/
-def limit_π_ring_hom (F : J ⥤ CommRing.{u}) (j) :
+def limit_π_ring_hom (F : J ⥤ CommRing) (j) :
   limit (F ⋙ forget CommRing) →+* (F ⋙ forget CommRing).obj j :=
 { to_fun := limit.π (F ⋙ forget CommRing) j,
   map_one' := by { simp only [types.types_limit_π], refl },
@@ -102,7 +102,7 @@ namespace CommRing_has_limits
 Construction of a limit cone in `CommRing`.
 (Internal use only; use the limits API.)
 -/
-def limit (F : J ⥤ CommRing.{u}) : cone F :=
+def limit (F : J ⥤ CommRing) : cone F :=
 { X := ⟨limit (F ⋙ forget _), by apply_instance⟩,
   π :=
   { app := limit_π_ring_hom F,
@@ -113,7 +113,7 @@ def limit (F : J ⥤ CommRing.{u}) : cone F :=
 Witness that the limit cone in `CommRing` is a limit cone.
 (Internal use only; use the limits API.)
 -/
-def limit_is_limit (F : J ⥤ CommRing.{u}) : is_limit (limit F) :=
+def limit_is_limit (F : J ⥤ CommRing) : is_limit (limit F) :=
 begin
   refine is_limit.of_faithful
     (forget CommRing) (limit.is_limit _)
@@ -128,7 +128,7 @@ end CommRing_has_limits
 open CommRing_has_limits
 
 /-- The category of commutative rings has all limits. -/
-instance CommRing_has_limits : has_limits.{u} CommRing.{u} :=
+instance CommRing_has_limits : has_limits CommRing :=
 { has_limits_of_shape := λ J 𝒥,
   { has_limit := λ F, by exactI
     { cone     := limit F,
@@ -138,7 +138,7 @@ instance CommRing_has_limits : has_limits.{u} CommRing.{u} :=
 The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying
 types could have been computed instead as limits in the category of types.)
 -/
-instance forget_preserves_limits : preserves_limits (forget CommRing.{u}) :=
+instance forget_preserves_limits : preserves_limits (forget CommRing) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ F,
     by exactI preserves_limit_of_preserves_limit_cone

src/algebra/category/Group/adjunctions.lean

@@ -22,10 +22,10 @@ namespace AddCommGroup
 open_locale classical
 
 /--
-The free functor `Type u ⥤ AddCommGroup.{u}` sending a type `X` to the
+The free functor `Type u ⥤ AddCommGroup` sending a type `X` to the
 free abelian group with generators `x : X`.
 -/
-def free : Type u ⥤ AddCommGroup.{u} :=
+def free : Type u ⥤ AddCommGroup :=
 { obj := λ α, of (free_abelian_group α),
   map := λ X Y f, add_monoid_hom.of (λ x : free_abelian_group X, f <$> x),
   map_id' := λ X, add_monoid_hom.ext $ by simp [types_id],

src/algebra/category/Group/basic.lean

@@ -58,7 +58,7 @@ instance : has_one Group := ⟨Group.of punit⟩
 instance : inhabited Group := ⟨1⟩
 
 @[to_additive]
-instance : unique (1 : Group.{u}) :=
+instance : unique (1 : Group) :=
 { default := 1,
   uniq := λ a, begin cases a, refl, end }
 
@@ -116,7 +116,7 @@ instance comm_group_instance (G : CommGroup) : comm_group G := G.str
 @[to_additive] instance : inhabited CommGroup := ⟨1⟩
 
 @[to_additive]
-instance : unique (1 : CommGroup.{u}) :=
+instance : unique (1 : CommGroup) :=
 { default := 1,
   uniq := λ a, begin cases a, refl, end }
 
@@ -156,8 +156,9 @@ namespace AddCommGroup
 
 /-- Any element of an abelian group gives a unique morphism from `ℤ` sending
 `1` to that element. -/
--- TODO allow other universe levels
--- this will require writing a `ulift_instances.lean` file
+-- Note that because `ℤ : Type 0`, this forces `G : AddCommGroup.{0}`,
+-- so we write this explicitly to be clear.
+-- TODO generalize this, requiring a `ulift_instances.lean` file
 def as_hom {G : AddCommGroup.{0}} (g : G) : (AddCommGroup.of ℤ) ⟶ G :=
 gmultiples_hom G g
 
@@ -219,7 +220,7 @@ namespace category_theory.iso
 /-- Build a `mul_equiv` from an isomorphism in the category `Group`. -/
 @[to_additive AddGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism in the category
 `AddGroup`."]
-def Group_iso_to_mul_equiv {X Y : Group.{u}} (i : X ≅ Y) : X ≃* Y :=
+def Group_iso_to_mul_equiv {X Y : Group} (i : X ≅ Y) : X ≃* Y :=
 { to_fun    := i.hom,
   inv_fun   := i.inv,
   left_inv  := by tidy,
@@ -231,7 +232,7 @@ attribute [simps] Group_iso_to_mul_equiv AddGroup_iso_to_add_equiv
 /-- Build a `mul_equiv` from an isomorphism in the category `CommGroup`. -/
 @[to_additive AddCommGroup_iso_to_add_equiv "Build an `add_equiv` from an isomorphism
 in the category `AddCommGroup`."]
-def CommGroup_iso_to_mul_equiv {X Y : CommGroup.{u}} (i : X ≅ Y) : X ≃* Y :=
+def CommGroup_iso_to_mul_equiv {X Y : CommGroup} (i : X ≅ Y) : X ≃* Y :=
 { to_fun    := i.hom,
   inv_fun   := i.inv,
   left_inv  := by tidy,

src/algebra/category/Group/biproducts.lean

@@ -21,7 +21,7 @@ universe u
 
 namespace AddCommGroup
 
-instance has_limit_pair (G H : AddCommGroup.{u}) : has_limit.{u} (pair G H) :=
+instance has_binary_product (G H : AddCommGroup.{u}) : has_binary_product G H :=
 { cone :=
   { X := AddCommGroup.of (G × H),
     π := { app := λ j, walking_pair.cases_on j (add_monoid_hom.fst G H) (add_monoid_hom.snd G H) }},
@@ -33,15 +33,15 @@ instance has_limit_pair (G H : AddCommGroup.{u}) : has_limit.{u} (pair G H) :=
       ext; [rw ← w walking_pair.left, rw ← w walking_pair.right]; refl,
     end, } }
 
-instance (G H : AddCommGroup.{u}) : has_binary_biproduct.{u} G H :=
+instance (G H : AddCommGroup.{u}) : has_binary_biproduct G H :=
 has_binary_biproduct.of_has_binary_product _ _
 
 -- We verify that the underlying type of the biproduct we've just defined is definitionally
 -- the cartesian product of the underlying types:
-example (G H : AddCommGroup.{u}) : ((G ⊞ H : AddCommGroup.{u}) : Type u) = (G × H) := rfl
+example (G H : AddCommGroup.{u}) : ((G ⊞ H : AddCommGroup) : Type u) = (G × H) := rfl
 
 -- Furthermore, our biproduct will automatically function as a coproduct.
-example (G H : AddCommGroup.{u}) : has_colimit.{u} (pair G H) := by apply_instance
+example (G H : AddCommGroup.{u}) : has_colimit (pair G H) := by apply_instance
 
 variables {J : Type u} (F : (discrete J) ⥤ AddCommGroup.{u})
 
@@ -156,6 +156,6 @@ instance (f : J → AddCommGroup.{u}) : has_biproduct f :=
 
 -- We verify that the underlying type of the biproduct we've just defined is definitionally
 -- the dependent function type:
-example (f : J → AddCommGroup.{u}) : ((⨁ f : AddCommGroup.{u}) : Type u) = (Π j, f j) := rfl
+example (f : J → AddCommGroup.{u}) : ((⨁ f : AddCommGroup) : Type u) = (Π j, f j) := rfl
 
 end AddCommGroup

src/algebra/category/Group/colimits.lean

@@ -283,7 +283,7 @@ def colimit_is_colimit : is_colimit (colimit_cocone F) :=
     refl
   end }.
 
-instance has_colimits_AddCommGroup : has_colimits.{v} AddCommGroup.{v} :=
+instance has_colimits_AddCommGroup : has_colimits AddCommGroup :=
 { has_colimits_of_shape := λ J 𝒥,
   { has_colimit := λ F, by exactI
     { cocone := colimit_cocone F,

src/algebra/category/Group/images.lean

@@ -16,6 +16,8 @@ universe u
 
 namespace AddCommGroup
 
+-- Note that because `injective_of_mono` is currently only proved in `Type 0`,
+-- we restrict to the lowest universe here for now.
 variables {G H : AddCommGroup.{0}} (f : G ⟶ H)
 
 local attribute [ext] subtype.ext_val

src/algebra/category/Group/limits.lean

@@ -28,11 +28,11 @@ namespace AddCommGroup
 
 variables {J : Type u} [small_category J]
 
-instance add_comm_group_obj (F : J ⥤ AddCommGroup.{u}) (j) :
+instance add_comm_group_obj (F : J ⥤ AddCommGroup) (j) :
   add_comm_group ((F ⋙ forget AddCommGroup).obj j) :=
 by { change add_comm_group (F.obj j), apply_instance }
 
-instance sections_add_submonoid (F : J ⥤ AddCommGroup.{u}) :
+instance sections_add_submonoid (F : J ⥤ AddCommGroup) :
   is_add_submonoid (F ⋙ forget AddCommGroup).sections :=
 { zero_mem := λ j j' f,
   begin
@@ -49,7 +49,7 @@ instance sections_add_submonoid (F : J ⥤ AddCommGroup.{u}) :
     refl,
   end }
 
-instance sections_add_subgroup (F : J ⥤ AddCommGroup.{u}) :
+instance sections_add_subgroup (F : J ⥤ AddCommGroup) :
   is_add_subgroup (F ⋙ forget AddCommGroup).sections :=
 { neg_mem := λ a ah j j' f,
   begin
@@ -60,13 +60,13 @@ instance sections_add_subgroup (F : J ⥤ AddCommGroup.{u}) :
   end,
   ..(AddCommGroup.sections_add_submonoid F) }
 
-instance limit_add_comm_group (F : J ⥤ AddCommGroup.{u}) :
+instance limit_add_comm_group (F : J ⥤ AddCommGroup) :
   add_comm_group (limit (F ⋙ forget AddCommGroup)) :=
 @subtype.add_comm_group ((Π (j : J), (F ⋙ forget _).obj j)) (by apply_instance) _
   (by convert (AddCommGroup.sections_add_subgroup F))
 
 /-- `limit.π (F ⋙ forget AddCommGroup) j` as a `add_monoid_hom`. -/
-def limit_π_add_monoid_hom (F : J ⥤ AddCommGroup.{u}) (j) :
+def limit_π_add_monoid_hom (F : J ⥤ AddCommGroup) (j) :
   limit (F ⋙ forget AddCommGroup) →+ (F ⋙ forget AddCommGroup).obj j :=
 { to_fun := limit.π (F ⋙ forget AddCommGroup) j,
   map_zero' := by { simp only [types.types_limit_π], refl },
@@ -81,7 +81,7 @@ namespace AddCommGroup_has_limits
 Construction of a limit cone in `AddCommGroup`.
 (Internal use only; use the limits API.)
 -/
-def limit (F : J ⥤ AddCommGroup.{u}) : cone F :=
+def limit (F : J ⥤ AddCommGroup) : cone F :=
 { X := ⟨limit (F ⋙ forget _), by apply_instance⟩,
   π :=
   { app := limit_π_add_monoid_hom F,
@@ -92,7 +92,7 @@ def limit (F : J ⥤ AddCommGroup.{u}) : cone F :=
 Witness that the limit cone in `AddCommGroup` is a limit cone.
 (Internal use only; use the limits API.)
 -/
-def limit_is_limit (F : J ⥤ AddCommGroup.{u}) : is_limit (limit F) :=
+def limit_is_limit (F : J ⥤ AddCommGroup) : is_limit (limit F) :=
 begin
   refine is_limit.of_faithful
     (forget AddCommGroup) (limit.is_limit _)
@@ -107,7 +107,7 @@ end AddCommGroup_has_limits
 open AddCommGroup_has_limits
 
 /-- The category of abelian groups has all limits. -/
-instance AddCommGroup_has_limits : has_limits.{u} AddCommGroup.{u} :=
+instance AddCommGroup_has_limits : has_limits AddCommGroup :=
 { has_limits_of_shape := λ J 𝒥,
   { has_limit := λ F, by exactI
     { cone     := limit F,
@@ -117,7 +117,7 @@ instance AddCommGroup_has_limits : has_limits.{u} AddCommGroup.{u} :=
 The forgetful functor from abelian groups to types preserves all limits. (That is, the underlying
 types could have been computed instead as limits in the category of types.)
 -/
-instance forget_preserves_limits : preserves_limits (forget AddCommGroup.{u}) :=
+instance forget_preserves_limits : preserves_limits (forget AddCommGroup) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ F,
     by exactI preserves_limit_of_preserves_limit_cone

src/algebra/category/Group/preadditive.lean

@@ -16,7 +16,7 @@ universe u
 
 namespace AddCommGroup
 
-instance : preadditive.{u} AddCommGroup.{u} :=
+instance : preadditive AddCommGroup :=
 { add_comp' := λ P Q R f f' g,
     show (f + f') ≫ g = f ≫ g + f' ≫ g, by { ext, simp },
   comp_add' := λ P Q R f g g',

src/algebra/category/Group/zero.lean

@@ -20,7 +20,7 @@ universe u
 
 namespace AddCommGroup
 
-instance : has_zero_object.{u} AddCommGroup.{u} :=
+instance : has_zero_object AddCommGroup :=
 { zero := 0,
   unique_to := λ X, ⟨⟨0⟩, λ f, begin ext, cases x, erw add_monoid_hom.map_zero, refl end⟩,
   unique_from := λ X, ⟨⟨0⟩, λ f, begin ext, apply subsingleton.elim, end⟩, }