feat(Algebra/Homology): extensions of bifunctors to complexes preserve homotopies (leanprover-community#32383)

Given a `TotalComplexShape c₁ c₂ c`, a functor `F : C₁ ⥤ C₂ ⥤ D`, we show in this PR that up to homotopy the morphism `mapBifunctorMap f₁ f₂ F c` only depends on the homotopy classes of the morphism `f₁` in `HomologicalComplex C c₁` and of the morphism `f₂` in `HomologicalComplex C c₂`.

(The case of `f₁` was already done, the case of `f₂` is obtained in this PR by symmetry.)

Author: joelriou

Mathlib/Algebra/Homology/BifunctorFlip.lean

@@ -29,7 +29,8 @@ namespace HomologicalComplex
 
 variable {I₁ I₂ J : Type*} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
   [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [Preadditive D]
-  (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
+  (K₁ L₁ : HomologicalComplex C₁ c₁) (φ₁ : K₁ ⟶ L₁)
+  (K₂ L₂ : HomologicalComplex C₂ c₂) (φ₂ : K₂ ⟶ L₂)
   (F : C₁ ⥤ C₂ ⥤ D) [F.PreservesZeroMorphisms] [∀ X₁, (F.obj X₁).PreservesZeroMorphisms]
   (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c]
   [TotalComplexShapeSymmetry c₁ c₂ c]
@@ -38,7 +39,7 @@ lemma hasMapBifunctor_flip_iff :
     HasMapBifunctor K₂ K₁ F.flip c ↔ HasMapBifunctor K₁ K₂ F c :=
   (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).flip_hasTotal_iff c
 
-variable [DecidableEq J] [HasMapBifunctor K₁ K₂ F c]
+variable [DecidableEq J] [HasMapBifunctor K₁ K₂ F c] [HasMapBifunctor L₁ L₂ F c]
 
 instance : HasMapBifunctor K₂ K₁ F.flip c := by
   rw [hasMapBifunctor_flip_iff]
@@ -49,9 +50,32 @@ noncomputable def mapBifunctorFlipIso :
     mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c :=
   (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalFlipIso c
 
+@[reassoc (attr := simp)]
+lemma ι_mapBifunctorFlipIso_hom (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₂.π c₁ c (i₂, i₁) = j) :
+    ιMapBifunctor K₂ K₁ F.flip c i₂ i₁ j hj ≫ (mapBifunctorFlipIso K₁ K₂ F c).hom.f j =
+      c₁.σ c₂ c i₁ i₂ • ιMapBifunctor K₁ K₂ F c i₁ i₂ j
+        (by rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]) :=
+  HomologicalComplex₂.ιTotal_totalFlipIso_f_hom
+    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂) c i₁ i₂ j hj
+
+@[reassoc (attr := simp)]
+lemma ι_mapBifunctorFlipIso_inv (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₁.π c₂ c (i₁, i₂) = j) :
+    ιMapBifunctor K₁ K₂ F c i₁ i₂ j hj ≫ (mapBifunctorFlipIso K₁ K₂ F c).inv.f j =
+      c₁.σ c₂ c i₁ i₂ • ιMapBifunctor K₂ K₁ F.flip c i₂ i₁ j
+        (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]) :=
+  HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
+    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂) c i₁ i₂ j hj
+
 lemma mapBifunctorFlipIso_flip
     [TotalComplexShapeSymmetry c₂ c₁ c] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c] :
     mapBifunctorFlipIso K₂ K₁ F.flip c = (mapBifunctorFlipIso K₁ K₂ F c).symm :=
   (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).flip_totalFlipIso c
 
+variable {K₁ K₂ L₁ L₂} in
+@[reassoc (attr := simp)]
+lemma mapBifunctorFlipIso_hom_naturality :
+      mapBifunctorMap φ₂ φ₁ F.flip c ≫ (mapBifunctorFlipIso L₁ L₂ F c).hom =
+    (mapBifunctorFlipIso K₁ K₂ F c).hom ≫ mapBifunctorMap φ₁ φ₂ F c := by
+  cat_disch
+
 end HomologicalComplex

Mathlib/Algebra/Homology/BifunctorHomotopy.lean

@@ -5,17 +5,17 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Homology.Bifunctor
+public import Mathlib.Algebra.Homology.BifunctorFlip
 public import Mathlib.Algebra.Homology.Homotopy
 
 /-!
 # The action of a bifunctor on homological complexes factors through homotopies
 
 Given a `TotalComplexShape c₁ c₂ c`, a functor `F : C₁ ⥤ C₂ ⥤ D`,
-we shall show in this file that up to homotopy the morphism
+we show in this file that up to homotopy the morphism
 `mapBifunctorMap f₁ f₂ F c` only depends on the homotopy classes of
 the morphism `f₁` in `HomologicalComplex C c₁` and of
-the morphism `f₂` in `HomologicalComplex C c₂` (TODO).
+the morphism `f₂` in `HomologicalComplex C c₂`.
 
 -/
 
@@ -32,11 +32,10 @@ variable {C₁ C₂ D I₁ I₂ J : Type*} [Category C₁] [Category C₂] [Cate
 namespace HomologicalComplex
 
 variable {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁')
-  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂)
+  {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ f₂' : K₂ ⟶ L₂) (h₂ : Homotopy f₂ f₂')
   (F : C₁ ⥤ C₂ ⥤ D) [F.Additive] [∀ X₁, (F.obj X₁).Additive]
   (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c]
-  [HasMapBifunctor K₁ K₂ F c]
-  [HasMapBifunctor L₁ L₂ F c]
+  [HasMapBifunctor K₁ K₂ F c] [HasMapBifunctor L₁ L₂ F c]
 
 namespace mapBifunctorMapHomotopy
 
@@ -57,6 +56,27 @@ lemma ιMapBifunctor_hom₁ (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J)
   subst h'
   simp [hom₁]
 
+variable (f₁) {f₂ f₂'} in
+/-- Auxiliary definition for `mapBifunctorMapHomotopy₂`. -/
+noncomputable def hom₂ (j j' : J) :
+    (mapBifunctor K₁ K₂ F c).X j ⟶ (mapBifunctor L₁ L₂ F c).X j' :=
+  HomologicalComplex₂.totalDesc _
+    (fun i₁ i₂ _ ↦ ComplexShape.ε₂ c₁ c₂ c (i₁, c₂.prev i₂) •
+      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫
+        (F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)) ≫
+          ιMapBifunctorOrZero L₁ L₂ F c _ _ j')
+
+variable (f₁) {f₂ f₂'} in
+@[reassoc]
+lemma ιMapBifunctor_hom₂ (i₁ : I₁) (i₂ i₂' : I₂) (j j' : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂') = j) (h' : c₂.prev i₂' = i₂) :
+    ιMapBifunctor K₁ K₂ F c i₁ i₂' j h ≫ hom₂ f₁ h₂ F c j j' =
+      ComplexShape.ε₂ c₁ c₂ c (i₁, i₂) •
+        (F.map (f₁.f i₁)).app (K₂.X i₂') ≫
+          (F.obj (L₁.X i₁)).map (h₂.hom i₂' i₂) ≫ ιMapBifunctorOrZero L₁ L₂ F c i₁ i₂ j' := by
+  subst h'
+  simp [hom₂]
+
 lemma zero₁ (j j' : J) (h : ¬ c.Rel j' j) :
     hom₁ h₁ f₂ F c j j' = 0 := by
   ext i₁ i₂ h'
@@ -158,4 +178,47 @@ noncomputable def mapBifunctorMapHomotopy₁ :
   zero := zero₁ h₁ f₂ F c
   comm := comm₁ h₁ f₂ F c
 
+variable (f₁) {f₂ f₂'} in
+open mapBifunctorMapHomotopy in
+/-- The homotopy between `mapBifunctorMap f₁ f₂ F c` and `mapBifunctorMap f₁ f₂' F c` that
+is induced by a homotopy between `f₂` and `f₂'`. -/
+noncomputable def mapBifunctorMapHomotopy₂ :
+    Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
+  letI : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
+  letI : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
+  haveI : F.flip.Additive := { }
+  haveI (X₁ : C₂) : (F.flip.obj X₁).Additive := { }
+  letI H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
+    (Homotopy.ofEq (by simp)).trans
+      ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight
+        (mapBifunctorFlipIso L₁ L₂ F c).hom).compLeft
+          ((mapBifunctorFlipIso K₁ K₂ F c).inv)).trans (Homotopy.ofEq (by simp)))
+  haveI hom₂_eq : hom₂ f₁ h₂ F c = H.hom := by
+    ext j j' i₁ i₂ hj
+    dsimp [H, mapBifunctorMapHomotopy₁]
+    rw [add_zero, zero_add, ι_mapBifunctorFlipIso_inv_assoc, Linear.units_smul_comp,
+      ιMapBifunctor_hom₁_assoc h₂ f₁ F.flip c _ i₂ i₁ j j'
+        (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]) rfl,
+      ιMapBifunctor_hom₂ f₁ h₂ F c i₁ _ i₂ j j' hj rfl]
+    dsimp
+    simp only [NatTrans.naturality_assoc, Linear.units_smul_comp, assoc]
+    by_cases hj' : c₁.π c₂ c (i₁, c₂.prev i₂) = j'
+    · rw [ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ hj',
+        ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ (by rwa [ComplexShape.π_symm c₁ c₂ c]),
+        ι_mapBifunctorFlipIso_hom, Linear.comp_units_smul, Linear.comp_units_smul,
+        smul_smul, smul_smul]
+      by_cases hi₂ : c₂.Rel (c₂.prev i₂) i₂
+      · congr 1
+        nth_rw 2 [mul_comm]
+        rw [← ComplexShape.σ_ε₂ c₁ c i₁ hi₂, mul_comm, ← mul_assoc,
+          Int.units_mul_self, one_mul]
+      · rw [h₂.zero _ _ hi₂, Functor.map_zero, zero_comp, comp_zero, smul_zero, smul_zero]
+    · rw [ιMapBifunctorOrZero_eq_zero _ _ _ _ _ _ _ hj',
+        ιMapBifunctorOrZero_eq_zero _ _ _ _ _ _ _ (by rwa [ComplexShape.π_symm c₁ c₂ c]),
+        comp_zero, comp_zero, smul_zero, zero_comp, comp_zero,
+        comp_zero, smul_zero, smul_zero]
+  { hom := hom₂ f₁ h₂ F c
+    zero j j' h := by simpa only [hom₂_eq] using H.zero j j' h
+    comm j := by simpa only [hom₂_eq] using H.comm j }
+
 end HomologicalComplex

Mathlib/Algebra/Homology/ComplexShapeSigns.lean

@@ -270,6 +270,18 @@ instance {I : Type*} [AddMonoid I] (c : ComplexShape I) [c.TensorSigns] :
 
 end ComplexShape
 
+/-- The total complex shape for `c₂`, `c₁` and `c₁₂` that is deduced
+from a total complex shape for `c₁`, `c₂` and `c₁₂`. -/
+def TotalComplexShape.symm [TotalComplexShape c₁ c₂ c₁₂] :
+    TotalComplexShape c₂ c₁ c₁₂ where
+  π := fun ⟨i₂, i₁⟩ ↦ ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩
+  ε₁ := fun ⟨i₂, i₁⟩ ↦ ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩
+  ε₂ := fun ⟨i₂, i₁⟩ ↦ ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩
+  rel₁ h i₁ := ComplexShape.rel_π₂ c₁ c₁₂ i₁ h
+  rel₂ i₂ _ _ h := ComplexShape.rel_π₁ c₂ c₁₂ h i₂
+  ε₂_ε₁ h₂ h₁ := by
+    rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]
+
 /-- A total complex shape symmetry contains the data and properties which allow the
 identification of the two total complex functors
 `HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂`
@@ -283,6 +295,17 @@ class TotalComplexShapeSymmetry [TotalComplexShape c₁ c₂ c₁₂] [TotalComp
   σ_ε₂ (i₁ : I₁) {i₂ i₂' : I₂} (h₂ : c₂.Rel i₂ i₂') :
     σ i₁ i₂ * ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = ComplexShape.ε₁ c₂ c₁ c₁₂ ⟨i₂, i₁⟩ * σ i₁ i₂'
 
+/-- The symmetry between the total complex shape for `c₁`, `c₂` and `c₁₂`,
+and its symmetric total complex shape. -/
+def TotalComplexShape.symmSymmetry [TotalComplexShape c₁ c₂ c₁₂] :
+    letI := TotalComplexShape.symm c₁ c₂ c₁₂
+    TotalComplexShapeSymmetry c₁ c₂ c₁₂ :=
+  letI := TotalComplexShape.symm c₁ c₂ c₁₂
+  { symm i₁ i₂ := rfl
+    σ _ _ := 1
+    σ_ε₁ _ _ := by aesop
+    σ_ε₂ _ _ := by aesop }
+
 namespace ComplexShape
 
 variable [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₂ c₁ c₁₂]