feat(Algebra/Homology): commutation up to signs of the compatibility …

…isomorphisms of the total complex with shifts in both variables (#11517)

Shifting horizontally a bicomplex by an integer `x` and then taking the total complex gives a cochain complex that is isomorphic to the shift of the total complex of the original bicomplex. The same applies to vertical shifts by an integer `y`. However, when we apply both horizontal and vertical shifts, depending on whether we apply the horizontal shift or the vertical shift first, we get two isomorphisms which differ by the sign `(x * y).negOnePow`.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/Algebra/Homology/BifunctorShift.lean

@@ -16,13 +16,14 @@ a functor `F : C₁ ⥤ C₂ ⥤ D`, we define an isomorphism of cochain complex
 - `CochainComplex.mapBifunctorShift₂Iso K₁ K₂ F y` of type
 `mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧` for `y : ℤ`.
 
-## TODO
-
-- obtain various compatibilities
+In the lemma `CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, we obtain
+that the two ways to deduce an isomorphism
+`mapBifunctor (K₁⟦x⟧) (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦x + y⟧` differ by the sign
+`(x * y).negOnePow`.
 
 -/
 
-open CategoryTheory Limits
+open CategoryTheory Category Limits
 
 variable {C₁ C₂ D : Type*} [Category C₁] [Category C₂] [Category D]
 
@@ -58,17 +59,19 @@ section
 variable [Preadditive C₁] [HasZeroMorphisms C₂] [Preadditive D]
   (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
   (F : C₁ ⥤ C₂ ⥤ D) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ)
-  [HasMapBifunctor K₁ K₂ F] [HasMapBifunctor (K₁⟦x⟧) K₂ F]
-  [HomologicalComplex₂.HasTotal ((HomologicalComplex₂.shiftFunctor₁ D x).obj
-    (((F.mapBifunctorHomologicalComplex _ _ ).obj K₁).obj K₂)) (ComplexShape.up ℤ)]
+  [HasMapBifunctor K₁ K₂ F]
 
 /-- Auxiliary definition for `mapBifunctorShift₁Iso`. -/
+@[simps! hom_f_f inv_f_f]
 def mapBifunctorHomologicalComplexShift₁Iso :
     ((F.mapBifunctorHomologicalComplex _ _).obj (K₁⟦x⟧)).obj K₂ ≅
     (HomologicalComplex₂.shiftFunctor₁ D x).obj
       (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂) :=
   HomologicalComplex.Hom.isoOfComponents (fun i₁ => Iso.refl _)
 
+instance : HasMapBifunctor (K₁⟦x⟧) K₂ F :=
+  HomologicalComplex₂.hasTotal_of_iso (mapBifunctorHomologicalComplexShift₁Iso K₁ K₂ F x).symm _
+
 /-- The canonical isomorphism `mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧`.
 This isomorphism does not involve signs. -/
 noncomputable def mapBifunctorShift₁Iso :
@@ -83,19 +86,20 @@ section
 variable [HasZeroMorphisms C₁] [Preadditive C₂] [Preadditive D]
   (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
   (F : C₁ ⥤ C₂ ⥤ D) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ)
-  [HasMapBifunctor K₁ K₂ F] [HasMapBifunctor K₁ (K₂⟦y⟧) F]
-  [HomologicalComplex₂.HasTotal
-    ((HomologicalComplex₂.shiftFunctor₂ D y).obj
-      (((F.mapBifunctorHomologicalComplex _ _ ).obj K₁).obj K₂)) (ComplexShape.up ℤ)]
+  [HasMapBifunctor K₁ K₂ F]
 
 /-- Auxiliary definition for `mapBifunctorShift₂Iso`. -/
+@[simps! hom_f_f inv_f_f]
 def mapBifunctorHomologicalComplexShift₂Iso :
     ((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj (K₂⟦y⟧) ≅
     (HomologicalComplex₂.shiftFunctor₂ D y).obj
       (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂) :=
   HomologicalComplex.Hom.isoOfComponents
     (fun i₁ => HomologicalComplex.Hom.isoOfComponents (fun i₂ => Iso.refl _))
 
+instance : HasMapBifunctor K₁ (K₂⟦y⟧) F :=
+  HomologicalComplex₂.hasTotal_of_iso (mapBifunctorHomologicalComplexShift₂Iso K₁ K₂ F y).symm _
+
 /-- The canonical isomorphism `mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧`.
 This isomorphism involves signs: on the summand `(F.obj (K₁.X p)).obj (K₂.X q)`, it is given
 by the multiplication by `(p * y).negOnePow`. -/
@@ -107,4 +111,35 @@ noncomputable def mapBifunctorShift₂Iso :
 
 end
 
+section
+
+variable [Preadditive C₁] [Preadditive C₂] [Preadditive D]
+  (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
+  (F : C₁ ⥤ C₂ ⥤ D) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (x y : ℤ)
+  [HasMapBifunctor K₁ K₂ F]
+
+lemma mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso :
+    mapBifunctorShift₁Iso K₁ (K₂⟦y⟧) F x ≪≫
+      (CategoryTheory.shiftFunctor _ x).mapIso (mapBifunctorShift₂Iso K₁ K₂ F y) =
+      (x * y).negOnePow • (mapBifunctorShift₂Iso (K₁⟦x⟧) K₂ F y ≪≫
+        (CategoryTheory.shiftFunctor _ y).mapIso (mapBifunctorShift₁Iso K₁ K₂ F x) ≪≫
+          (shiftFunctorComm (CochainComplex D ℤ) x y).app _) := by
+  ext1
+  dsimp [mapBifunctorShift₁Iso, mapBifunctorShift₂Iso]
+  rw [Functor.map_comp, Functor.map_comp, assoc, assoc, assoc,
+    ← HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc,
+    HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom,
+    ← HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc,
+    Linear.comp_units_smul, Linear.comp_units_smul,
+    smul_left_cancel_iff,
+    ← HomologicalComplex₂.total.map_comp_assoc,
+    ← HomologicalComplex₂.total.map_comp_assoc,
+    ← HomologicalComplex₂.total.map_comp_assoc]
+  congr 2
+  ext a b
+  dsimp [HomologicalComplex₂.shiftFunctor₁₂CommIso]
+  simp only [id_comp]
+
+end
+
 end CochainComplex

Mathlib/Algebra/Homology/TotalComplex.lean

@@ -38,6 +38,12 @@ variable {C : Type*} [Category C] [Preadditive C]
 of the objects `(K.X i₁).X i₂` such that `ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂` exists. -/
 abbrev HasTotal := K.toGradedObject.HasMap (ComplexShape.π c₁ c₂ c₁₂)
 
+variable {K L} in
+lemma hasTotal_of_iso [K.HasTotal c₁₂] : L.HasTotal c₁₂ :=
+  GradedObject.hasMap_of_iso (GradedObject.isoMk K.toGradedObject L.toGradedObject
+    (fun ⟨i₁, i₂⟩ =>
+      (HomologicalComplex.eval _ _ i₁ ⋙ HomologicalComplex.eval _ _ i₂).mapIso e)) _
+
 variable [K.HasTotal c₁₂]
 
 section

Mathlib/Algebra/Homology/TotalComplexShift.lean

@@ -25,12 +25,11 @@ for any `x : ℤ` (which does not involve signs) and an isomorphism
 for any `y : ℤ` (which is given by the multiplication by `(p * y).negOnePow` on the
 summand in bidegree `(p, q)` of `K`).
 
-## TODO
-
-- show that the two sorts of shift functors on bicomplexes "commute", but that signs
-appear when we compare the compositions of the two compatibilities with the total complex functor.
-- deduce compatiblities with shifts on both variables of the action of a
-bifunctor on cochain complexes
+Depending on the order of the "composition" of the two isomorphisms
+`totalShift₁Iso` and `totalShift₂Iso`, we get
+two ways to identify `((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).total (up ℤ)`
+and `(K.total (up ℤ))⟦x + y⟧`. The lemma `totalShift₁Iso_trans_totalShift₂Iso` shows that
+these two compositions of isomorphisms differ by the sign `(x * y).negOnePow`.
 
 -/
 
@@ -53,11 +52,77 @@ abbrev shiftFunctor₂ (y : ℤ) :
   (shiftFunctor _ y).mapHomologicalComplex _
 
 variable {C}
-variable (K : HomologicalComplex₂ C (up ℤ) (up ℤ))
+variable (K L : HomologicalComplex₂ C (up ℤ) (up ℤ)) (f : K ⟶ L)
+
+/-- The isomorphism `(((shiftFunctor₁ C x).obj K).X a).X b ≅ (K.X a').X b` when `a' = a + x`. -/
+def shiftFunctor₁XXIso (a x a' : ℤ) (h : a' = a + x) (b : ℤ) :
+    (((shiftFunctor₁ C x).obj K).X a).X b ≅ (K.X a').X b := eqToIso (by subst h; rfl)
+
+/-- The isomorphism `(((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b'` when `b' = b + y`. -/
+def shiftFunctor₂XXIso (a b y b' : ℤ) (h : b' = b + y) :
+    (((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b' := eqToIso (by subst h; rfl)
+
+@[simp]
+lemma shiftFunctor₁XXIso_refl (a b x : ℤ) :
+    K.shiftFunctor₁XXIso a x (a + x) rfl b = Iso.refl _ := rfl
+
+@[simp]
+lemma shiftFunctor₂XXIso_refl (a b y : ℤ) :
+    K.shiftFunctor₂XXIso a b y (b + y) rfl = Iso.refl _ := rfl
 
-section
+variable (x y : ℤ) [K.HasTotal (up ℤ)]
 
-variable (x : ℤ) [K.HasTotal (up ℤ)] [((shiftFunctor₁ C x).obj K).HasTotal (up ℤ)]
+instance : ((shiftFunctor₁ C x).obj K).HasTotal (up ℤ) := fun n =>
+  hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (π (up ℤ) (up ℤ) (up ℤ)) (n + x)) _
+    { toFun := fun ⟨⟨a, b⟩, h⟩ => ⟨⟨a + x, b⟩, by
+        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        omega⟩
+      invFun := fun ⟨⟨a, b⟩, h⟩ => ⟨(a - x, b), by
+        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        omega⟩
+      left_inv := by
+        rintro ⟨⟨a, b⟩, h⟩
+        ext
+        · dsimp
+          omega
+        · rfl
+      right_inv := by
+        intro ⟨⟨a, b⟩, h⟩
+        ext
+        · dsimp
+          omega
+        · rfl }
+    (fun _ => Iso.refl _)
+
+instance : ((shiftFunctor₂ C y).obj K).HasTotal (up ℤ) := fun n =>
+  hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (π (up ℤ) (up ℤ) (up ℤ)) (n + y)) _
+    { toFun := fun ⟨⟨a, b⟩, h⟩ => ⟨⟨a, b + y⟩, by
+        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        omega⟩
+      invFun := fun ⟨⟨a, b⟩, h⟩ => ⟨(a, b - y), by
+        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        omega⟩
+      left_inv := by
+        rintro ⟨⟨a, b⟩, h⟩
+        ext
+        · rfl
+        · dsimp
+          omega
+      right_inv := by
+        intro ⟨⟨a, b⟩, h⟩
+        ext
+        · rfl
+        · dsimp
+          omega }
+    (fun _ => Iso.refl _)
+
+instance : ((shiftFunctor₂ C y ⋙ shiftFunctor₁ C x).obj K).HasTotal (up ℤ) := by
+  dsimp
+  infer_instance
+
+instance : ((shiftFunctor₁ C x ⋙ shiftFunctor₂ C y).obj K).HasTotal (up ℤ) := by
+  dsimp
+  infer_instance
 
 /-- Auxiliary definition for `totalShift₁Iso`. -/
 noncomputable def totalShift₁XIso (n n' : ℤ) (h : n + x = n') :
@@ -127,11 +192,40 @@ noncomputable def totalShift₁Iso :
         Linear.comp_units_smul, K.D₁_totalShift₁XIso_hom x n n' _ _ rfl rfl,
         K.D₂_totalShift₁XIso_hom x n n' _ _ rfl rfl])
 
-end
+@[reassoc]
+lemma ι_totalShift₁Iso_hom_f (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x)
+    (n' : ℤ) (hn' : n' = n + x) :
+    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n =
+      (K.shiftFunctor₁XXIso a x a' ha' b).hom ≫ K.ιTotal (up ℤ) a' b n' (by dsimp; omega) ≫
+        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv := by
+  subst ha' hn'
+  simp [totalShift₁Iso, totalShift₁XIso]
 
-section
+@[reassoc]
+lemma ι_totalShift₁Iso_inv_f (a b n : ℤ) (h : a + b = n) (a' n' : ℤ)
+    (ha' : a' + b = n') (hn' : n' = n + x) :
+    K.ιTotal (up ℤ) a' b n' ha' ≫
+      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv ≫
+        (K.totalShift₁Iso x).inv.f n =
+      (K.shiftFunctor₁XXIso a x a' (by omega) b).inv ≫
+        ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h := by
+  subst hn'
+  obtain rfl : a = a' - x := by omega
+  dsimp [totalShift₁Iso, totalShift₁XIso, shiftFunctor₁XXIso, XXIsoOfEq]
+  simp only [id_comp, ι_totalDesc]
 
-variable (y : ℤ) [K.HasTotal (up ℤ)] [((shiftFunctor₂ C y).obj K).HasTotal (up ℤ)]
+variable {K L} in
+@[reassoc]
+lemma totalShift₁Iso_hom_naturality [L.HasTotal (up ℤ)] :
+    total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom =
+      (K.totalShift₁Iso x).hom ≫ (total.map f (up ℤ))⟦x⟧' := by
+  ext n i₁ i₂ h
+  dsimp at h
+  dsimp
+  rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
+    K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]
+  dsimp
+  rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
 
 attribute [local simp] smul_smul
 
@@ -199,7 +293,7 @@ lemma D₂_totalShift₂XIso_hom (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y
 
 /-- The isomorphism `((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧`
 expressing the compatibility of the total complex with the shift on the second indices.
-This isomorphism involves signs: in the summand in degree `(p, q)` of `K`, it is given by the
+This isomorphism involves signs: on the summand in degree `(p, q)` of `K`, it is given by the
 multiplication by `(p * y).negOnePow`. -/
 noncomputable def totalShift₂Iso :
     ((shiftFunctor₂ C y).obj K).total (up ℤ) ≅ (K.total (up ℤ))⟦y⟧ :=
@@ -210,6 +304,84 @@ noncomputable def totalShift₂Iso :
         Linear.comp_units_smul, K.D₁_totalShift₂XIso_hom y n n' _ _ rfl rfl,
         K.D₂_totalShift₂XIso_hom y n n' _ _ rfl rfl])
 
-end
+@[reassoc]
+lemma ι_totalShift₂Iso_hom_f (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y)
+    (n' : ℤ) (hn' : n' = n + y) :
+    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
+      (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
+        K.ιTotal (up ℤ) a b' n' (by dsimp; omega) ≫
+          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv := by
+  subst hb' hn'
+  simp [totalShift₂Iso, totalShift₂XIso]
+
+@[reassoc]
+lemma ι_totalShift₂Iso_inv_f (a b n : ℤ) (h : a + b = n) (b' n' : ℤ)
+    (hb' : a + b' = n') (hn' : n' = n + y) :
+    K.ιTotal (up ℤ) a b' n' hb' ≫
+      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫
+        (K.totalShift₂Iso y).inv.f n =
+      (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' (by omega)).inv ≫
+        ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h := by
+  subst hn'
+  obtain rfl : b = b' - y := by omega
+  dsimp [totalShift₂Iso, totalShift₂XIso, shiftFunctor₂XXIso, XXIsoOfEq]
+  simp only [id_comp, ι_totalDesc]
+
+variable {K L} in
+@[reassoc]
+lemma totalShift₂Iso_hom_naturality [L.HasTotal (up ℤ)] :
+    total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom =
+      (K.totalShift₂Iso y).hom ≫ (total.map f (up ℤ))⟦y⟧' := by
+  ext n i₁ i₂ h
+  dsimp at h
+  dsimp
+  rw [ιTotal_map_assoc, L.ι_totalShift₂Iso_hom_f y i₁ i₂ n h _ rfl _ rfl,
+    K.ι_totalShift₂Iso_hom_f_assoc y i₁ i₂ n h _ rfl _ rfl]
+  dsimp
+  rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
+    Linear.units_smul_comp, ιTotal_map]
+
+variable (C) in
+/-- The shift functors `shiftFunctor₁ C x` and `shiftFunctor₂ C y` on bicomplexes
+with respect to both variables commute. -/
+def shiftFunctor₁₂CommIso (x y : ℤ) :
+    shiftFunctor₂ C y ⋙ shiftFunctor₁ C x ≅ shiftFunctor₁ C x ⋙ shiftFunctor₂ C y :=
+  Iso.refl _
+
+/-- The compatibility isomorphisms of the total complex with the shifts
+in both variables "commute" only up to a sign `(x * y).negOnePow`. -/
+lemma totalShift₁Iso_trans_totalShift₂Iso :
+    ((shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫
+      (shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) =
+    (x * y).negOnePow • (total.mapIso ((shiftFunctor₁₂CommIso C x y).app K) (up ℤ)) ≪≫
+      ((shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫
+      (shiftFunctor _ y).mapIso (K.totalShift₁Iso x) ≪≫
+      (shiftFunctorComm (CochainComplex C ℤ) x y).app _ := by
+  ext n n₁ n₂ h
+  dsimp at h ⊢
+  rw [Linear.comp_units_smul,ι_totalShift₁Iso_hom_f_assoc _ x n₁ n₂ n h _ rfl _ rfl,
+    ιTotal_map_assoc, ι_totalShift₂Iso_hom_f_assoc _ y n₁ n₂ n h _ rfl _ rfl,
+    Linear.units_smul_comp, Linear.comp_units_smul]
+  dsimp [shiftFunctor₁₂CommIso]
+  rw [id_comp, id_comp, id_comp, id_comp, comp_id,
+    ι_totalShift₂Iso_hom_f _ y (n₁ + x) n₂ (n + x) (by omega) _ rfl _ rfl, smul_smul,
+    ← Int.negOnePow_add, add_mul, add_comm (x * y)]
+  dsimp
+  rw [id_comp, comp_id,
+    ι_totalShift₁Iso_hom_f_assoc _ x n₁ (n₂ + y) (n + y) (by omega) _ rfl (n + x + y) (by omega),
+    CochainComplex.shiftFunctorComm_hom_app_f]
+  dsimp
+  rw [Iso.inv_hom_id, comp_id, id_comp]
+
+/-- The compatibility isomorphisms of the total complex with the shifts
+in both variables "commute" only up to a sign `(x * y).negOnePow`. -/
+@[reassoc]
+lemma totalShift₁Iso_hom_totalShift₂Iso_hom :
+    (((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom ≫ (K.totalShift₂Iso y).hom⟦x⟧' =
+      (x * y).negOnePow • (total.map ((shiftFunctor₁₂CommIso C x y).hom.app K) (up ℤ) ≫
+          (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom ≫
+          (K.totalShift₁Iso x).hom⟦y⟧' ≫
+          (shiftFunctorComm (CochainComplex C ℤ) x y).hom.app _) :=
+  congr_arg Iso.hom (totalShift₁Iso_trans_totalShift₂Iso K x y)
 
 end HomologicalComplex₂

Mathlib/CategoryTheory/GradedObject.lean

@@ -285,6 +285,12 @@ variable (j : J)
 for all `j : J`, the coproduct of all `X i` such `p i = j` exists. -/
 abbrev HasMap : Prop := ∀ (j : J), HasCoproduct (X.mapObjFun p j)
 
+variable {X Y} in
+lemma hasMap_of_iso [HasMap X p] : HasMap Y p := fun j => by
+  have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
+    Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)
+  exact hasColimitOfIso α.symm
+
 variable [X.HasMap p] [Y.HasMap p] [Z.HasMap p]
 
 /-- Given `X : GradedObject I C` and `p : I → J`, `X.mapObj p` is the graded object by `J`

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -102,6 +102,22 @@ abbrev HasCoproduct (f : β → C) :=
   HasColimit (Discrete.functor f)
 #align category_theory.limits.has_coproduct CategoryTheory.Limits.HasCoproduct
 
+lemma hasCoproduct_of_equiv_of_iso (f : α → C) (g : β → C)
+    [HasCoproduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasCoproduct g := by
+  have : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
+    hasColimit_equivalence_comp _
+  have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
+    Discrete.natIso (fun ⟨j⟩ => iso j)
+  exact hasColimitOfIso α
+
+lemma hasProduct_of_equiv_of_iso (f : α → C) (g : β → C)
+    [HasProduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasProduct g := by
+  have : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
+    hasLimitEquivalenceComp _
+  have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
+    Discrete.natIso (fun ⟨j⟩ => iso j)
+  exact hasLimitOfIso α.symm
+
 /-- Make a fan `f` into a limit fan by providing `lift`, `fac`, and `uniq` --
   just a convenience lemma to avoid having to go through `Discrete` -/
 @[simps]