feat(category_theory/limits): (co/bi)products over types with a uniqu…

…e term (#14191)




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

src/category_theory/discrete_category.lean

@@ -64,6 +64,9 @@ by { dsimp [discrete], apply_instance }
 instance [subsingleton α] : subsingleton (discrete α) :=
 by { dsimp [discrete], apply_instance }
 
+instance [unique α] : unique (discrete α) :=
+by { dsimp [discrete], apply_instance }
+
 /-- Extract the equation from a morphism in a discrete category. -/
 lemma eq_of_hom {X Y : discrete α} (i : X ⟶ Y) : X = Y := i.down.down
 

src/category_theory/limits/shapes/biproducts.lean

@@ -72,7 +72,7 @@ structure bicone (F : J → C) :=
 (X : C)
 (π : Π j, X ⟶ F j)
 (ι : Π j, F j ⟶ X)
-(ι_π : ∀ j j', ι j ≫ π j' = if h : j = j' then eq_to_hom (congr_arg F h) else 0)
+(ι_π : ∀ j j', ι j ≫ π j' = if h : j = j' then eq_to_hom (congr_arg F h) else 0 . obviously)
 
 @[simp, reassoc] lemma bicone_ι_π_self {F : J → C} (B : bicone F) (j : J) :
   B.ι j ≫ B.π j = 𝟙 (F j) :=
@@ -600,6 +600,30 @@ by { refine ⟨⟨biproduct pempty.elim, λ X, ⟨⟨⟨0⟩, _⟩⟩, λ X, ⟨
 
 end
 
+section
+variables [unique J] (f : J → C)
+
+/-- The limit bicone for the biproduct over an index type with exactly one term. -/
+@[simps]
+def limit_bicone_of_unique : limit_bicone f :=
+{ bicone :=
+  { X := f default,
+    π := λ j, eq_to_hom (by congr),
+    ι := λ j, eq_to_hom (by congr), },
+  is_bilimit :=
+  { is_limit := (limit_cone_of_unique f).is_limit,
+    is_colimit := (colimit_cocone_of_unique f).is_colimit, }, }
+
+@[priority 100] instance has_biproduct_unique : has_biproduct f :=
+has_biproduct.mk (limit_bicone_of_unique f)
+
+/-- A biproduct over a index type with exactly one term is just the object over that term. -/
+@[simps]
+def biproduct_unique_iso : ⨁ f ≅ f default :=
+(biproduct.unique_up_to_iso _ (limit_bicone_of_unique f).is_bilimit).symm
+
+end
+
 /--
 A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
 maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,

src/category_theory/limits/shapes/products.lean

@@ -191,6 +191,69 @@ abbreviation has_products := Π (J : Type v), has_limits_of_shape (discrete J) C
 /-- An abbreviation for `Π J, has_colimits_of_shape (discrete J) C` -/
 abbreviation has_coproducts := Π (J : Type v), has_colimits_of_shape (discrete J) C
 
+/-!
+(Co)products over a type with a unique term.
+-/
+section unique
+variables {C} [unique β] (f : β → C)
+
+/-- The limit cone for the product over an index type with exactly one term. -/
+@[simps]
+def limit_cone_of_unique : limit_cone (discrete.functor f) :=
+{ cone :=
+  { X := f default,
+    π := { app := λ j, eq_to_hom (by { dsimp, congr, }), }, },
+  is_limit :=
+  { lift := λ s, s.π.app default,
+    fac' := λ s j, begin
+      have w := (s.π.naturality (eq_to_hom (unique.default_eq _))).symm,
+      dsimp at w,
+      simpa using w,
+    end,
+    uniq' := λ s m w, begin
+      specialize w default,
+      dsimp at w,
+      simpa using w,
+    end, }, }
+
+@[priority 100] instance has_product_unique : has_product f :=
+has_limit.mk (limit_cone_of_unique f)
+
+/-- A product over a index type with exactly one term is just the object over that term. -/
+@[simps]
+def product_unique_iso : ∏ f ≅ f default :=
+is_limit.cone_point_unique_up_to_iso (limit.is_limit _) (limit_cone_of_unique f).is_limit
+
+/-- The colimit cocone for the coproduct over an index type with exactly one term. -/
+@[simps]
+def colimit_cocone_of_unique : colimit_cocone (discrete.functor f) :=
+{ cocone :=
+  { X := f default,
+    ι := { app := λ j, eq_to_hom (by { dsimp, congr, }), }, },
+  is_colimit :=
+  { desc := λ s, s.ι.app default,
+    fac' := λ s j, begin
+      have w := (s.ι.naturality (eq_to_hom (unique.eq_default _))),
+      dsimp at w,
+      simpa using w,
+    end,
+    uniq' := λ s m w, begin
+      specialize w default,
+      dsimp at w,
+      simpa using w,
+    end, }, }
+
+@[priority 100] instance has_coproduct_unique : has_coproduct f :=
+has_colimit.mk (colimit_cocone_of_unique f)
+
+/-- A coproduct over a index type with exactly one term is just the object over that term. -/
+@[simps]
+def coproduct_unique_iso : ∐ f ≅ f default :=
+is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _)
+  (colimit_cocone_of_unique f).is_colimit
+
+end unique
+
 section reindex
 variables {C} {γ : Type v} (ε : β ≃ γ) (f : γ → C)