feat: functors which preserve homology (#7197)

Author: joelriou

Mathlib.lean

@@ -247,6 +247,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Homology
 import Mathlib.Algebra.Homology.ShortComplex.LeftHomology
 import Mathlib.Algebra.Homology.ShortComplex.Limits
 import Mathlib.Algebra.Homology.ShortComplex.Preadditive
+import Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
 import Mathlib.Algebra.Homology.ShortComplex.RightHomology
 import Mathlib.Algebra.Homology.ShortExact.Abelian
 import Mathlib.Algebra.Homology.ShortExact.Preadditive

Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2023 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.ShortComplex.Homology
+import Mathlib.CategoryTheory.Limits.Preserves.Finite
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
+
+/-!
+# Functors which preserves homology
+
+If `F : C ⥤ D` is a functor between categories with zero morphisms, we shall
+say that `F` preserves homology when `F` preserves both kernels and cokernels.
+This typeclass is named `[F.PreservesHomology]`, and is automatically
+satisfied when `F` preserves both finite limits and finite colimits.
+
+TODO: If `S : ShortComplex C` and `[F.PreservesHomology]`, then there is an
+isomorphism `S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology`.
+
+-/
+
+namespace CategoryTheory
+
+open Category Limits
+
+variable {C D : Type*} [Category C] [Category D] [HasZeroMorphisms C] [HasZeroMorphisms D]
+
+namespace Functor
+
+variable (F : C ⥤ D)
+
+/-- A functor preserves homology when it preserves both kernels and cokernels. -/
+class PreservesHomology (F : C ⥤ D) [PreservesZeroMorphisms F] where
+  /-- the functor preserves kernels -/
+  preservesKernels ⦃X Y : C⦄ (f : X ⟶ Y) : PreservesLimit (parallelPair f 0) F :=
+    by infer_instance
+  /-- the functor preserves cokernels -/
+  preservesCokernels ⦃X Y : C⦄ (f : X ⟶ Y) : PreservesColimit (parallelPair f 0) F :=
+    by infer_instance
+
+variable [PreservesZeroMorphisms F]
+
+/-- A functor which preserves homology preserves kernels. -/
+def PreservesHomology.preservesKernel [F.PreservesHomology] {X Y : C} (f : X ⟶ Y) :
+    PreservesLimit (parallelPair f 0) F :=
+  PreservesHomology.preservesKernels _
+
+/-- A functor which preserves homology preserves cokernels. -/
+def PreservesHomology.preservesCokernel [F.PreservesHomology] {X Y : C} (f : X ⟶ Y) :
+    PreservesColimit (parallelPair f 0) F :=
+  PreservesHomology.preservesCokernels _
+
+noncomputable instance preservesHomologyOfExact
+    [PreservesFiniteLimits F] [PreservesFiniteColimits F] :
+  F.PreservesHomology where
+
+end Functor
+
+namespace ShortComplex
+
+variable {S S₁ S₂ : ShortComplex C}
+
+namespace LeftHomologyData
+
+variable (h : S.LeftHomologyData) (F : C ⥤ D)
+
+/-- A left homology data `h` of a short complex `S` is preserved by a functor `F` is
+`F` preserves the kernel of `S.g : S.X₂ ⟶ S.X₃` and the cokernel of `h.f' : S.X₁ ⟶ h.K`. -/
+class IsPreservedBy [F.PreservesZeroMorphisms] where
+  /-- the functor preserves the kernel of `S.g : S.X₂ ⟶ S.X₃`. -/
+  g : PreservesLimit (parallelPair S.g 0) F
+  /-- the functor preserves the cokernel of `h.f' : S.X₁ ⟶ h.K`. -/
+  f' : PreservesColimit (parallelPair h.f' 0) F
+
+variable [F.PreservesZeroMorphisms]
+
+noncomputable instance isPreservedByOfPreservesHomology [F.PreservesHomology] :
+    h.IsPreservedBy F where
+  g := Functor.PreservesHomology.preservesKernel _ _
+  f' := Functor.PreservesHomology.preservesCokernel _ _
+
+variable [h.IsPreservedBy F]
+
+/-- When a left homology data is preserved by a functor `F`, this functor
+preserves the kernel of `S.g : S.X₂ ⟶ S.X₃`. -/
+def IsPreservedBy.hg : PreservesLimit (parallelPair S.g 0) F :=
+  @IsPreservedBy.g _ _ _ _ _ _ _ h F _ _
+
+/-- When a left homology data `h` is preserved by a functor `F`, this functor
+preserves the cokernel of `h.f' : S.X₁ ⟶ h.K`. -/
+def IsPreservedBy.hf' : PreservesColimit (parallelPair h.f' 0) F := IsPreservedBy.f'
+
+/-- When a left homology data `h` of a short complex `S` is preserved by a functor `F`,
+this is the induced left homology data `h.map F` for the short complex `S.map F`. -/
+@[simps]
+noncomputable def map : (S.map F).LeftHomologyData := by
+  have := IsPreservedBy.hg h F
+  have := IsPreservedBy.hf' h F
+  have wi : F.map h.i ≫ F.map S.g = 0 := by rw [← F.map_comp, h.wi, F.map_zero]
+  have hi := KernelFork.mapIsLimit _ h.hi F
+  let f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f (S.map F).zero)
+  have hf' : f' = F.map h.f' := Fork.IsLimit.hom_ext hi (by
+    rw [Fork.IsLimit.lift_ι hi]
+    simp only [KernelFork.map_ι, Fork.ι_ofι, map_f, ← F.map_comp, f'_i])
+  have wπ : f' ≫ F.map h.π = 0 := by rw [hf', ← F.map_comp, f'_π, F.map_zero]
+  have hπ : IsColimit (CokernelCofork.ofπ (F.map h.π) wπ) := by
+    let e : parallelPair f' 0 ≅ parallelPair (F.map h.f') 0 :=
+      parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hf') (by simp)
+    refine' IsColimit.precomposeInvEquiv e _
+      (IsColimit.ofIsoColimit (CokernelCofork.mapIsColimit _ h.hπ' F) _)
+    exact Cofork.ext (Iso.refl _) (by simp)
+  exact
+    { K := F.obj h.K
+      H := F.obj h.H
+      i := F.map h.i
+      π := F.map h.π
+      wi := wi
+      hi := hi
+      wπ := wπ
+      hπ := hπ }
+
+@[simp]
+lemma map_f' : (h.map F).f' = F.map h.f' := by
+  rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]
+
+end LeftHomologyData
+
+/-- Given a left homology map data `ψ : LeftHomologyMapData φ h₁ h₂` such that
+both left homology data `h₁` and `h₂` are preserved by a functor `F`, this is
+the induced left homology map data for the morphism `F.mapShortComplex.map φ`. -/
+@[simps]
+def LeftHomologyMapData.map {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData}
+    {h₂ : S₂.LeftHomologyData} (ψ : LeftHomologyMapData φ h₁ h₂) (F : C ⥤ D)
+    [F.PreservesZeroMorphisms] [h₁.IsPreservedBy F] [h₂.IsPreservedBy F] :
+    LeftHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F) where
+  φK := F.map ψ.φK
+  φH := F.map ψ.φH
+  commi := by simpa only [F.map_comp] using F.congr_map ψ.commi
+  commf' := by simpa only [LeftHomologyData.map_f', F.map_comp] using F.congr_map ψ.commf'
+  commπ := by simpa only [F.map_comp] using F.congr_map ψ.commπ
+
+end ShortComplex
+
+end CategoryTheory