chore(category_theory/limits): move constructions folder (#5681)

As mentioned here: #5516 (comment)

The linter is giving new errors, so I might as well fix them in this PR.

src/category_theory/abelian/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 
-import category_theory.limits.shapes.constructions.pullbacks
+import category_theory.limits.constructions.pullbacks
 import category_theory.limits.shapes.biproducts
 import category_theory.limits.shapes.images
 import category_theory.abelian.non_preadditive

src/category_theory/limits/shapes/constructions/binary_products.lean → src/category_theory/limits/constructions/binary_products.lean

@@ -7,8 +7,6 @@ import category_theory.limits.shapes.terminal
 import category_theory.limits.shapes.pullbacks
 import category_theory.limits.shapes.binary_products
 
-universes v u
-
 /-!
 # Constructing binary product from pullbacks and terminal object.
 
@@ -17,6 +15,8 @@ If a category has pullbacks and a terminal object, then it has binary products.
 TODO: provide the dual result.
 -/
 
+universes v u
+
 open category_theory category_theory.category category_theory.limits
 
 /-- Any category with pullbacks and terminal object has binary products. -/

src/category_theory/limits/shapes/constructions/over/connected.lean → src/category_theory/limits/constructions/over/connected.lean

@@ -8,8 +8,10 @@ import category_theory.limits.connected
 import category_theory.limits.creates
 
 /-!
-# `forget : over B ⥤ C` creates connected limits.
+# Connected limits in the over category
 
+Shows that the forgetful functor `over B ⥤ C` creates connected limits, in particular `over B` has
+any connected limit which `C` has.
 -/
 
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
@@ -54,7 +56,8 @@ lemma raised_cone_lowers_to_original [is_connected J] {B : C} {F : J ⥤ over B}
 by tidy
 
 /-- (Impl) Show that the raised cone is a limit. -/
-def raised_cone_is_limit [is_connected J] {B : C} {F : J ⥤ over B} {c : cone (F ⋙ forget B)} (t : is_limit c) :
+def raised_cone_is_limit [is_connected J] {B : C} {F : J ⥤ over B}
+  {c : cone (F ⋙ forget B)} (t : is_limit c) :
   is_limit (raise_cone c) :=
 { lift := λ s, over.hom_mk (t.lift ((forget B).map_cone s)) (by { dsimp, simp }),
   uniq' := λ s m K, by { ext1, apply t.hom_ext, intro j, simp [← K j] } }

src/category_theory/limits/shapes/constructions/over/default.lean → src/category_theory/limits/constructions/over/default.lean

@@ -3,11 +3,17 @@ Copyright (c) 2018 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Reid Barton, Bhavik Mehta
 -/
-import category_theory.limits.shapes.constructions.over.products
-import category_theory.limits.shapes.constructions.over.connected
-import category_theory.limits.shapes.constructions.limits_of_products_and_equalizers
-import category_theory.limits.shapes.constructions.equalizers
+import category_theory.limits.constructions.over.products
+import category_theory.limits.constructions.over.connected
+import category_theory.limits.constructions.limits_of_products_and_equalizers
+import category_theory.limits.constructions.equalizers
 
+/-!
+# Limits in the over category
+
+Declare instances for limits in the over category: If `C` has finite wide pullbacks, `over B` has
+finite limits, and if `C` has arbitrary wide pullbacks then `over B` has limits.
+-/
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
 open category_theory category_theory.limits

src/category_theory/limits/shapes/constructions/over/products.lean → src/category_theory/limits/constructions/over/products.lean

@@ -8,21 +8,33 @@ import category_theory.limits.shapes.pullbacks
 import category_theory.limits.shapes.wide_pullbacks
 import category_theory.limits.shapes.finite_products
 
+/-!
+# Products in the over category
+
+Shows that products in the over category can be derived from wide pullbacks in the base category.
+The main result is `over_product_of_wide_pullback`, which says that if `C` has `J`-indexed wide
+pullbacks, then `over B` has `J`-indexed products.
+-/
 universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
 open category_theory category_theory.limits
 
-variables {J : Type v} [small_category J]
+variables {J : Type v}
 variables {C : Type u} [category.{v} C]
 variable {X : C}
 
 namespace category_theory.over
 
 namespace construct_products
 
-/-- (Impl) Given a product shape in `C/B`, construct the corresponding wide pullback diagram in `C`. -/
+/--
+(Implementation)
+Given a product diagram in `C/B`, construct the corresponding wide pullback diagram
+in `C`.
+-/
 @[reducible]
-def wide_pullback_diagram_of_diagram_over (B : C) {J : Type v} (F : discrete J ⥤ over B) : wide_pullback_shape J ⥤ C :=
+def wide_pullback_diagram_of_diagram_over (B : C) {J : Type v} (F : discrete J ⥤ over B) :
+  wide_pullback_shape J ⥤ C :=
 wide_pullback_shape.wide_cospan B (λ j, (F.obj j).left) (λ j, (F.obj j).hom)
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/
@@ -63,38 +75,43 @@ def cones_equiv_functor (B : C) {J : Type v} (F : discrete J ⥤ over B) :
   cone (wide_pullback_diagram_of_diagram_over B F) ⥤ cone F :=
 { obj := λ c,
   { X := over.mk (c.π.app none),
-    π := { app := λ j, over.hom_mk (c.π.app (some j)) (by apply c.w (wide_pullback_shape.hom.term j)) } },
+    π :=
+    { app := λ j, over.hom_mk (c.π.app (some j))
+                    (by apply c.w (wide_pullback_shape.hom.term j)) } },
   map := λ c₁ c₂ f,
   { hom := over.hom_mk f.hom } }
 
 local attribute [tidy] tactic.case_bash
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simp]
-def cones_equiv_unit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) :
+def cones_equiv_unit_iso (B : C) (F : discrete J ⥤ over B) :
   𝟭 (cone (wide_pullback_diagram_of_diagram_over B F)) ≅
     cones_equiv_functor B F ⋙ cones_equiv_inverse B F :=
 nat_iso.of_components (λ _, cones.ext {hom := 𝟙 _, inv := 𝟙 _} (by tidy)) (by tidy)
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simp]
-def cones_equiv_counit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) :
+def cones_equiv_counit_iso (B : C) (F : discrete J ⥤ over B) :
   cones_equiv_inverse B F ⋙ cones_equiv_functor B F ≅ 𝟭 (cone F) :=
 nat_iso.of_components
   (λ _, cones.ext {hom := over.hom_mk (𝟙 _), inv := over.hom_mk (𝟙 _)} (by tidy)) (by tidy)
 
--- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and `cones.ext`?
-/-- (Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`. -/
+-- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and
+--       `cones.ext`?
+/--
+(Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`.
+-/
 @[simps]
-def cones_equiv (B : C) {J : Type v} (F : discrete J ⥤ over B) :
+def cones_equiv (B : C) (F : discrete J ⥤ over B) :
   cone (wide_pullback_diagram_of_diagram_over B F) ≌ cone F :=
 { functor := cones_equiv_functor B F,
   inverse := cones_equiv_inverse B F,
   unit_iso := cones_equiv_unit_iso B F,
   counit_iso := cones_equiv_counit_iso B F, }
 
 /-- Use the above equivalence to prove we have a limit. -/
-lemma has_over_limit_discrete_of_wide_pullback_limit {B : C} {J : Type v} (F : discrete J ⥤ over B)
+lemma has_over_limit_discrete_of_wide_pullback_limit {B : C} (F : discrete J ⥤ over B)
   [has_limit (wide_pullback_diagram_of_diagram_over B F)] :
   has_limit F :=
 has_limit.mk
@@ -103,7 +120,7 @@ has_limit.mk
     (cones_equiv B F).functor (limit.is_limit (wide_pullback_diagram_of_diagram_over B F)) }
 
 /-- Given a wide pullback in `C`, construct a product in `C/B`. -/
-lemma over_product_of_wide_pullback {J : Type v} [has_limits_of_shape (wide_pullback_shape J) C] {B : C} :
+lemma over_product_of_wide_pullback [has_limits_of_shape (wide_pullback_shape J) C] {B : C} :
   has_limits_of_shape (discrete J) (over B) :=
 { has_limit := λ F, has_over_limit_discrete_of_wide_pullback_limit F }
 

src/category_theory/limits/shapes/constructions/pullbacks.lean → src/category_theory/limits/constructions/pullbacks.lean

@@ -7,15 +7,15 @@ import category_theory.limits.shapes.binary_products
 import category_theory.limits.shapes.equalizers
 import category_theory.limits.shapes.pullbacks
 
-universes v u
-
 /-!
 # Constructing pullbacks from binary products and equalizers
 
 If a category as binary products and equalizers, then it has pullbacks.
 Also, if a category has binary coproducts and coequalizers, then it has pushouts
 -/
 
+universes v u
+
 open category_theory
 
 namespace category_theory.limits

src/order/category/omega_complete_partial_order.lean

@@ -8,7 +8,7 @@ import order.omega_complete_partial_order
 import order.category.Preorder
 import category_theory.limits.shapes.products
 import category_theory.limits.shapes.equalizers
-import category_theory.limits.shapes.constructions.limits_of_products_and_equalizers
+import category_theory.limits.constructions.limits_of_products_and_equalizers
 
 /-!
 # Category of types with a omega complete partial order