feat(category_theory/limits/preserves): preserving binary products (#…

…5061)

This moves and re-does my old file about preserving binary products to match the new API and framework for preservation of special shapes, and also cleans up some existing API. 
(I can split this up if necessary but they're all pretty minor changes, so hope this is okay!)

src/category_theory/closed/cartesian.lean

@@ -5,7 +5,7 @@ Authors: Bhavik Mehta, Edward Ayers, Thomas Read
 -/
 
 import category_theory.limits.shapes.finite_products
-import category_theory.limits.shapes.constructions.preserve_binary_products
+import category_theory.limits.preserves.shapes.binary_products
 import category_theory.closed.monoidal
 import category_theory.monoidal.of_has_finite_products
 import category_theory.adjunction
@@ -389,9 +389,12 @@ lemma exp_comparison_natural_left (A A' B : C) (f : A' ⟶ A) :
 begin
   rw [exp_comparison, exp_comparison, ← curry_natural_left, eq_curry_iff, uncurry_natural_left,
        pre, uncurry_curry, prod.map_swap_assoc, curry_eq, prod.map_id_comp, assoc, ev_naturality],
-  erw [ev_coev_assoc, ← F.map_id, ← prod_comparison_inv_natural_assoc,
-       ← F.map_id, ← prod_comparison_inv_natural_assoc, ← F.map_comp, ← F.map_comp, pre, curry_eq,
-       prod.map_id_comp, assoc, (ev _).naturality, ev_coev_assoc], refl,
+  dsimp only [prod.functor_obj_obj],
+  rw [ev_coev_assoc, ← F.map_id, ← F.map_id, ← prod_comparison_inv_natural_assoc,
+      ← prod_comparison_inv_natural_assoc, ← F.map_comp, ← F.map_comp, pre, curry_eq,
+      prod.map_id_comp, assoc, ev_naturality],
+  dsimp only [prod.functor_obj_obj],
+  rw ev_coev_assoc,
 end
 
 /-- The exponential comparison map is natural in its right argument. -/

src/category_theory/limits/preserves/functor_category.lean

@@ -5,7 +5,7 @@ Authors: Bhavik Mehta
 -/
 import category_theory.limits.presheaf
 import category_theory.limits.functor_category
-import category_theory.limits.shapes.constructions.preserve_binary_products
+import category_theory.limits.preserves.shapes.binary_products
 
 /-!
 # Preservation of (co)limits in the functor category

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

@@ -0,0 +1,100 @@
+/-
+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.binary_products
+import category_theory.limits.preserves.basic
+
+/-!
+# Preserving binary products
+
+Constructions to relate the notions of preserving binary products and reflecting binary products
+to concrete binary fans.
+
+In particular, we show that `prod_comparison G X Y` is an isomorphism iff `G` preserves
+the product of `X` and `Y`.
+-/
+
+noncomputable theory
+
+universes v u₁ u₂
+
+open category_theory category_theory.category category_theory.limits
+
+variables {C : Type u₁} [category.{v} C]
+variables {D : Type u₂} [category.{v} D]
+variables (G : C ⥤ D)
+
+namespace category_theory.limits
+
+variables {P X Y Z : C} (f : P ⟶ X) (g : P ⟶ Y)
+
+/--
+The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This
+essentially lets us commute `binary_fan.mk` with `functor.map_cone`.
+-/
+def is_limit_map_cone_binary_fan_equiv :
+  is_limit (G.map_cone (binary_fan.mk f g)) ≃ is_limit (binary_fan.mk (G.map f) (G.map g)) :=
+(is_limit.postcompose_hom_equiv (diagram_iso_pair _) _).symm.trans
+  (is_limit.equiv_iso_limit (cones.ext (iso.refl _) (by { rintro (_ | _), tidy })))
+
+/-- The property of preserving products expressed in terms of binary fans. -/
+def map_is_limit_of_preserves_of_is_limit [preserves_limit (pair X Y) G]
+  (l : is_limit (binary_fan.mk f g)) :
+  is_limit (binary_fan.mk (G.map f) (G.map g)) :=
+is_limit_map_cone_binary_fan_equiv G f g (preserves_limit.preserves l)
+
+/-- The property of reflecting products expressed in terms of binary fans. -/
+def is_limit_of_reflects_of_map_is_limit [reflects_limit (pair X Y) G]
+  (l : is_limit (binary_fan.mk (G.map f) (G.map g))) :
+  is_limit (binary_fan.mk f g) :=
+reflects_limit.reflects ((is_limit_map_cone_binary_fan_equiv G f g).symm l)
+
+variables (X Y) [has_binary_product X Y]
+
+/--
+If `G` preserves binary products and `C` has them, then the binary fan constructed of the mapped
+morphisms of the binary product cone is a limit.
+-/
+def is_limit_of_has_binary_product_of_preserves_limit
+  [preserves_limit (pair X Y) G] :
+  is_limit (binary_fan.mk (G.map (limits.prod.fst : X ⨯ Y ⟶ X)) (G.map (limits.prod.snd))) :=
+map_is_limit_of_preserves_of_is_limit G _ _ (prod_is_prod X Y)
+
+variables [has_binary_product (G.obj X) (G.obj Y)]
+
+/--
+If the product comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
+pair of `(X,Y)`.
+-/
+def preserves_pair.of_iso_comparison [i : is_iso (prod_comparison G X Y)] :
+  preserves_limit (pair X Y) G :=
+begin
+  apply preserves_limit_of_preserves_limit_cone (prod_is_prod X Y),
+  apply (is_limit_map_cone_binary_fan_equiv _ _ _).symm _,
+  apply is_limit.of_point_iso (limit.is_limit (pair (G.obj X) (G.obj Y))),
+  apply i,
+end
+
+variables [preserves_limit (pair X Y) G]
+/--
+If `G` preserves the product of `(X,Y)`, then the product comparison map for `G` at `(X,Y)` is
+an isomorphism.
+-/
+def preserves_pair.iso :
+  G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y :=
+is_limit.cone_point_unique_up_to_iso
+  (is_limit_of_has_binary_product_of_preserves_limit G X Y)
+  (limit.is_limit _)
+
+@[simp]
+lemma preserves_pair.iso_hom : (preserves_pair.iso G X Y).hom = prod_comparison G X Y := rfl
+
+instance : is_iso (prod_comparison G X Y) :=
+begin
+  rw ← preserves_pair.iso_hom,
+  apply_instance
+end
+
+end category_theory.limits

src/category_theory/limits/shapes/binary_products.lean

@@ -84,36 +84,32 @@ section
 variables {F G : discrete walking_pair.{v} ⥤ C} (f : F.obj left ⟶ G.obj left) (g : F.obj right ⟶ G.obj right)
 
 /-- The natural transformation between two functors out of the walking pair, specified by its components. -/
-def map_pair : F ⟶ G :=
-{ app := λ j, match j with
-  | left := f
-  | right := g
-  end }
+def map_pair : F ⟶ G := { app := λ j, walking_pair.cases_on j f g }
 
 @[simp] lemma map_pair_left : (map_pair f g).app left = f := rfl
 @[simp] lemma map_pair_right : (map_pair f g).app right = g := rfl
 
 /-- The natural isomorphism between two functors out of the walking pair, specified by its components. -/
-@[simps]
+@[simps {rhs_md := semireducible}]
 def map_pair_iso (f : F.obj left ≅ G.obj left) (g : F.obj right ≅ G.obj right) : F ≅ G :=
-{ hom := map_pair f.hom g.hom,
-  inv := map_pair f.inv g.inv,
-  hom_inv_id' := by { ext ⟨⟩; simp, },
-  inv_hom_id' := by { ext ⟨⟩; simp, } }
+nat_iso.of_components (λ j, walking_pair.cases_on j f g) (by tidy)
+
 end
 
+/-- Every functor out of the walking pair is naturally isomorphic (actually, equal) to a `pair` -/
+@[simps {rhs_md := semireducible}]
+def diagram_iso_pair (F : discrete walking_pair ⥤ C) :
+  F ≅ pair (F.obj walking_pair.left) (F.obj walking_pair.right) :=
+map_pair_iso (iso.refl _) (iso.refl _)
+
 section
 variables {D : Type u} [category.{v} D]
 
 /-- The natural isomorphism between `pair X Y ⋙ F` and `pair (F.obj X) (F.obj Y)`. -/
 def pair_comp (X Y : C) (F : C ⥤ D) : pair X Y ⋙ F ≅ pair (F.obj X) (F.obj Y) :=
-map_pair_iso (eq_to_iso rfl) (eq_to_iso rfl)
-end
+diagram_iso_pair _
 
-/-- Every functor out of the walking pair is naturally isomorphic (actually, equal) to a `pair` -/
-def diagram_iso_pair (F : discrete walking_pair ⥤ C) :
-  F ≅ pair (F.obj walking_pair.left) (F.obj walking_pair.right) :=
-map_pair_iso (eq_to_iso rfl) (eq_to_iso rfl)
+end
 
 /-- A binary fan is just a cone on a diagram indexing a product. -/
 abbreviation binary_fan (X Y : C) := cone (pair X Y)
@@ -222,6 +218,16 @@ colimit.ι (pair X Y) walking_pair.left
 abbreviation coprod.inr {X Y : C} [has_binary_coproduct X Y] : Y ⟶ X ⨿ Y :=
 colimit.ι (pair X Y) walking_pair.right
 
+/-- The binary fan constructed from the projection maps is a limit. -/
+def prod_is_prod (X Y : C) [has_binary_product X Y] :
+  is_limit (binary_fan.mk (prod.fst : X ⨯ Y ⟶ X) prod.snd) :=
+(limit.is_limit _).of_iso_limit (cones.ext (iso.refl _) (by { rintro (_ | _), tidy }))
+
+/-- The binary cofan constructed from the coprojection maps is a colimit. -/
+def coprod_is_coprod {X Y : C} [has_binary_coproduct X Y] :
+  is_colimit (binary_cofan.mk (coprod.inl : X ⟶ X ⨿ Y) coprod.inr) :=
+(colimit.is_colimit _).of_iso_colimit (cocones.ext (iso.refl _) (by { rintro (_ | _), tidy }))
+
 @[ext] lemma prod.hom_ext {W X Y : C} [has_binary_product X Y] {f g : W ⟶ X ⨯ Y}
   (h₁ : f ≫ prod.fst = g ≫ prod.fst) (h₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g :=
 binary_fan.is_limit.hom_ext (limit.is_limit _) h₁ h₂
@@ -702,17 +708,18 @@ nat_iso.of_components (prod.associator _ _) (by tidy)
 end prod_functor
 
 section prod_comparison
-variables {C} [has_binary_products C]
 
-variables {D : Type u₂} [category.{v} D]
+variables {C} {D : Type u₂} [category.{v} D]
 variables (F : C ⥤ D) {A A' B B' : C}
+variables [has_binary_product A B] [has_binary_product A' B']
 variables [has_binary_product (F.obj A) (F.obj B)] [has_binary_product (F.obj A') (F.obj B')]
 /--
 The product comparison morphism.
 
 In `category_theory/limits/preserves` we show this is always an iso iff F preserves binary products.
 -/
-def prod_comparison (F : C ⥤ D) (A B : C) [has_binary_product (F.obj A) (F.obj B)] :
+def prod_comparison (F : C ⥤ D) (A B : C)
+  [has_binary_product A B] [has_binary_product (F.obj A) (F.obj B)] :
   F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B :=
 prod.lift (F.map prod.fst) (F.map prod.snd)