[Merged by Bors] - feat(category_theory/limits/preserves/shapes/products): preserve products

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

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2020 Scott Morrison, Bhavik Mehta. 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.products
+import category_theory.limits.preserves.basic
+
+/-!
+# Preserving products
+
+Constructions to relate the notions of preserving products and reflecting products
+to concrete fans.
+
+In particular, we show that `pi_comparison G f` is an isomorphism iff `G` preserves
+the limit of `f`.
+-/
+
+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 preserves
+
+variables {J : Type v} (f : J → C)
+
+/--
+The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This
+essentially lets us commute `fan.mk` with `functor.map_cone`.
+-/
+def fan_map_cone_limit {P : C} (g : Π j, P ⟶ f j) :
+  is_limit (G.map_cone (fan.mk P g)) ≃
+  is_limit (fan.mk _ (λ j, G.map (g j)) : fan (λ j, G.obj (f j))) :=
+begin
+  refine (is_limit.postcompose_hom_equiv _ _).symm.trans (is_limit.equiv_iso_limit _),
+  refine discrete.nat_iso (λ j, iso.refl (G.obj (f j))),
+  refine cones.ext (iso.refl _) (λ j, by { dsimp, simp }),
+end
+
+/-- The property of preserving products expressed in terms of fans. -/
+def map_is_limit_of_preserves_of_is_limit [preserves_limit (discrete.functor f) G]
+  {P : C} (g : Π j, P ⟶ f j) (t : is_limit (fan.mk _ g)) :
+  is_limit (fan.mk _ (λ j, G.map (g j)) : fan (λ j, G.obj (f j))) :=
+fan_map_cone_limit _ _ _ (preserves_limit.preserves t)
+
+/-- The property of reflecting products expressed in terms of fans. -/
+def is_limit_of_reflects_of_map_is_limit [reflects_limit (discrete.functor f) G]
+  {P : C} (g : Π j, P ⟶ f j) (t : is_limit (fan.mk _ (λ j, G.map (g j)) : fan (λ j, G.obj (f j)))) :
+  is_limit (fan.mk P g) :=
+reflects_limit.reflects ((fan_map_cone_limit _ _ _).symm t)
+
+variables [has_product f]
+
+/--
+If `G` preserves products and `C` has them, then the fan constructed of the mapped projection of a
+product is a limit.
+-/
+def is_limit_of_has_product_of_preserves_limit [preserves_limit (discrete.functor f) G] :
+  is_limit (fan.mk _ (λ (j : J), G.map (pi.π f j)) : fan (λ j, G.obj (f j))) :=
+map_is_limit_of_preserves_of_is_limit G f _ (product_is_product _)
+
+variables [has_product (λ (j : J), G.obj (f j))]
+
+/-- If `pi_comparison G f` is an isomorphism, then `G` preserves the limit of `f`. -/
+def preserves_product_of_iso_comparison [i : is_iso (pi_comparison G f)] :
+  preserves_limit (discrete.functor f) G :=
+begin
+  apply preserves_limit_of_preserves_limit_cone (product_is_product f),
+  apply (fan_map_cone_limit _ _ _).symm _,
+  apply is_limit.of_point_iso (limit.is_limit (discrete.functor (λ (j : J), G.obj (f j)))),
+  apply i,
+end
+
+variable [preserves_limit (discrete.functor f) G]
+
+/--
+If `G` preserves limits, we have an isomorphism from the image of a product to the product of the
+images.
+-/
+def preserves_products_iso : G.obj (∏ f) ≅ ∏ (λ j, G.obj (f j)) :=
+is_limit.cone_point_unique_up_to_iso
+  (is_limit_of_has_product_of_preserves_limit G f)
+  (limit.is_limit _)
+
+@[simp]
+lemma preserves_products_iso_hom : (preserves_products_iso G f).hom = pi_comparison G f :=
+rfl
+
+instance : is_iso (pi_comparison G f) :=
+begin
+  rw ← preserves_products_iso_hom,
+  apply_instance,
+end
+
+end preserves

src/category_theory/limits/shapes/products.lean

@@ -71,6 +71,11 @@ limit.π (discrete.functor f) b
 abbreviation sigma.ι (f : β → C) [has_coproduct f] (b : β) : f b ⟶ ∐ f :=
 colimit.ι (discrete.functor f) b
 
+/-- The fan constructed of the projections from the product is limiting. -/
+def product_is_product (f : β → C) [has_product f] :
+  is_limit (fan.mk _ (pi.π f)) :=
+is_limit.of_iso_limit (limit.is_limit (discrete.functor f)) (cones.ext (iso.refl _) (by tidy))
+
 /-- A collection of morphisms `P ⟶ f b` induces a morphism `P ⟶ ∏ f`. -/
 abbreviation pi.lift {f : β → C} [has_product f] {P : C} (p : Π b, P ⟶ f b) : P ⟶ ∏ f :=
 limit.lift _ (fan.mk P p)

src/topology/sheaves/forget.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import topology.sheaves.sheaf
-import category_theory.limits.preserves.shapes
+import category_theory.limits.preserves.shapes.products
 import category_theory.limits.types
 
 /-!
@@ -59,17 +59,19 @@ def diagram_comp_preserves_limits :
 begin
   fapply nat_iso.of_components,
   rintro ⟨j⟩,
-  exact (preserves_products_iso _ _),
-  exact (preserves_products_iso _ _),
+  exact (preserves.preserves_products_iso _ _),
+  exact (preserves.preserves_products_iso _ _),
   rintros ⟨⟩ ⟨⟩ ⟨⟩,
   { ext, simp, dsimp, simp, }, -- non-terminal `simp`, but `squeeze_simp` fails
   { ext,
-    simp only [limit.lift_π, functor.comp_map, parallel_pair_map_left, fan.mk_π_app,
-      map_lift_comp_preserves_products_iso_hom, functor.map_comp, category.assoc],
+    simp only [limit.lift_π, functor.comp_map, map_lift_pi_comparison, fan.mk_π_app,
+               preserves.preserves_products_iso_hom, parallel_pair_map_left, functor.map_comp,
+               category.assoc],
     dsimp, simp, },
   { ext,
     simp only [limit.lift_π, functor.comp_map, parallel_pair_map_right, fan.mk_π_app,
-      map_lift_comp_preserves_products_iso_hom, functor.map_comp, category.assoc],
+               preserves.preserves_products_iso_hom, map_lift_pi_comparison, functor.map_comp,
+               category.assoc],
     dsimp, simp, },
  { ext, simp, dsimp, simp, },
 end
@@ -182,7 +184,7 @@ begin
         ext1 j,
         dsimp,
         simp only [category.assoc, ←functor.map_comp_assoc, equalizer.lift_ι,
-          map_lift_comp_preserves_products_iso_hom_assoc],
+          map_lift_pi_comparison_assoc],
         dsimp [res], simp,
       end,
       -- conclude that it is an isomorphism,