feat(category_theory/limits): reindexing (co/bi)products (#14193)

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

src/category_theory/limits/shapes/biproducts.lean

@@ -1395,6 +1395,20 @@ by { ext, simp, }
 
 end
 
+/-- Reindex a categorical biproduct via an equivalence of the index types. -/
+@[simps]
+def biproduct.reindex {β γ : Type v} [fintype β] [decidable_eq β] [decidable_eq γ]
+  (ε : β ≃ γ) (f : γ → C) [has_biproduct f] [has_biproduct (f ∘ ε)] : (⨁ (f ∘ ε)) ≅ (⨁ f) :=
+{ hom := biproduct.desc (λ b, biproduct.ι f (ε b)),
+  inv := biproduct.lift (λ b, biproduct.π f (ε b)),
+  hom_inv_id' := by { ext b b', by_cases h : b = b', { subst h, simp, }, { simp [h], }, },
+  inv_hom_id' := begin
+    ext g g',
+    by_cases h : g = g';
+    simp [preadditive.sum_comp, preadditive.comp_sum, biproduct.ι_π, biproduct.ι_π_assoc, comp_dite,
+      equiv.apply_eq_iff_eq_symm_apply, finset.sum_dite_eq' finset.univ (ε.symm g') _, h],
+  end, }
+
 /--
 In a preadditive category, we can construct a binary biproduct for `X Y : C` from
 any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

src/category_theory/limits/shapes/products.lean

@@ -191,4 +191,57 @@ 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
 
+section reindex
+variables {C} {γ : Type v} (ε : β ≃ γ) (f : γ → C)
+
+section
+variables [has_product f] [has_product (f ∘ ε)]
+
+/-- Reindex a categorical product via an equivalence of the index types. -/
+def pi.reindex : pi_obj (f ∘ ε) ≅ pi_obj f :=
+has_limit.iso_of_equivalence (discrete.equivalence ε) (discrete.nat_iso (λ i, iso.refl _))
+
+@[simp, reassoc]
+lemma pi.reindex_hom_π (b : β) : (pi.reindex ε f).hom ≫ pi.π f (ε b) = pi.π (f ∘ ε) b :=
+begin
+  dsimp [pi.reindex],
+  simp only [has_limit.iso_of_equivalence_hom_π, discrete.nat_iso_inv_app,
+    equivalence.equivalence_mk'_counit, discrete.equivalence_counit_iso, discrete.nat_iso_hom_app,
+    eq_to_iso.hom, eq_to_hom_map],
+  dsimp,
+  simpa using limit.w (discrete.functor (f ∘ ε)) (eq_to_hom (ε.symm_apply_apply b)),
+end
+
+@[simp, reassoc]
+lemma pi.reindex_inv_π (b : β) : (pi.reindex ε f).inv ≫ pi.π (f ∘ ε) b = pi.π f (ε b) :=
+by simp [iso.inv_comp_eq]
+
+end
+
+section
+variables [has_coproduct f] [has_coproduct (f ∘ ε)]
+
+/-- Reindex a categorical coproduct via an equivalence of the index types. -/
+def sigma.reindex : sigma_obj (f ∘ ε) ≅ sigma_obj f :=
+has_colimit.iso_of_equivalence (discrete.equivalence ε) (discrete.nat_iso (λ i, iso.refl _))
+
+@[simp, reassoc]
+lemma sigma.ι_reindex_hom (b : β) : sigma.ι (f ∘ ε) b ≫ (sigma.reindex ε f).hom = sigma.ι f (ε b) :=
+begin
+  dsimp [sigma.reindex],
+  simp only [has_colimit.iso_of_equivalence_hom_π, equivalence.equivalence_mk'_unit,
+    discrete.equivalence_unit_iso, discrete.nat_iso_hom_app, eq_to_iso.hom, eq_to_hom_map,
+    discrete.nat_iso_inv_app],
+  dsimp,
+  simp [←colimit.w (discrete.functor f) (eq_to_hom (ε.apply_symm_apply (ε b)))],
+end
+
+@[simp, reassoc]
+lemma sigma.ι_reindex_inv (b : β) : sigma.ι f (ε b) ≫ (sigma.reindex ε f).inv = sigma.ι (f ∘ ε) b :=
+by simp [iso.comp_inv_eq]
+
+end
+
+end reindex
+
 end category_theory.limits