refactor(category_theory/finite_limits): reorganise import hierarchy (#…

…3320)

Previously, all of the "special shapes" that happened to be finite imported `category_theory.limits.shapes.finite_limits`. Now it's the other way round, which I think ends up being cleaner.

This also results in some significant reductions to the dependency graph (e.g. talking about homology of complexes no longer requires compiling `data.fintype.basic` and all its antecedents).

No actual content, just moving content around.



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

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -2,7 +2,7 @@ import topology.category.Top.limits
 import category_theory.limits.shapes
 import topology.instances.real
 
-/- This file contains some demos of using the (co)limits API to do topology. -/
+/-! This file contains some demos of using the (co)limits API to do topology. -/
 
 noncomputable theory
 
@@ -18,10 +18,10 @@ section MappingCylinder
 def to_pt (X : Top) : X ⟶ pt :=
 { val := λ _, unit.star, property := continuous_const }
 def I₀ : pt ⟶ I :=
-{ val := λ _, ⟨(0 : ℝ), begin rw [set.left_mem_Icc], norm_num, end⟩,
+{ val := λ _, ⟨(0 : ℝ), by norm_num [set.left_mem_Icc]⟩,
   property := continuous_const }
 def I₁ : pt ⟶ I :=
-{ val := λ _, ⟨(1 : ℝ), begin rw [set.right_mem_Icc], norm_num, end⟩,
+{ val := λ _, ⟨(1 : ℝ), by norm_num [set.right_mem_Icc]⟩,
   property := continuous_const }
 
 def cylinder (X : Top) : Top := prod X I
@@ -90,15 +90,18 @@ section Products
 /-- The countably infinite product of copies of `ℝ`. -/
 def Y : Top := ∏ (λ n : ℕ, R)
 
-/-- We define a point of this infinite product by specifying its coordinates. -/
+/--
+We can define a point in this infinite product by specifying its coordinates.
+Let's define the point whose `n`-th coordinate is `n + 1` (as a real number).
+-/
 def q : pt ⟶ Y :=
-pi.lift (λ (n : ℕ), ⟨λ (_ : pt), (n : ℝ), continuous_const⟩)
+pi.lift (λ (n : ℕ), ⟨λ (_ : pt), (n + 1 : ℝ), continuous_const⟩)
 
 -- "Looking under the hood", we see that `q` is a `subtype`, whose `val` is a function `unit → Y.α`.
 -- #check q.val -- q.val : pt.α → Y.α
--- `q.property` is the fact this function is continous (i.e. no content)
+-- `q.property` is the fact this function is continuous (i.e. no content, since `pt` is a singleton)
 
 -- We can check that this function is definitionally just the function we specified.
-example : (q.val ()).val (57 : ℕ) = ((57 : ℕ) : ℝ) := rfl
+example : (q.val ()).val (9 : ℕ) = ((10 : ℕ) : ℝ) := rfl
 
 end Products

docs/tutorial/category_theory/intro.lean

@@ -11,11 +11,6 @@ We cover how the basic theory of categories, functors and natural transformation
 Most of the below is not hard to read off from the files `category_theory/category.lean`,
 `category_theory/functor.lean` and `category_theory/natural_transformation.lean`.
 
-First a word of warning. In `mathlib`, in the `/src` directory, there is a subdirectory called
-`category`. This is *not* where categories, in the sense of mathematics, are defined; it's for use
-by computer scientists. The directory we will be concerned with here is the `category_theory`
-subdirectory.
-
 ## Overview
 
 A category is a collection of objects, and a collection of morphisms (also known as arrows) between

src/algebra/homology/chain_complex.lean

@@ -3,6 +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 data.int.basic
 import category_theory.graded_object
 import category_theory.differential_object
 

src/category_theory/abelian/non_preadditive.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.finite_products
 import category_theory.limits.shapes.kernels
 import category_theory.limits.shapes.pullbacks
 import category_theory.limits.shapes.regular_mono

src/category_theory/closed/cartesian.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Edward Ayers, Thomas Read
 -/
 
-import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.finite_products
 import category_theory.limits.shapes.constructions.preserve_binary_products
 import category_theory.closed.monoidal
 import category_theory.monoidal.of_has_finite_products

src/category_theory/connected.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import data.list.chain
 import category_theory.const
 import category_theory.discrete_category
 import category_theory.eq_to_hom

src/category_theory/discrete_category.lean

@@ -3,8 +3,6 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
-import data.ulift
-import data.fintype.basic
 import category_theory.eq_to_hom
 
 namespace category_theory
@@ -29,12 +27,6 @@ variables {α : Type u₁}
 instance [inhabited α] : inhabited (discrete α) :=
 by { dsimp [discrete], apply_instance }
 
-instance [fintype α] : fintype (discrete α) :=
-by { dsimp [discrete], apply_instance }
-
-instance fintype_fun [decidable_eq α] (X Y : discrete α) : fintype (X ⟶ Y) :=
-by { apply ulift.fintype }
-
 instance [subsingleton α] : subsingleton (discrete α) :=
 by { dsimp [discrete], apply_instance }
 

src/category_theory/limits/lattice.lean

@@ -3,8 +3,7 @@ Copyright (c) 2019 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.shapes.finite_products
+import category_theory.limits.shapes.finite_limits
 import order.complete_lattice
 
 universes u

src/category_theory/limits/shapes/binary_products.lean

@@ -3,7 +3,8 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Bhavik Mehta
 -/
-import category_theory.limits.shapes.terminal
+import category_theory.limits.limits
+import category_theory.discrete_category
 
 /-!
 # Binary (co)products
@@ -34,10 +35,6 @@ inductive walking_pair : Type v
 
 open walking_pair
 
-instance fintype_walking_pair : fintype walking_pair :=
-{ elems := {left, right},
-  complete := λ x, by { cases x; simp } }
-
 /--
 The equivalence swapping left and right.
 -/
@@ -414,13 +411,6 @@ class has_binary_coproducts :=
 
 attribute [instance] has_binary_products.has_limits_of_shape has_binary_coproducts.has_colimits_of_shape
 
-@[priority 200] -- see Note [lower instance priority]
-instance [has_finite_products C] : has_binary_products.{v} C :=
-{ has_limits_of_shape := by apply_instance }
-@[priority 200] -- see Note [lower instance priority]
-instance [has_finite_coproducts C] : has_binary_coproducts.{v} C :=
-{ has_colimits_of_shape := by apply_instance }
-
 /-- If `C` has all limits of diagrams `pair X Y`, then it has all binary products -/
 def has_binary_products_of_has_limit_pair [Π {X Y : C}, has_limit (pair X Y)] :
   has_binary_products C :=
@@ -431,10 +421,8 @@ def has_binary_coproducts_of_has_colimit_pair [Π {X Y : C}, has_colimit (pair X
   has_binary_coproducts C :=
 { has_colimits_of_shape := { has_colimit := λ F, has_colimit_of_iso (diagram_iso_pair F) } }
 
-section
-
+section prod_functor
 variables {C} [has_binary_products C]
-variables {D : Type u₂} [category.{v} D] [has_binary_products D]
 
 -- FIXME deterministic timeout with `-T50000`
 /-- The binary product functor. -/
@@ -443,54 +431,12 @@ def prod_functor : C ⥤ C ⥤ C :=
 { obj := λ X, { obj := λ Y, X ⨯ Y, map := λ Y Z, prod.map (𝟙 X) },
   map := λ Y Z f, { app := λ T, prod.map f (𝟙 T) }}
 
-/-- The braiding isomorphism which swaps a binary product. -/
-@[simps] def prod.braiding (P Q : C) : P ⨯ Q ≅ Q ⨯ P :=
-{ hom := prod.lift prod.snd prod.fst,
-  inv := prod.lift prod.snd prod.fst }
-
-/-- The braiding isomorphism can be passed through a map by swapping the order. -/
-@[reassoc] lemma braid_natural {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
-  prod.map f g ≫ (prod.braiding _ _).hom = (prod.braiding _ _).hom ≫ prod.map g f :=
-by tidy
-
-@[simp, reassoc] lemma prod.symmetry' (P Q : C) :
-  prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q) :=
-by tidy
+end prod_functor
 
-/-- The braiding isomorphism is symmetric. -/
-@[reassoc] lemma prod.symmetry (P Q : C) :
-  (prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _ :=
-by simp
-
-/-- The associator isomorphism for binary products. -/
-@[simps] def prod.associator
-  (P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ (Q ⨯ R) :=
-{ hom :=
-  prod.lift
-    (prod.fst ≫ prod.fst)
-    (prod.lift (prod.fst ≫ prod.snd) prod.snd),
-  inv :=
-  prod.lift
-    (prod.lift prod.fst (prod.snd ≫ prod.fst))
-    (prod.snd ≫ prod.snd) }
-
-/-- The product functor can be decomposed. -/
-def prod_functor_left_comp (X Y : C) :
-  prod_functor.obj (X ⨯ Y) ≅ prod_functor.obj Y ⋙ prod_functor.obj X :=
-nat_iso.of_components (prod.associator _ _) (by tidy)
-
-@[reassoc]
-lemma prod.pentagon (W X Y Z : C) :
-  prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
-      (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
-    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
-by tidy
+section prod_comparison
+variables {C} [has_binary_products C]
 
-@[reassoc]
-lemma prod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
-  prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
-    (prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃) :=
-by tidy
+variables {D : Type u₂} [category.{v} D] [has_binary_products D]
 
 /--
 The product comparison morphism.
@@ -536,106 +482,6 @@ lemma prod_comparison_inv_natural (F : C ⥤ D) {A A' B B' : C} (f : A ⟶ A') (
 by { erw [(as_iso (prod_comparison F A' B')).eq_comp_inv, category.assoc,
     (as_iso (prod_comparison F A B)).inv_comp_eq, prod_comparison_natural], refl }
 
-variables [has_terminal C]
-
-/-- The left unitor isomorphism for binary products with the terminal object. -/
-@[simps] def prod.left_unitor
-  (P : C) : ⊤_ C ⨯ P ≅ P :=
-{ hom := prod.snd,
-  inv := prod.lift (terminal.from P) (𝟙 _) }
-
-/-- The right unitor isomorphism for binary products with the terminal object. -/
-@[simps] def prod.right_unitor
-  (P : C) : P ⨯ ⊤_ C ≅ P :=
-{ hom := prod.fst,
-  inv := prod.lift (𝟙 _) (terminal.from P) }
-
-@[reassoc]
-lemma prod_left_unitor_hom_naturality (f : X ⟶ Y):
-  prod.map (𝟙 _) f ≫ (prod.left_unitor Y).hom = (prod.left_unitor X).hom ≫ f :=
-prod.map_snd _ _
-
-@[reassoc]
-lemma prod_left_unitor_inv_naturality (f : X ⟶ Y):
-  (prod.left_unitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.left_unitor Y).inv :=
-by rw [iso.inv_comp_eq, ← category.assoc, iso.eq_comp_inv, prod_left_unitor_hom_naturality]
-
-@[reassoc]
-lemma prod_right_unitor_hom_naturality (f : X ⟶ Y):
-  prod.map f (𝟙 _) ≫ (prod.right_unitor Y).hom = (prod.right_unitor X).hom ≫ f :=
-prod.map_fst _ _
-
-@[reassoc]
-lemma prod_right_unitor_inv_naturality (f : X ⟶ Y):
-  (prod.right_unitor X).inv ≫ prod.map f (𝟙 _) = f ≫ (prod.right_unitor Y).inv :=
-by rw [iso.inv_comp_eq, ← category.assoc, iso.eq_comp_inv, prod_right_unitor_hom_naturality]
-
-lemma prod.triangle (X Y : C) :
-  (prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) ((prod.left_unitor Y).hom) =
-    prod.map ((prod.right_unitor X).hom) (𝟙 Y) :=
-by tidy
-
-end
-
-section
-variables {C} [has_binary_coproducts C]
-
-/-- The braiding isomorphism which swaps a binary coproduct. -/
-@[simps] def coprod.braiding (P Q : C) : P ⨿ Q ≅ Q ⨿ P :=
-{ hom := coprod.desc coprod.inr coprod.inl,
-  inv := coprod.desc coprod.inr coprod.inl }
-
-@[simp] lemma coprod.symmetry' (P Q : C) :
-  coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q) :=
-by tidy
-
-/-- The braiding isomorphism is symmetric. -/
-lemma coprod.symmetry (P Q : C) :
-  (coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _ :=
-by simp
-
-/-- The associator isomorphism for binary coproducts. -/
-@[simps] def coprod.associator
-  (P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ (Q ⨿ R) :=
-{ hom :=
-  coprod.desc
-    (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr))
-    (coprod.inr ≫ coprod.inr),
-  inv :=
-  coprod.desc
-    (coprod.inl ≫ coprod.inl)
-    (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) }
-
-lemma coprod.pentagon (W X Y Z : C) :
-  coprod.map ((coprod.associator W X Y).hom) (𝟙 Z) ≫
-      (coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) =
-    (coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom :=
-by tidy
-
-lemma coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
-  coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
-    (coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃) :=
-by tidy
-
-variables [has_initial C]
-
-/-- The left unitor isomorphism for binary coproducts with the initial object. -/
-@[simps] def coprod.left_unitor
-  (P : C) : ⊥_ C ⨿ P ≅ P :=
-{ hom := coprod.desc (initial.to P) (𝟙 _),
-  inv := coprod.inr }
-
-/-- The right unitor isomorphism for binary coproducts with the initial object. -/
-@[simps] def coprod.right_unitor
-  (P : C) : P ⨿ ⊥_ C ≅ P :=
-{ hom := coprod.desc (𝟙 _) (initial.to P),
-  inv := coprod.inl }
-
-lemma coprod.triangle (X Y : C) :
-  (coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) ((coprod.left_unitor Y).hom) =
-    coprod.map ((coprod.right_unitor X).hom) (𝟙 Y) :=
-by tidy
-
-end
+end prod_comparison
 
 end category_theory.limits

src/category_theory/limits/shapes/biproducts.lean

@@ -4,14 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.epi_mono
+import category_theory.limits.shapes.finite_products
 import category_theory.limits.shapes.binary_products
 import category_theory.preadditive
 import algebra.big_operators
 
 /-!
 # Biproducts and binary biproducts
 
-We introduce the notion of biproducts and binary biproducts.
+We introduce the notion of (finite) biproducts and binary biproducts.
 
 These are slightly unusual relative to the other shapes in the library,
 as they are simultaneously limits and colimits.

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

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import category_theory.limits.shapes.terminal
 import category_theory.limits.shapes.pullbacks
 import category_theory.limits.shapes.binary_products
 

src/category_theory/limits/shapes/default.lean

@@ -1,3 +1,12 @@
+import category_theory.limits.shapes.terminal
 import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.products
+import category_theory.limits.shapes.finite_products
+import category_theory.limits.shapes.finite_limits
+import category_theory.limits.shapes.biproducts
+import category_theory.limits.shapes.images
+import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.kernels
 import category_theory.limits.shapes.equalizers
+import category_theory.limits.shapes.wide_pullbacks
 import category_theory.limits.shapes.pullbacks