refactor(category_theory/limits): split file (#6751)

This splits `category_theory.limits.limits` into
`category_theory.limits.is_limit` and `category_theory.limits.has_limits`.

It doesn't meaningfully reduce imports, as everything imports `has_limits`, but in principle it could, and hopefully it makes the content slightly easier to understand when separated.

In any case, the file was certainly too large.



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

Author: kim-em

src/algebra/category/CommRing/colimits.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.CommRing.basic
-import category_theory.limits.limits
+import category_theory.limits.has_limits
 import category_theory.limits.concrete_category
 
 /-!

src/algebra/category/Group/colimits.lean

@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import algebra.category.Group.preadditive
 import group_theory.quotient_group
-import category_theory.limits.limits
 import category_theory.limits.concrete_category
 import category_theory.limits.shapes.kernels
 import category_theory.limits.shapes.concrete_category

src/algebra/category/Mon/colimits.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.Mon.basic
-import category_theory.limits.limits
+import category_theory.limits.has_limits
 import category_theory.limits.concrete_category
 
 /-!

src/category_theory/limits/concrete_category.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.limits.limits
+import category_theory.limits.has_limits
 import category_theory.concrete_category.basic
 
 /-!

src/category_theory/limits/fubini.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.limits.limits
+import category_theory.limits.has_limits
 import category_theory.products.basic
 import category_theory.currying