From ecd2ff7c97ed5bdc8c1446a3d6c7b96ab28b2d72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sat, 8 Jun 2024 04:33:26 +0000 Subject: [PATCH] feat(Algebra/Homology): commutation up to signs of the compatibility isomorphisms of the total complex with shifts in both variables (#11517) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 57 ++++- Mathlib/Algebra/Homology/TotalComplex.lean | 6 + .../Algebra/Homology/TotalComplexShift.lean | 200 ++++++++++++++++-- Mathlib/CategoryTheory/GradedObject.lean | 6 + .../Limits/Shapes/Products.lean | 16 ++ 5 files changed, 260 insertions(+), 25 deletions(-) diff --git a/Mathlib/Algebra/Homology/BifunctorShift.lean b/Mathlib/Algebra/Homology/BifunctorShift.lean index 635b815cdf833..4f6b9ee6aabb4 100644 --- a/Mathlib/Algebra/Homology/BifunctorShift.lean +++ b/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,12 +86,10 @@ 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 @@ -96,6 +97,9 @@ def mapBifunctorHomologicalComplexShift₂Iso : 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 diff --git a/Mathlib/Algebra/Homology/TotalComplex.lean b/Mathlib/Algebra/Homology/TotalComplex.lean index b03a9fcf7c592..7bb57bddef5e1 100644 --- a/Mathlib/Algebra/Homology/TotalComplex.lean +++ b/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 diff --git a/Mathlib/Algebra/Homology/TotalComplexShift.lean b/Mathlib/Algebra/Homology/TotalComplexShift.lean index 9156a8e18de1c..320dda9418c3e 100644 --- a/Mathlib/Algebra/Homology/TotalComplexShift.lean +++ b/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₂ diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean index 0a4d74cb14788..7afd61ef0f919 100644 --- a/Mathlib/CategoryTheory/GradedObject.lean +++ b/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` diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean index ed616768e9018..b3650cdfde2f0 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean +++ b/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]