From ca26a2ccbe64e39ecef9fd2ba4e686ea2af85777 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 7 Apr 2024 23:15:00 +0000 Subject: [PATCH] feat(Algebra/Homology): action of a bifunctor on cochain complexes and shifts (#10880) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In this PR, we introduce the abbreviation `CochainComplex.mapBifunctor K₁ K₂ F` for `K₁` and `K₂` two cochain complexes, and `F` a bifunctor. We obtain isomorphisms which express the behavior of this construction with respect to shifts on both variables: `mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧` and `mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- Mathlib.lean | 1 + Mathlib/Algebra/Homology/BifunctorShift.lean | 110 ++++++++++++++++++ Mathlib/Algebra/Homology/TotalComplex.lean | 11 +- .../Preadditive/FunctorCategory.lean | 4 + 4 files changed, 125 insertions(+), 1 deletion(-) create mode 100644 Mathlib/Algebra/Homology/BifunctorShift.lean diff --git a/Mathlib.lean b/Mathlib.lean index c3d67dab7c9d9..bd516b605f44f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -247,6 +247,7 @@ import Mathlib.Algebra.Homology.Additive import Mathlib.Algebra.Homology.Augment import Mathlib.Algebra.Homology.Bifunctor import Mathlib.Algebra.Homology.BifunctorHomotopy +import Mathlib.Algebra.Homology.BifunctorShift import Mathlib.Algebra.Homology.ComplexShape import Mathlib.Algebra.Homology.ComplexShapeSigns import Mathlib.Algebra.Homology.ConcreteCategory diff --git a/Mathlib/Algebra/Homology/BifunctorShift.lean b/Mathlib/Algebra/Homology/BifunctorShift.lean new file mode 100644 index 0000000000000..635b815cdf833 --- /dev/null +++ b/Mathlib/Algebra/Homology/BifunctorShift.lean @@ -0,0 +1,110 @@ +/- +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.Bifunctor +import Mathlib.Algebra.Homology.TotalComplexShift + +/-! +# Behavior of the action of a bifunctor on cochain complexes with respect to shifts + +In this file, given cochain complexes `K₁ : CochainComplex C₁ ℤ`, `K₂ : CochainComplex C₂ ℤ` and +a functor `F : C₁ ⥤ C₂ ⥤ D`, we define an isomorphism of cochain complexes in `D`: +- `CochainComplex.mapBifunctorShift₁Iso K₁ K₂ F x` of type +`mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧` for `x : ℤ`. +- `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 + +-/ + +open CategoryTheory Limits + +variable {C₁ C₂ D : Type*} [Category C₁] [Category C₂] [Category D] + +namespace CochainComplex + +section + +variable [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] + (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ) [Preadditive D] + (F : C₁ ⥤ C₂ ⥤ D) [F.PreservesZeroMorphisms] + [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] + +/-- The condition that `((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂` has +a total cochain complex. -/ +abbrev HasMapBifunctor := HomologicalComplex.HasMapBifunctor K₁ K₂ F (ComplexShape.up ℤ) + +/-- Given `K₁ : CochainComplex C₁ ℤ`, `K₂ : CochainComplex C₂ ℤ`, +a bifunctor `F : C₁ ⥤ C₂ ⥤ D`, this `mapBifunctor K₁ K₂ F : CochainComplex D ℤ` +is the total complex of the bicomplex obtained by applying `F` to `K₁` and `K₂`. -/ +noncomputable abbrev mapBifunctor [HasMapBifunctor K₁ K₂ F] : CochainComplex D ℤ := + HomologicalComplex.mapBifunctor K₁ K₂ F (ComplexShape.up ℤ) + +/-- The inclusion of a summand `(F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n` +of the total cochain complex when `n₁ + n₂ = n`. -/ +noncomputable abbrev ιMapBifunctor [HasMapBifunctor K₁ K₂ F] (n₁ n₂ n : ℤ) (h : n₁ + n₂ = n) : + (F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n := + HomologicalComplex.ιMapBifunctor K₁ K₂ F _ _ _ _ h + +end + +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 ℤ)] + +/-- Auxiliary definition for `mapBifunctorShift₁Iso`. -/ +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 _) + +/-- The canonical isomorphism `mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧`. +This isomorphism does not involve signs. -/ +noncomputable def mapBifunctorShift₁Iso : + mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧ := + HomologicalComplex₂.total.mapIso (mapBifunctorHomologicalComplexShift₁Iso K₁ K₂ F x) _ ≪≫ + (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂).totalShift₁Iso x + +end + +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 ℤ)] + +/-- Auxiliary definition for `mapBifunctorShift₂Iso`. -/ +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 _)) + +/-- 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`. -/ +noncomputable def mapBifunctorShift₂Iso : + mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧ := + HomologicalComplex₂.total.mapIso + (mapBifunctorHomologicalComplexShift₂Iso K₁ K₂ F y) (ComplexShape.up ℤ) ≪≫ + (((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂).totalShift₂Iso y + +end + +end CochainComplex diff --git a/Mathlib/Algebra/Homology/TotalComplex.lean b/Mathlib/Algebra/Homology/TotalComplex.lean index ca76bff125df4..ba24b4e7d1542 100644 --- a/Mathlib/Algebra/Homology/TotalComplex.lean +++ b/Mathlib/Algebra/Homology/TotalComplex.lean @@ -30,7 +30,7 @@ namespace HomologicalComplex₂ variable {C : Type*} [Category C] [Preadditive C] {I₁ I₂ I₁₂ : Type*} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} - (K L M : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (ψ : L ⟶ M) + (K L M : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (e : K ≅ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [DecidableEq I₁₂] [TotalComplexShape c₁ c₂ c₁₂] @@ -404,6 +404,15 @@ lemma map_comp : map (φ ≫ ψ) c₁₂ = map φ c₁₂ ≫ map ψ c₁₂ := apply (HomologicalComplex.forget _ _).map_injective exact GradedObject.mapMap_comp (toGradedObjectMap φ) (toGradedObjectMap ψ) _ +/-- The isomorphism `K.total c₁₂ ≅ L.total c₁₂` of homological complexes induced +by an isomorphism of bicomplexes `K ≅ L`. -/ +@[simps] +noncomputable def mapIso : K.total c₁₂ ≅ L.total c₁₂ where + hom := map e.hom _ + inv := map e.inv _ + hom_inv_id := by rw [← map_comp, e.hom_inv_id, map_id] + inv_hom_id := by rw [← map_comp, e.inv_hom_id, map_id] + end total section diff --git a/Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean b/Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean index 1bec6979399f4..9cf1ffb0c34f3 100644 --- a/Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean @@ -122,6 +122,10 @@ theorem app_zsmul (X : C) (α : F ⟶ G) (n : ℤ) : (n • α).app X = n • α (appHom X : (F ⟶ G) →+ (F.obj X ⟶ G.obj X)).map_zsmul α n #align category_theory.nat_trans.app_zsmul CategoryTheory.NatTrans.app_zsmul +@[simp] +theorem app_units_zsmul (X : C) (α : F ⟶ G) (n : ℤˣ) : (n • α).app X = n • α.app X := by + apply app_zsmul + @[simp] theorem app_sum {ι : Type*} (s : Finset ι) (X : C) (α : ι → (F ⟶ G)) : (∑ i in s, α i).app X = ∑ i in s, (α i).app X := by