feat(Algebra/Homology): the action of a bifunctor on homological comp…

…lexes (#10764)

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

Mathlib.lean

@@ -241,6 +241,7 @@ import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.HierarchyDesign
 import Mathlib.Algebra.Homology.Additive
 import Mathlib.Algebra.Homology.Augment
+import Mathlib.Algebra.Homology.Bifunctor
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.Algebra.Homology.ComplexShapeSigns
 import Mathlib.Algebra.Homology.ConcreteCategory

Mathlib/Algebra/Homology/Bifunctor.lean

@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.TotalComplex
+import Mathlib.CategoryTheory.GradedObject.Bifunctor
+
+/-!
+# The action of a bifunctor on homological complexes
+
+Given a bifunctor `F : C₁ ⥤ C₂ ⥤ D` and complexes shapes `c₁ : ComplexShape I₁` and
+`c₂ : ComplexShape I₂`, we define a bifunctor `mapBifunctorHomologicalComplex F c₁ c₂`
+of type `HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂`.
+
+Then, when `K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂` and
+`c : ComplexShape J` are such that we have `TotalComplexShape c₁ c₂ c`, we introduce
+a typeclass `HasMapBifunctor K₁ K₂ F c` which allows to define
+`mapBifunctor K₁ K₂ F c : HomologicalComplex D c` as the total complex of the
+bicomplex `(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂)`.
+
+-/
+
+open CategoryTheory Limits
+
+variable {C₁ C₂ D : Type*} [Category C₁] [Category C₂] [Category D]
+
+namespace CategoryTheory
+
+namespace Functor
+
+variable [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [HasZeroMorphisms D]
+  (F : C₁ ⥤ C₂ ⥤ D) {I₁ I₂ J : Type*} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
+  [F.PreservesZeroMorphisms] [∀ X₁, (F.obj X₁).PreservesZeroMorphisms]
+
+variable {c₁} in
+/-- Auxiliary definition for `mapBifunctorHomologicalComplex`. -/
+@[simps!]
+def mapBifunctorHomologicalComplexObj (K₁ : HomologicalComplex C₁ c₁) :
+    HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂ where
+  obj K₂ := HomologicalComplex₂.ofGradedObject c₁ c₂
+      (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
+      (fun i₁ i₁' i₂ => (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
+      (fun i₁ i₂ i₂' => (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))
+      (fun i₁ i₁' h₁ i₂ => by
+        dsimp
+        rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app])
+      (fun i₁ i₂ i₂' h₂ => by
+        dsimp
+        rw [K₂.shape _ _ h₂, Functor.map_zero])
+      (fun i₁ i₁' i₁'' i₂ => by
+        dsimp
+        rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
+          Functor.map_zero, zero_app])
+      (fun i₁ i₂ i₂' i₂'' => by
+        dsimp
+        rw [← Functor.map_comp, HomologicalComplex.d_comp_d, Functor.map_zero])
+      (fun i₁ i₁' i₂ i₂' => by
+        dsimp
+        rw [NatTrans.naturality])
+  map {K₂ K₂' φ} := HomologicalComplex₂.homMk
+      (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map φ.f) (by simp) (by
+        intros
+        dsimp
+        simp only [← Functor.map_comp, φ.comm])
+  map_id K₂ := by ext; dsimp; rw [Functor.map_id]
+  map_comp f g := by ext; dsimp; rw [Functor.map_comp]
+
+/-- Given a functor `F : C₁ ⥤ C₂ ⥤ D`, this is the bifunctor which sends
+`K₁ : HomologicalComplex C₁ c₁` and `K₂ : HomologicalComplex C₂ c₂` to the bicomplex
+which is degree `(i₁, i₂)` consists of `(F.obj (K₁.X i₁)).obj (K₂.X i₂)`. -/
+@[simps! obj_obj_X_X obj_obj_X_d obj_obj_d_f obj_map_f_f map_app_f_f]
+def mapBifunctorHomologicalComplex :
+    HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂ where
+  obj := mapBifunctorHomologicalComplexObj F c₂
+  map {K₁ K₁'} f :=
+    { app := fun K₂ => HomologicalComplex₂.homMk
+        (((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X) (by
+          intros
+          dsimp
+          simp only [← NatTrans.comp_app, ← F.map_comp, f.comm]) (by simp) }
+
+variable {c₁ c₂}
+
+@[simp]
+lemma mapBifunctorHomologicalComplex_obj_obj_toGradedObject
+    (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) :
+    (((mapBifunctorHomologicalComplex F c₁ c₂).obj K₁).obj K₂).toGradedObject =
+      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X := rfl
+
+end Functor
+
+end CategoryTheory
+
+namespace HomologicalComplex
+
+variable {I₁ I₂ J : Type*} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
+  [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [Preadditive D]
+  (K₁ L₁ : HomologicalComplex C₁ c₁) (K₂ L₂ : HomologicalComplex C₂ c₂)
+  (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂)
+  (F : C₁ ⥤ C₂ ⥤ D) [F.PreservesZeroMorphisms] [∀ X₁, (F.obj X₁).PreservesZeroMorphisms]
+  (c : ComplexShape J) [TotalComplexShape c₁ c₂ c]
+
+/-- The condition that `((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂` has
+a total complex. -/
+abbrev HasMapBifunctor := (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).HasTotal c
+
+variable [HasMapBifunctor K₁ K₂ F c] [HasMapBifunctor L₁ L₂ F c] [DecidableEq J]
+
+/-- Given `K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂`,
+a bifunctor `F : C₁ ⥤ C₂ ⥤ D` and a complex shape `ComplexShape J` such that we have
+`[TotalComplexShape c₁ c₂ c]`, this `mapBifunctor K₁ K₂ F c : HomologicalComplex D c`
+is the total complex of the bicomplex obtained by applying `F` to `K₁` and `K₂`. -/
+noncomputable abbrev mapBifunctor : HomologicalComplex D c :=
+  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).total c
+
+/-- The inclusion of a summand of `(mapBifunctor K₁ K₂ F c).X j`. -/
+noncomputable abbrev ιMapBifunctor
+    (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (mapBifunctor K₁ K₂ F c).X j :=
+  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h
+
+/-- The inclusion of a summand of `(mapBifunctor K₁ K₂ F c).X j`, or zero. -/
+noncomputable abbrev ιMapBifunctorOrZero (i₁ : I₁) (i₂ : I₂) (j : J) :
+    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (mapBifunctor K₁ K₂ F c).X j :=
+  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotalOrZero c i₁ i₂ j
+
+lemma ιMapBifunctorOrZero_eq (i₁ : I₁) (i₂ : I₂) (j : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂ j = ιMapBifunctor K₁ K₂ F c i₁ i₂ j h := dif_pos h
+
+lemma ιMapBifunctorOrZero_eq_zero (i₁ : I₁) (i₂ : I₂) (j : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) ≠ j) :
+    ιMapBifunctorOrZero K₁ K₂ F c i₁ i₂ j = 0 := dif_neg h
+
+section
+
+variable {K₁ K₂ L₁ L₂}
+
+/-- The morphism `mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c` induced by
+morphisms of complexes `K₁ ⟶ L₁` and `K₂ ⟶ L₂`. -/
+noncomputable def mapBifunctorMap : mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c :=
+  HomologicalComplex₂.total.map (((F.mapBifunctorHomologicalComplex c₁ c₂).map f₁).app K₂ ≫
+    ((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).map f₂) c
+
+@[reassoc (attr := simp)]
+lemma ι_mapBifunctorMap (i₁ : I₁) (i₂ : I₂) (j : J)
+    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
+    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j =
+      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
+        ιMapBifunctor L₁ L₂ F c i₁ i₂ j h := by
+  simp [mapBifunctorMap]
+
+end
+
+end HomologicalComplex

Mathlib/Algebra/Homology/HomologicalBicomplex.lean

@@ -68,6 +68,61 @@ instance : Faithful (toGradedObjectFunctor C c₁ c₂) where
     ext i₁ i₂
     exact congr_fun h ⟨i₁, i₂⟩
 
+section OfGradedObject
+
+variable (c₁ c₂)
+variable (X : GradedObject (I₁ × I₂) C)
+    (d₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), X ⟨i₁, i₂⟩ ⟶ X ⟨i₁', i₂⟩)
+    (d₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), X ⟨i₁, i₂⟩ ⟶ X ⟨i₁, i₂'⟩)
+    (shape₁ : ∀ (i₁ i₁' : I₁) (_ : ¬c₁.Rel i₁ i₁') (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
+    (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂) (_ : ¬c₂.Rel i₂ i₂'), d₂ i₁ i₂ i₂' = 0)
+    (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0)
+    (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0)
+    (comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' =
+      d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂')
+
+/-- Constructor for bicomplexes taking as inputs a graded object, horizontal differentials
+and vertical differentials satisfying suitable relations. -/
+@[simps]
+def ofGradedObject :
+    HomologicalComplex₂ C c₁ c₂ where
+  X i₁ :=
+    { X := fun i₂ => X ⟨i₁, i₂⟩
+      d := fun i₂ i₂' => d₂ i₁ i₂ i₂'
+      shape := shape₂ i₁
+      d_comp_d' := by intros; apply d₂_comp_d₂ }
+  d i₁ i₁' :=
+    { f := fun i₂ => d₁ i₁ i₁' i₂
+      comm' := by intros; apply comm }
+  shape i₁ i₁' h := by
+    ext i₂
+    exact shape₁ i₁ i₁' h i₂
+  d_comp_d' i₁ i₁' i₁'' _ _ := by ext i₂; apply d₁_comp_d₁
+
+@[simp]
+lemma ofGradedObject_toGradedObject :
+    (ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X :=
+  rfl
+
+end OfGradedObject
+
+/-- Constructor for a morphism `K ⟶ L` in the category `HomologicalComplex₂ C c₁ c₂` which
+takes as inputs a morphism `f : K.toGradedObject ⟶ L.toGradedObject` and
+the compatibilites with both horizontal and vertical differentials. -/
+@[simps!]
+def homMk {K L : HomologicalComplex₂ C c₁ c₂}
+    (f : K.toGradedObject ⟶ L.toGradedObject)
+    (comm₁ : ∀ i₁ i₁' i₂, c₁.Rel i₁ i₁' →
+      f ⟨i₁, i₂⟩ ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f ⟨i₁', i₂⟩)
+    (comm₂ : ∀ i₁ i₂ i₂', c₂.Rel i₂ i₂' →
+      f ⟨i₁, i₂⟩ ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f ⟨i₁, i₂'⟩) : K ⟶ L where
+  f i₁ :=
+    { f := fun i₂ => f ⟨i₁, i₂⟩
+      comm' := comm₂ i₁ }
+  comm' i₁ i₁' h₁ := by
+    ext i₂
+    exact comm₁ i₁ i₁' i₂ h₁
+
 lemma shape_f (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (h : ¬ c₁.Rel i₁ i₁') (i₂ : I₂) :
     (K.d i₁ i₁').f i₂ = 0 := by
   rw [K.shape _ _ h, zero_f]