feat(category_theory/limits): preserves biproducts if comparison is i…

…so (#14419)

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

@@ -5,6 +5,8 @@ Authors: Markus Himmel
 -/
 import category_theory.limits.shapes.biproducts
 import category_theory.limits.preserves.shapes.zero
+import category_theory.limits.preserves.shapes.binary_products
+import category_theory.limits.preserves.shapes.products
 
 /-!
 # Preservation of biproducts
@@ -13,7 +15,10 @@ We define the image of a (binary) bicone under a functor that preserves zero mor
 classes `preserves_biproduct` and `preserves_binary_biproduct`. We then
 
 * show that a functor that preserves biproducts of a two-element type preserves binary biproducts,
-* give the canonical isomorphism between the image of a biproduct and the biproduct of the images,
+* construct the comparison morphisms between the image of a biproduct and the biproduct of the
+  images and show that the biproduct is preserved if one of them is an isomorphism,
+* give the canonical isomorphism between the image of a biproduct and the biproduct of the images
+  in case that the biproduct is preserved,
 * show that in a preadditive category, a functor preserves a biproduct if and only if it preserves
   the corresponding product if and only if it preserves the corresponding coproduct.
 
@@ -179,8 +184,53 @@ open category_theory.limits
 namespace functor
 
 section bicone
-variables {J : Type w₁} (F : C ⥤ D) [preserves_zero_morphisms F] (f : J → C)
-  [has_biproduct f] [preserves_biproduct f F]
+variables {J : Type w₁} (F : C ⥤ D) (f : J → C)
+  [has_biproduct f]
+
+section
+variables [has_biproduct (F.obj ∘ f)]
+
+/-- As for products, any functor between categories with biproducts gives rise to a morphism
+    `F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f)`. -/
+def biproduct_comparison : F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f) :=
+biproduct.lift (λ j, F.map (biproduct.π f j))
+
+@[simp, reassoc] lemma biproduct_comparison_π (j : J) :
+  biproduct_comparison F f ≫ biproduct.π _ j = F.map (biproduct.π f j) :=
+biproduct.lift_π _ _
+
+/-- As for coproducts, any functor between categories with biproducts gives rise to a morphism
+    `⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)` -/
+def biproduct_comparison' : ⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f) :=
+biproduct.desc (λ j, F.map (biproduct.ι f j))
+
+@[simp, reassoc] lemma ι_biproduct_comparison' (j : J) :
+  biproduct.ι _ j ≫ biproduct_comparison' F f = F.map (biproduct.ι f j) :=
+biproduct.ι_desc _ _
+
+variables [preserves_zero_morphisms F]
+
+/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
+    the biproduct, see `preserves_biproduct_of_mono_biproduct_comparison`.  -/
+@[simp, reassoc] lemma biproduct_comparison'_comp_biproduct_comparison :
+  biproduct_comparison' F f ≫ biproduct_comparison F f = 𝟙 (⨁ (F.obj ∘ f)) :=
+by { classical, ext, simp [biproduct.ι_π, ← functor.map_comp, eq_to_hom_map] }
+
+instance : split_epi (biproduct_comparison F f) :=
+⟨biproduct_comparison' F f⟩
+
+@[simp] lemma section_biproduct_comparison :
+  section_ (biproduct_comparison F f) = biproduct_comparison' F f := rfl
+
+instance : split_mono (biproduct_comparison' F f) :=
+⟨biproduct_comparison F f⟩
+
+@[simp] lemma retraction_biproduct_comparison' :
+  retraction (biproduct_comparison' F f) = biproduct_comparison F f := rfl
+
+end
+
+variables [preserves_zero_morphisms F] [preserves_biproduct f F]
 
 instance has_biproduct_of_preserves : has_biproduct (F.obj ∘ f) :=
 has_biproduct.mk
@@ -201,8 +251,60 @@ rfl
 
 end bicone
 
-variables (F : C ⥤ D) [preserves_zero_morphisms F] (X Y : C) [has_binary_biproduct X Y]
-  [preserves_binary_biproduct X Y F]
+variables (F : C ⥤ D) (X Y : C) [has_binary_biproduct X Y]
+
+section
+variables [has_binary_biproduct (F.obj X) (F.obj Y)]
+
+/-- As for products, any functor between categories with binary biproducts gives rise to a
+    morphism `F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y`. -/
+def biprod_comparison : F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y :=
+biprod.lift (F.map biprod.fst) (F.map biprod.snd)
+
+@[simp, reassoc] lemma biprod_comparison_fst :
+  biprod_comparison F X Y ≫ biprod.fst = F.map biprod.fst :=
+biprod.lift_fst _ _
+
+@[simp, reassoc] lemma biprod_comparison_snd :
+  biprod_comparison F X Y ≫ biprod.snd = F.map biprod.snd :=
+biprod.lift_snd _ _
+
+/-- As for coproducts, any functor between categories with binary biproducts gives rise to a
+    morphism `F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)`. -/
+def biprod_comparison' : F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y) :=
+biprod.desc (F.map biprod.inl) (F.map biprod.inr)
+
+@[simp, reassoc] lemma inl_biprod_comparison' :
+  biprod.inl ≫ biprod_comparison' F X Y = F.map biprod.inl :=
+biprod.inl_desc _ _
+
+@[simp, reassoc] lemma inr_biprod_comparison' :
+  biprod.inr ≫ biprod_comparison' F X Y = F.map biprod.inr :=
+biprod.inr_desc _ _
+
+variables [preserves_zero_morphisms F]
+
+/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
+    the biproduct, see `preserves_binary_biproduct_of_mono_biprod_comparison`. -/
+@[simp, reassoc] lemma biprod_comparison'_comp_biprod_comparison :
+  biprod_comparison' F X Y ≫ biprod_comparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y) :=
+by { ext; simp [← functor.map_comp] }
+
+instance : split_epi (biprod_comparison F X Y) :=
+⟨biprod_comparison' F X Y⟩
+
+@[simp] lemma section_biprod_comparison :
+  section_ (biprod_comparison F X Y) = biprod_comparison' F X Y := rfl
+
+instance : split_mono (biprod_comparison' F X Y) :=
+⟨biprod_comparison F X Y⟩
+
+@[simp] lemma retraction_biprod_comparison' :
+  retraction (biprod_comparison' F X Y) = biprod_comparison F X Y := rfl
+
+end
+
+variables [preserves_zero_morphisms F] [preserves_binary_biproduct X Y F]
 
 instance has_binary_biproduct_of_preserves : has_binary_biproduct (F.obj X) (F.obj Y) :=
 has_binary_biproduct.mk
@@ -311,6 +413,30 @@ def preserves_biproduct_of_preserves_product {f : J → C} [preserves_limit (dis
       (F.map_cone b.to_cone)).symm (is_limit_of_preserves F hb.is_limit)) $
       cones.ext (iso.refl _) (by tidy) }
 
+/-- If the (product-like) biproduct comparison for `F` and `f` is a monomorphism, then `F`
+    preserves the biproduct of `f`. For the converse, see `map_biproduct`. -/
+def preserves_biproduct_of_mono_biproduct_comparison {f : J → C} [has_biproduct f]
+  [has_biproduct (F.obj ∘ f)] [mono (biproduct_comparison F f)] : preserves_biproduct f F :=
+begin
+  have : pi_comparison F f = (F.map_iso (biproduct.iso_product f)).inv ≫
+    biproduct_comparison F f ≫ (biproduct.iso_product _).hom,
+  { ext, convert pi_comparison_comp_π F f j.as; simp [← functor.map_comp] },
+  haveI : is_iso (biproduct_comparison F f) := is_iso_of_mono_of_split_epi _,
+  haveI : is_iso (pi_comparison F f) := by { rw this, apply_instance },
+  haveI := preserves_product.of_iso_comparison F f,
+  apply preserves_biproduct_of_preserves_product
+end
+
+/-- If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F`
+    preserves the biproduct of `F` and `f`. For the converse, see `map_biproduct`. -/
+def preserves_biproduct_of_epi_biproduct_comparison' {f : J → C} [has_biproduct f]
+  [has_biproduct (F.obj ∘ f)] [epi (biproduct_comparison' F f)] : preserves_biproduct f F :=
+begin
+  haveI : epi (section_ (biproduct_comparison F f)) := by simpa,
+  haveI : is_iso (biproduct_comparison F f) := is_iso.of_epi_section,
+  apply preserves_biproduct_of_mono_biproduct_comparison
+end
+
 /-- A functor between preadditive categories that preserves (zero morphisms and) finite products
     preserves finite biproducts. -/
 def preserves_biproducts_of_shape_of_preserves_products_of_shape
@@ -385,6 +511,31 @@ def preserves_binary_biproduct_of_preserves_binary_product {X Y : C}
       (F.map_cone b.to_cone)).symm (is_limit_of_preserves F hb.is_limit)) $
         cones.ext (iso.refl _) (λ j, by { rcases j with ⟨⟨⟩⟩, tidy }) }
 
+/-- If the (product-like) biproduct comparison for `F`, `X` and `Y` is a monomorphism, then
+    `F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`. -/
+def preserves_binary_biproduct_of_mono_biprod_comparison {X Y : C} [has_binary_biproduct X Y]
+  [has_binary_biproduct (F.obj X) (F.obj Y)] [mono (biprod_comparison F X Y)] :
+  preserves_binary_biproduct X Y F :=
+begin
+  have : prod_comparison F X Y = (F.map_iso (biprod.iso_prod X Y)).inv ≫
+    biprod_comparison F X Y ≫ (biprod.iso_prod _ _).hom := by { ext; simp [← functor.map_comp] },
+  haveI : is_iso (biprod_comparison F X Y) := is_iso_of_mono_of_split_epi _,
+  haveI : is_iso (prod_comparison F X Y) := by { rw this, apply_instance },
+  haveI := preserves_limit_pair.of_iso_prod_comparison F X Y,
+  apply preserves_binary_biproduct_of_preserves_binary_product
+end
+
+/-- If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then
+    `F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`. -/
+def preserves_binary_biproduct_of_epi_biprod_comparison' {X Y : C} [has_binary_biproduct X Y]
+  [has_binary_biproduct (F.obj X) (F.obj Y)] [epi (biprod_comparison' F X Y)] :
+  preserves_binary_biproduct X Y F :=
+begin
+  haveI : epi (section_ (biprod_comparison F X Y)) := by simpa,
+  haveI : is_iso (biprod_comparison F X Y) := is_iso.of_epi_section,
+  apply preserves_binary_biproduct_of_mono_biprod_comparison
+end
+
 /-- A functor between preadditive categories that preserves (zero morphisms and) binary products
     preserves binary biproducts. -/
 def preserves_binary_biproducts_of_preserves_binary_products

src/category_theory/limits/shapes/biproducts.lean

@@ -102,7 +102,9 @@ def to_cone (B : bicone F) : cone (discrete.functor F) :=
 
 @[simp] lemma to_cone_X (B : bicone F) : B.to_cone.X = B.X := rfl
 
-@[simp] lemma to_cone_π_app (B : bicone F) (j : J) : B.to_cone.π.app ⟨j⟩ = B.π j := rfl
+@[simp] lemma to_cone_π_app (B : bicone F) (j : discrete J) : B.to_cone.π.app j = B.π j.as := rfl
+
+lemma to_cone_π_app_mk (B : bicone F) (j : J) : B.to_cone.π.app ⟨j⟩ = B.π j := rfl
 
 /-- Extract the cocone from a bicone. -/
 def to_cocone (B : bicone F) : cocone (discrete.functor F) :=
@@ -111,7 +113,10 @@ def to_cocone (B : bicone F) : cocone (discrete.functor F) :=
 
 @[simp] lemma to_cocone_X (B : bicone F) : B.to_cocone.X = B.X := rfl
 
-@[simp] lemma to_cocone_ι_app (B : bicone F) (j : J) : B.to_cocone.ι.app ⟨j⟩ = B.ι j := rfl
+@[simp] lemma to_cocone_ι_app (B : bicone F) (j : discrete J) : B.to_cocone.ι.app j = B.ι j.as :=
+rfl
+
+lemma to_cocone_ι_app_mk (B : bicone F) (j : J) : B.to_cocone.ι.app ⟨j⟩ = B.ι j := rfl
 
 /-- We can turn any limit cone over a discrete collection of objects into a bicone. -/
 @[simps]
@@ -384,12 +389,36 @@ is_colimit.map (biproduct.is_colimit f) (biproduct.bicone g).to_cocone
   (w : ∀ j, biproduct.ι f j ≫ g = biproduct.ι f j ≫ h) : g = h :=
 (biproduct.is_colimit f).hom_ext (λ j, w j.as)
 
+/-- The canonical isomorphism between the chosen biproduct and the chosen product. -/
+def biproduct.iso_product (f : J → C) [has_biproduct f] : ⨁ f ≅ ∏ f :=
+is_limit.cone_point_unique_up_to_iso (biproduct.is_limit f) (limit.is_limit _)
+
+@[simp] lemma biproduct.iso_product_hom {f : J → C} [has_biproduct f] :
+  (biproduct.iso_product f).hom = pi.lift (biproduct.π f) :=
+limit.hom_ext $ λ j, by simp [biproduct.iso_product]
+
+@[simp] lemma biproduct.iso_product_inv {f : J → C} [has_biproduct f] :
+  (biproduct.iso_product f).inv = biproduct.lift (pi.π f) :=
+biproduct.hom_ext _ _ $ λ j, by simp [iso.inv_comp_eq]
+
+/-- The canonical isomorphism between the chosen biproduct and the chosen coproduct. -/
+def biproduct.iso_coproduct (f : J → C) [has_biproduct f] : ⨁ f ≅ ∐ f :=
+is_colimit.cocone_point_unique_up_to_iso (biproduct.is_colimit f) (colimit.is_colimit _)
+
+@[simp] lemma biproduct.iso_coproduct_inv {f : J → C} [has_biproduct f] :
+  (biproduct.iso_coproduct f).inv = sigma.desc (biproduct.ι f) :=
+colimit.hom_ext $ λ j, by simp [biproduct.iso_coproduct]
+
+@[simp] lemma biproduct.iso_coproduct_hom {f : J → C} [has_biproduct f] :
+  (biproduct.iso_coproduct f).hom = biproduct.desc (sigma.ι f) :=
+biproduct.hom_ext' _ _ $ λ j, by simp [← iso.eq_comp_inv]
+
 lemma biproduct.map_eq_map' {f g : J → C} [has_biproduct f] [has_biproduct g]
   (p : Π b, f b ⟶ g b) : biproduct.map p = biproduct.map' p :=
 begin
   ext j j',
   simp only [discrete.nat_trans_app, limits.is_colimit.ι_map, limits.is_limit.map_π, category.assoc,
-    ←bicone.to_cone_π_app, ←biproduct.bicone_π, ←bicone.to_cocone_ι_app, ←biproduct.bicone_ι],
+    ←bicone.to_cone_π_app_mk, ←biproduct.bicone_π, ←bicone.to_cocone_ι_app_mk, ←biproduct.bicone_ι],
   simp only [biproduct.bicone_ι, biproduct.bicone_π, bicone.to_cocone_ι_app, bicone.to_cone_π_app],
   dsimp,
   rw [biproduct.ι_π_assoc, biproduct.ι_π],
@@ -1068,6 +1097,30 @@ binary_fan.is_limit.hom_ext (binary_biproduct.is_limit X Y) h₀ h₁
   (h₀ : biprod.inl ≫ f = biprod.inl ≫ g) (h₁ : biprod.inr ≫ f = biprod.inr ≫ g) : f = g :=
 binary_cofan.is_colimit.hom_ext (binary_biproduct.is_colimit X Y) h₀ h₁
 
+/-- The canonical isomorphism between the chosen biproduct and the chosen product. -/
+def biprod.iso_prod (X Y : C) [has_binary_biproduct X Y] : X ⊞ Y ≅ X ⨯ Y :=
+is_limit.cone_point_unique_up_to_iso (binary_biproduct.is_limit X Y) (limit.is_limit _)
+
+@[simp] lemma biprod.iso_prod_hom {X Y : C} [has_binary_biproduct X Y] :
+  (biprod.iso_prod X Y).hom = prod.lift biprod.fst biprod.snd :=
+by ext; simp [biprod.iso_prod]
+
+@[simp] lemma biprod.iso_prod_inv {X Y : C} [has_binary_biproduct X Y] :
+  (biprod.iso_prod X Y).inv = biprod.lift prod.fst prod.snd :=
+by apply biprod.hom_ext; simp [iso.inv_comp_eq]
+
+/-- The canonical isomorphism between the chosen biproduct and the chosen coproduct. -/
+def biprod.iso_coprod (X Y : C) [has_binary_biproduct X Y] : X ⊞ Y ≅ X ⨿ Y :=
+is_colimit.cocone_point_unique_up_to_iso (binary_biproduct.is_colimit X Y) (colimit.is_colimit _)
+
+@[simp] lemma biprod.iso_coprod_inv {X Y : C} [has_binary_biproduct X Y] :
+  (biprod.iso_coprod X Y).inv = coprod.desc biprod.inl biprod.inr :=
+by ext; simp [biprod.iso_coprod]; refl
+
+@[simp] lemma biprod_iso_coprod_hom {X Y : C} [has_binary_biproduct X Y] :
+  (biprod.iso_coprod X Y).hom = biprod.desc coprod.inl coprod.inr :=
+by apply biprod.hom_ext'; simp [← iso.eq_comp_inv]
+
 lemma biprod.map_eq_map' {W X Y Z : C} [has_binary_biproduct W X] [has_binary_biproduct Y Z]
   (f : W ⟶ Y) (g : X ⟶ Z) : biprod.map f g = biprod.map' f g :=
 begin
@@ -1094,19 +1147,19 @@ end
 
 instance biprod.inl_mono {X Y : C} [has_binary_biproduct X Y] :
   split_mono (biprod.inl : X ⟶ X ⊞ Y) :=
-{ retraction := biprod.desc (𝟙 X) (biprod.inr ≫ biprod.fst) }
+{ retraction := biprod.fst }
 
 instance biprod.inr_mono {X Y : C} [has_binary_biproduct X Y] :
   split_mono (biprod.inr : Y ⟶ X ⊞ Y) :=
-{ retraction := biprod.desc (biprod.inl ≫ biprod.snd) (𝟙 Y)}
+{ retraction := biprod.snd }
 
 instance biprod.fst_epi {X Y : C} [has_binary_biproduct X Y] :
   split_epi (biprod.fst : X ⊞ Y ⟶ X) :=
-{ section_ := biprod.lift (𝟙 X) (biprod.inl ≫ biprod.snd) }
+{ section_ := biprod.inl }
 
 instance biprod.snd_epi {X Y : C} [has_binary_biproduct X Y] :
   split_epi (biprod.snd : X ⊞ Y ⟶ Y) :=
-{ section_ := biprod.lift (biprod.inr ≫ biprod.fst) (𝟙 Y) }
+{ section_ := biprod.inr }
 
 @[simp,reassoc]
 lemma biprod.map_fst {W X Y Z : C} [has_binary_biproduct W X] [has_binary_biproduct Y Z]

src/category_theory/preadditive/additive_functor.lean

@@ -118,6 +118,7 @@ instance preserves_finite_biproducts_of_additive [additive F] : preserves_finite
         simp_rw [← F.map_id],
         refine congr_arg _ (hb.is_limit.hom_ext (λ j, hb.is_colimit.hom_ext (λ j', _))),
         cases j, cases j',
+        dsimp only [limits.bicone.to_cone_π_app],
         simp [sum_comp, comp_sum, bicone.ι_π, comp_dite, dite_comp],
       end } } }