feat(category_theory/limits): is_bilimit

src/category_theory/limits/shapes/biproducts.lean

@@ -73,7 +73,7 @@ structure bicone (F : J → C) :=
 @[simp] lemma bicone_ι_π_self {F : J → C} (B : bicone F) (j : J) : B.ι j ≫ B.π j = 𝟙 (F j) :=
 by simpa using B.ι_π j j
 
-@[simp] lemma bicone_ι_π_ne {F : J → C} (B : bicone F) {j j' : J} (h : j ≠ j') :
+@[simp, reassoc] lemma bicone_ι_π_ne {F : J → C} (B : bicone F) {j j' : J} (h : j ≠ j') :
   B.ι j ≫ B.π j' = 0 :=
 by simpa [h] using B.ι_π j j'
 
@@ -92,6 +92,38 @@ def to_cocone (B : bicone F) : cocone (discrete.functor F) :=
 { X := B.X,
   ι := { app := λ j, B.ι j }, }
 
+/-- We can turn any limit cone over a discrete collection of objects into a bicone. -/
+@[simps]
+def of_limit_cone {f : J → C} {t : cone (discrete.functor f)} (ht : is_limit t) :
+  bicone f :=
+{ X := t.X,
+  π := t.π.app,
+  ι := λ j, ht.lift (fan.mk _ (λ j', if h : j = j' then eq_to_hom (congr_arg f h) else 0)),
+  ι_π := λ j j', by simp }
+
+lemma ι_of_is_limit {f : J → C} {t : bicone f} (ht : is_limit t.to_cone) (j : J) :
+  t.ι j = ht.lift (fan.mk _ (λ j', if h : j = j' then eq_to_hom (congr_arg f h) else 0)) :=
+ht.hom_ext (λ j', by { rw ht.fac, simp [t.ι_π] })
+
+/-- We can turn any colimit cocone over a discrete collection of objects into a bicone. -/
+@[simps]
+def of_colimit_cocone {f : J → C} {t : cocone (discrete.functor f)} (ht : is_colimit t) :
+  bicone f :=
+{ X := t.X,
+  π := λ j, ht.desc (cofan.mk _ (λ j', if h : j' = j then eq_to_hom (congr_arg f h) else 0)),
+  ι := t.ι.app,
+  ι_π := λ j j', by simp }
+
+lemma π_of_is_colimit {f : J → C} {t : bicone f} (ht : is_colimit t.to_cocone) (j : J) :
+  t.π j = ht.desc (cofan.mk _ (λ j', if h : j' = j then eq_to_hom (congr_arg f h) else 0)) :=
+ht.hom_ext (λ j', by { rw ht.fac, simp [t.ι_π] })
+
+/-- Structure witnessing that a bicone is both a limit cone and a colimit cocone. -/
+@[nolint has_inhabited_instance]
+structure is_bilimit {F : J → C} (B : bicone F) :=
+(is_limit : is_limit B.to_cone)
+(is_colimit : is_colimit B.to_cocone)
+
 end bicone
 
 /--
@@ -100,8 +132,7 @@ A bicone over `F : J → C`, which is both a limit cone and a colimit cocone.
 @[nolint has_inhabited_instance]
 structure limit_bicone (F : J → C) :=
 (bicone : bicone F)
-(is_limit : is_limit bicone.to_cone)
-(is_colimit : is_colimit bicone.to_cocone)
+(is_bilimit : bicone.is_bilimit)
 
 /--
 `has_biproduct F` expresses the mere existence of a bicone which is
@@ -121,14 +152,18 @@ classical.choice has_biproduct.exists_biproduct
 def biproduct.bicone (F : J → C) [has_biproduct F] : bicone F :=
 (get_biproduct_data F).bicone
 
+/-- `biproduct.bicone F` is a bilimit bicone. -/
+def biproduct.is_bilimit (F : J → C) [has_biproduct F] : (biproduct.bicone F).is_bilimit :=
+(get_biproduct_data F).is_bilimit
+
 /-- `biproduct.bicone F` is a limit cone. -/
 def biproduct.is_limit (F : J → C) [has_biproduct F] : is_limit (biproduct.bicone F).to_cone :=
-(get_biproduct_data F).is_limit
+(get_biproduct_data F).is_bilimit.is_limit
 
 /-- `biproduct.bicone F` is a colimit cocone. -/
 def biproduct.is_colimit (F : J → C) [has_biproduct F] :
   is_colimit (biproduct.bicone F).to_cocone :=
-(get_biproduct_data F).is_colimit
+(get_biproduct_data F).is_bilimit.is_colimit
 
 @[priority 100]
 instance has_product_of_has_biproduct [has_biproduct F] : has_limit (discrete.functor F) :=
@@ -428,6 +463,25 @@ lemma to_cocone_ι_app_left (c : binary_bicone P Q) :
 lemma to_cocone_ι_app_right (c : binary_bicone P Q) :
   c.to_cocone.ι.app (walking_pair.right) = c.inr := rfl
 
+/-- Convert a `binary_bicone` into a `bicone` over a pair. -/
+@[simps]
+def to_bicone {X Y : C} (b : binary_bicone X Y) : bicone (pair X Y).obj :=
+{ X := b.X,
+  π := λ j, walking_pair.cases_on j b.fst b.snd,
+  ι := λ j, walking_pair.cases_on j b.inl b.inr,
+  ι_π := λ j j', by { cases j; cases j', tidy } }
+
+/-- A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone. -/
+def to_bicone_is_limit {X Y : C} (b : binary_bicone X Y) :
+  is_limit (b.to_bicone.to_cone) ≃ is_limit (b.to_cone) :=
+is_limit.equiv_iso_limit $ cones.ext (iso.refl _) (λ j, by { cases j, tidy })
+
+/-- A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit
+    cocone. -/
+def to_bicone_is_colimit {X Y : C} (b : binary_bicone X Y) :
+  is_colimit (b.to_bicone.to_cocone) ≃ is_colimit (b.to_cocone) :=
+is_colimit.equiv_iso_colimit $ cocones.ext (iso.refl _) (λ j, by { cases j, tidy })
+
 end binary_bicone
 
 namespace bicone
@@ -445,50 +499,52 @@ def to_binary_bicone {X Y : C} (b : bicone (pair X Y).obj) : binary_bicone X Y :
   inl_snd' := by simp [bicone.ι_π],
   inr_snd' := by { simp [bicone.ι_π], refl, }, }
 
-/--
-If the cone obtained from a bicone over `pair X Y` is a limit cone,
-so is the cone obtained by converting that bicone to a binary_bicone, then to a cone.
--/
-def to_binary_bicone_is_limit {X Y : C} {b : bicone (pair X Y).obj}
-  (c : is_limit (b.to_cone)) :
-  is_limit (b.to_binary_bicone.to_cone) :=
-{ lift := λ s, c.lift s,
-   fac' := λ s j, by { cases j; erw c.fac, },
-   uniq' := λ s m w,
-   begin
-     apply c.uniq s,
-     rintro (⟨⟩|⟨⟩),
-     exact w walking_pair.left,
-     exact w walking_pair.right,
-   end, }
+/-- A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit
+    cone.  -/
+def to_binary_bicone_is_limit {X Y : C} (b : bicone (pair X Y).obj) :
+  is_limit (b.to_binary_bicone.to_cone) ≃ is_limit (b.to_cone) :=
+is_limit.equiv_iso_limit $ cones.ext (iso.refl _) (λ j, by { cases j, tidy })
 
-/--
-If the cocone obtained from a bicone over `pair X Y` is a colimit cocone,
-so is the cocone obtained by converting that bicone to a binary_bicone, then to a cocone.
--/
-def to_binary_bicone_is_colimit {X Y : C} {b : bicone (pair X Y).obj}
-  (c : is_colimit (b.to_cocone)) :
-  is_colimit (b.to_binary_bicone.to_cocone) :=
-{ desc := λ s, c.desc s,
-   fac' := λ s j, by { cases j; erw c.fac, },
-   uniq' := λ s m w,
-   begin
-     apply c.uniq s,
-     rintro (⟨⟩|⟨⟩),
-     exact w walking_pair.left,
-     exact w walking_pair.right,
-   end, }
+/-- A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a
+    colimit cocone. -/
+def to_binary_bicone_is_colimit {X Y : C} (b : bicone (pair X Y).obj) :
+  is_colimit (b.to_binary_bicone.to_cocone) ≃ is_colimit (b.to_cocone) :=
+is_colimit.equiv_iso_colimit $ cocones.ext (iso.refl _) (λ j, by { cases j, tidy })
 
 end bicone
 
+/-- Structure witnessing that a binary bicone is a limit cone and a limit cocone. -/
+@[nolint has_inhabited_instance]
+structure binary_bicone.is_bilimit {P Q : C} (b : binary_bicone P Q) :=
+(is_limit : is_limit b.to_cone)
+(is_colimit : is_colimit b.to_cocone)
+
+/-- A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit. -/
+def binary_bicone.to_bicone_is_bilimit {X Y : C} (b : binary_bicone X Y) :
+  b.to_bicone.is_bilimit ≃ b.is_bilimit :=
+{ to_fun := λ h, ⟨b.to_bicone_is_limit h.is_limit, b.to_bicone_is_colimit h.is_colimit⟩,
+  inv_fun := λ h, ⟨b.to_bicone_is_limit.symm h.is_limit, b.to_bicone_is_colimit.symm h.is_colimit⟩,
+  left_inv := λ ⟨h, h'⟩, by { dsimp only, simp },
+  right_inv := λ ⟨h, h'⟩, by { dsimp only, simp } }
+
+/-- A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a
+    bilimit. -/
+def bicone.to_binary_bicone_is_bilimit {X Y : C} (b : bicone (pair X Y).obj) :
+  b.to_binary_bicone.is_bilimit ≃ b.is_bilimit :=
+{ to_fun := λ h, ⟨b.to_binary_bicone_is_limit h.is_limit,
+    b.to_binary_bicone_is_colimit h.is_colimit⟩,
+  inv_fun := λ h, ⟨b.to_binary_bicone_is_limit.symm h.is_limit,
+    b.to_binary_bicone_is_colimit.symm h.is_colimit⟩,
+  left_inv := λ ⟨h, h'⟩, by { dsimp only, simp },
+  right_inv := λ ⟨h, h'⟩, by { dsimp only, simp } }
+
 /--
 A bicone over `P Q : C`, which is both a limit cone and a colimit cocone.
 -/
 @[nolint has_inhabited_instance]
 structure binary_biproduct_data (P Q : C) :=
 (bicone : binary_bicone P Q)
-(is_limit : is_limit bicone.to_cone)
-(is_colimit : is_colimit bicone.to_cocone)
+(is_bilimit : bicone.is_bilimit)
 
 /--
 `has_binary_biproduct P Q` expresses the mere existence of a bicone which is
@@ -511,15 +567,20 @@ classical.choice has_binary_biproduct.exists_binary_biproduct
 def binary_biproduct.bicone (P Q : C) [has_binary_biproduct P Q] : binary_bicone P Q :=
 (get_binary_biproduct_data P Q).bicone
 
+/-- `binary_biproduct.bicone P Q` is a limit bicone. -/
+def binary_biproduct.is_bilimit (P Q : C) [has_binary_biproduct P Q] :
+  (binary_biproduct.bicone P Q).is_bilimit :=
+(get_binary_biproduct_data P Q).is_bilimit
+
 /-- `binary_biproduct.bicone P Q` is a limit cone. -/
 def binary_biproduct.is_limit (P Q : C) [has_binary_biproduct P Q] :
   is_limit (binary_biproduct.bicone P Q).to_cone :=
-(get_binary_biproduct_data P Q).is_limit
+(get_binary_biproduct_data P Q).is_bilimit.is_limit
 
 /-- `binary_biproduct.bicone P Q` is a colimit cocone. -/
 def binary_biproduct.is_colimit (P Q : C) [has_binary_biproduct P Q] :
   is_colimit (binary_biproduct.bicone P Q).to_cocone :=
-(get_binary_biproduct_data P Q).is_colimit
+(get_binary_biproduct_data P Q).is_bilimit.is_colimit
 
 section
 variable (C)
@@ -543,8 +604,7 @@ lemma has_binary_biproducts_of_finite_biproducts [has_finite_biproducts C] :
   has_binary_biproducts C :=
 { has_binary_biproduct := λ P Q, has_binary_biproduct.mk
   { bicone := (biproduct.bicone (pair P Q).obj).to_binary_bicone,
-    is_limit := bicone.to_binary_bicone_is_limit (biproduct.is_limit _),
-    is_colimit := bicone.to_binary_bicone_is_colimit (biproduct.is_colimit _) } }
+    is_bilimit := (bicone.to_binary_bicone_is_bilimit _).symm (biproduct.is_bilimit _) } }
 
 end
 
@@ -837,35 +897,36 @@ lemma has_biproduct_of_total {f : J → C} (b : bicone f) (total : ∑ j : J, b.
   has_biproduct f :=
 has_biproduct.mk
 { bicone := b,
-  is_limit :=
-  { lift := λ s, ∑ j, s.π.app j ≫ b.ι j,
-    uniq' := λ s m h,
-    begin
-      erw [←category.comp_id m, ←total, comp_sum],
-      apply finset.sum_congr rfl,
-      intros j m,
-      erw [reassoc_of (h j)],
-    end,
-    fac' := λ s j,
-    begin
-      simp only [sum_comp, category.assoc, bicone.to_cone_π_app, b.ι_π, comp_dite],
-      -- See note [dsimp, simp].
-      dsimp, simp,
-    end },
-  is_colimit :=
-  { desc := λ s, ∑ j, b.π j ≫ s.ι.app j,
-    uniq' := λ s m h,
-    begin
-      erw [←category.id_comp m, ←total, sum_comp],
-            apply finset.sum_congr rfl,
-      intros j m,
-      erw [category.assoc, h],
-    end,
-    fac' := λ s j,
-    begin
-      simp only [comp_sum, ←category.assoc, bicone.to_cocone_ι_app, b.ι_π, dite_comp],
-      dsimp, simp,
-    end } }
+  is_bilimit :=
+  { is_limit :=
+    { lift := λ s, ∑ j, s.π.app j ≫ b.ι j,
+      uniq' := λ s m h,
+      begin
+        erw [←category.comp_id m, ←total, comp_sum],
+        apply finset.sum_congr rfl,
+        intros j m,
+        erw [reassoc_of (h j)],
+      end,
+      fac' := λ s j,
+      begin
+        simp only [sum_comp, category.assoc, bicone.to_cone_π_app, b.ι_π, comp_dite],
+        -- See note [dsimp, simp].
+        dsimp, simp,
+      end },
+    is_colimit :=
+    { desc := λ s, ∑ j, b.π j ≫ s.ι.app j,
+      uniq' := λ s m h,
+      begin
+        erw [←category.id_comp m, ←total, sum_comp],
+              apply finset.sum_congr rfl,
+        intros j m,
+        erw [category.assoc, h],
+      end,
+      fac' := λ s j,
+      begin
+        simp only [comp_sum, ←category.assoc, bicone.to_cocone_ι_app, b.ι_π, dite_comp],
+        dsimp, simp,
+      end } } }
 
 /-- In a preadditive category, if the product over `f : J → C` exists,
     then the biproduct over `f` exists. -/
@@ -986,18 +1047,19 @@ lemma has_binary_biproduct_of_total {X Y : C} (b : binary_bicone X Y)
   has_binary_biproduct X Y :=
 has_binary_biproduct.mk
 { bicone := b,
-  is_limit :=
-  { lift := λ s, binary_fan.fst s ≫ b.inl +
-      binary_fan.snd s ≫ b.inr,
-    uniq' := λ s m h, by erw [←category.comp_id m, ←total,
-      comp_add, reassoc_of (h walking_pair.left), reassoc_of (h walking_pair.right)],
-    fac' := λ s j, by cases j; simp, },
-  is_colimit :=
-  { desc := λ s, b.fst ≫ binary_cofan.inl s +
-      b.snd ≫ binary_cofan.inr s,
-    uniq' := λ s m h, by erw [←category.id_comp m, ←total,
-      add_comp, category.assoc, category.assoc, h walking_pair.left, h walking_pair.right],
-    fac' := λ s j, by cases j; simp, } }
+  is_bilimit :=
+  { is_limit :=
+    { lift := λ s, binary_fan.fst s ≫ b.inl +
+        binary_fan.snd s ≫ b.inr,
+      uniq' := λ s m h, by erw [←category.comp_id m, ←total,
+        comp_add, reassoc_of (h walking_pair.left), reassoc_of (h walking_pair.right)],
+      fac' := λ s j, by cases j; simp, },
+    is_colimit :=
+    { desc := λ s, b.fst ≫ binary_cofan.inl s +
+        b.snd ≫ binary_cofan.inr s,
+      uniq' := λ s m h, by erw [←category.id_comp m, ←total,
+        add_comp, category.assoc, category.assoc, h walking_pair.left, h walking_pair.right],
+      fac' := λ s j, by cases j; simp, } } }
 
 /-- In a preadditive category, if the product of `X` and `Y` exists, then the
     binary biproduct of `X` and `Y` exists. -/