feat: (co/bi/)products unchanged by reindexing and isomorphism of factors (#6259)

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

Author: kim-em

Mathlib/Algebra/Homology/DifferentialObject.lean

@@ -100,8 +100,7 @@ def dgoToHomologicalComplex :
       comm' := fun i j h => by
         dsimp at h ⊢
         subst h
-        simp [Category.comp_id, eqToHom_refl, dif_pos rfl, Category.assoc,
-          eqToHom_f']
+        simp only [dite_true, Category.assoc, eqToHom_f']
         -- Porting note: this `rw` used to be part of the `simp`.
         have : f.f i ≫ Y.d i = X.d i ≫ f.f _ := (congr_fun f.comm i).symm
         rw [reassoc_of% this] }
@@ -146,7 +145,7 @@ to the category of homological complexes in `V`.
 -/
 @[simps]
 def dgoEquivHomologicalComplex :
-    DifferentialObject ℤ (GradedObjectWithShift b V) ≌ 
+    DifferentialObject ℤ (GradedObjectWithShift b V) ≌
       HomologicalComplex V (ComplexShape.up' b) where
   functor := dgoToHomologicalComplex b V
   inverse := homologicalComplexToDGO b V

Mathlib/CategoryTheory/EqToHom.lean

@@ -69,8 +69,35 @@ theorem eqToHom_comp_iff {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y)
     mpr := fun h => h ▸ by simp [whisker_eq _ h] }
 #align category_theory.eq_to_hom_comp_iff CategoryTheory.eqToHom_comp_iff
 
+/-- We can push `eqToHom` to the left through families of morphisms. -/
+-- The simpNF linter incorrectly claims that this will never apply.
+-- https://github.com/leanprover-community/mathlib4/issues/5049
+@[reassoc (attr := simp, nolint simpNF)]
+theorem eqToHom_naturality {f g : β → C} (z : ∀ b, f b ⟶ g b) {j j' : β} (w : j = j') :
+    z j ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ z j' := by
+  cases w
+  simp
+
+/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`. -/
+-- The simpNF linter incorrectly claims that this will never apply.
+-- https://github.com/leanprover-community/mathlib4/issues/5049
+@[reassoc (attr := simp, nolint simpNF)]
+theorem eqToHom_iso_hom_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
+    (z j).hom ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').hom := by
+  cases w
+  simp
+
+/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`. -/
+-- The simpNF linter incorrectly claims that this will never apply.
+-- https://github.com/leanprover-community/mathlib4/issues/5049
+@[reassoc (attr := simp, nolint simpNF)]
+theorem eqToHom_iso_inv_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
+    (z j).inv ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').inv := by
+  cases w
+  simp
+
 /- Porting note: simpNF complains about this not reducing but it is clearly used
-in `congrArg_mrp_hom_left`. It has been no-linted. -/
+in `congrArg_mpr_hom_left`. It has been no-linted. -/
 /-- Reducible form of congrArg_mpr_hom_left -/
 @[simp, nolint simpNF]
 theorem congrArg_cast_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

@@ -583,6 +583,53 @@ def biproduct.mapIso {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀
   inv := biproduct.map fun b => (p b).inv
 #align category_theory.limits.biproduct.map_iso CategoryTheory.Limits.biproduct.mapIso
 
+/-- Two biproducts which differ by an equivalence in the indexing type,
+and up to isomorphism in the factors, are isomorphic.
+
+Unfortunately there are two natural ways to define each direction of this isomorphism
+(because it is true for both products and coproducts separately).
+We give the alternative definitions as lemmas below.
+-/
+@[simps]
+def biproduct.whisker_equiv {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j)
+    [HasBiproduct f] [HasBiproduct g] : ⨁ f ≅ ⨁ g where
+  hom := biproduct.desc fun j => (w j).inv ≫ biproduct.ι g (e j)
+  inv := biproduct.desc fun k => eqToHom (by simp) ≫ (w (e.symm k)).hom ≫ biproduct.ι f _
+
+lemma biproduct.whisker_equiv_hom_eq_lift {f : J → C} {g : K → C} (e : J ≃ K)
+    (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
+    (biproduct.whisker_equiv e w).hom =
+      biproduct.lift fun k => biproduct.π f (e.symm k) ≫ (w _).inv ≫ eqToHom (by simp) := by
+  simp only [whisker_equiv_hom]
+  ext k j
+  by_cases h : k = e j
+  · subst h
+    simp
+  · simp only [ι_desc_assoc, Category.assoc, ne_eq, lift_π]
+    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
+    · simp
+    · rintro rfl
+      simp at h
+    · exact Ne.symm h
+
+lemma biproduct.whisker_equiv_inv_eq_lift {f : J → C} {g : K → C} (e : J ≃ K)
+    (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
+    (biproduct.whisker_equiv e w).inv =
+      biproduct.lift fun j => biproduct.π g (e j) ≫ (w j).hom := by
+  simp only [whisker_equiv_inv]
+  ext j k
+  by_cases h : k = e j
+  · subst h
+    simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
+      Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
+      lift_π, bicone_ι_π_self_assoc]
+  · simp only [ι_desc_assoc, Category.assoc, ne_eq, lift_π]
+    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
+    · simp
+    · exact h
+    · rintro rfl
+      simp at h
+
 instance (f : ι → Type _) (g : (i : ι) → (f i) → C)
     [∀ i, HasBiproduct (g i)] [HasBiproduct fun i => ⨁ g i] :
     HasBiproduct fun p : Σ i, f i => g p.1 p.2 where

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -260,6 +260,24 @@ abbrev Sigma.mapIso {f g : β → C} [HasCoproductsOfShape β C] (p : ∀ b, f b
   colim.mapIso (Discrete.natIso fun X => p X.as)
 #align category_theory.limits.sigma.map_iso CategoryTheory.Limits.Sigma.mapIso
 
+/-- Two products which differ by an equivalence in the indexing type,
+and up to isomorphism in the factors, are isomorphic.
+-/
+@[simps]
+def Pi.whisker_equiv {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j)
+    [HasProduct f] [HasProduct g] : ∏ f ≅ ∏ g where
+  hom := Pi.lift fun k => Pi.π f (e.symm k) ≫ (w _).inv ≫ eqToHom (by simp)
+  inv := Pi.lift fun j => Pi.π g (e j) ≫ (w j).hom
+
+/-- Two coproducts which differ by an equivalence in the indexing type,
+and up to isomorphism in the factors, are isomorphic.
+-/
+@[simps]
+def Sigma.whisker_equiv {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j)
+    [HasCoproduct f] [HasCoproduct g] : ∐ f ≅ ∐ g where
+  hom := Sigma.desc fun j => (w j).inv ≫ Sigma.ι g (e j)
+  inv := Sigma.desc fun k => eqToHom (by simp) ≫ (w (e.symm k)).hom ≫ Sigma.ι f _
+
 instance (f : ι → Type _) (g : (i : ι) → (f i) → C)
     [∀ i, HasProduct (g i)] [HasProduct fun i => ∏ g i] :
     HasProduct fun p : Σ i, f i => g p.1 p.2 where