feat: the shift on the homotopy category of cochain complexes

joelriou · joelriou · commit 77883be26cf8 · 2023-09-09T10:52:24.000+02:00
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
@@ -3,25 +3,26 @@ 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.Additive
+import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.Algebra.GroupPower.NegOnePow
+import Mathlib.CategoryTheory.Shift.Quotient
 import Mathlib.Tactic.Linarith
 
 /-!
 # The shift on cochain complexes and on the homotopy category
 
-In this file, we show `[HasShift (CochainComplex C ℤ) ℤ]` for any preadditive
-category `C`.
-
-TODO: show `[HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ]`.
+In this file, we show that for any preadditive category `C`, the categories
+`CochainComplex C ℤ` and `HomotopyCategory C (ComplexShape.up ℤ)` are
+equipped with a shift by `ℤ`.
 
 -/
 
-universe v u
+universe v v' u u'
 
 open CategoryTheory
 
 variable (C : Type u) [Category.{v} C] [Preadditive C]
+  {D : Type u'} [Category.{v'} D] [Preadditive D]
 
 namespace CochainComplex
 
@@ -110,7 +111,7 @@ lemma shiftFunctor_map_f' {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n p : ℤ
 @[simp]
 lemma shiftFunctor_obj_d' (K : CochainComplex C ℤ) (n i j : ℤ) :
     ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j =
-      ((-1 : Units ℤ) ^ n : ℤ) • K.d _ _ := rfl
+      n.negOnePow • K.d _ _ := rfl
 
 lemma shiftFunctorAdd_inv_app_f (K : CochainComplex C ℤ) (a b n : ℤ) :
     ((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n =
@@ -184,3 +185,102 @@ lemma shiftFunctorComm_hom_app_f (K : CochainComplex C ℤ) (a b p : ℤ) :
   simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans]
 
 end CochainComplex
+
+
+namespace CategoryTheory
+
+open Category
+
+namespace Functor
+
+variable {C}
+variable (F : C ⥤ D) [F.Additive]
+
+attribute [local simp] Functor.map_zsmul
+
+/-- The commutation with the shift isomorphism for the functor on cochain complexes
+induced by an additive functor between preadditive categories. -/
+@[simps!]
+def mapCochainComplexShiftIso (n : ℤ) :
+    shiftFunctor _ n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ) ≅
+      F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor _ n :=
+  NatIso.ofComponents (fun K => HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _)
+    (by aesop_cat)) (fun _ => by ext; dsimp; rw [id_comp, comp_id])
+
+instance commShiftMapCochainComplex :
+    (F.mapHomologicalComplex (ComplexShape.up ℤ)).CommShift ℤ where
+  iso := F.mapCochainComplexShiftIso
+  zero := by
+    ext
+    rw [CommShift.isoZero_hom_app]
+    dsimp
+    simp only [mapCochainComplexShiftIso_hom_app_f, CochainComplex.shiftFunctorZero_inv_app_f,
+       CochainComplex.shiftFunctorZero_hom_app_f, HomologicalComplex.XIsoOfEq, eqToIso,
+       eqToHom_map, eqToHom_trans, eqToHom_refl]
+  add := fun a b => by
+    ext
+    rw [CommShift.isoAdd_hom_app]
+    dsimp
+    erw [id_comp, id_comp]
+    simp only [CochainComplex.shiftFunctorAdd_hom_app_f,
+      CochainComplex.shiftFunctorAdd_inv_app_f, HomologicalComplex.XIsoOfEq, eqToIso,
+      eqToHom_map, eqToHom_trans, eqToHom_refl]
+
+lemma mapHomologicalComplex_commShiftIso_eq (n : ℤ) :
+    (F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n =
+      F.mapCochainComplexShiftIso n := rfl
+
+@[simp]
+lemma mapHomologicalComplex_commShiftIso_hom_app_f (K : CochainComplex C ℤ) (n i : ℤ) :
+    (((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).hom.app K).f i = 𝟙 _ := rfl
+
+@[simp]
+lemma mapHomologicalComplex_commShiftIso_inv_app_f (K : CochainComplex C ℤ) (n i : ℤ) :
+    (((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).inv.app K).f i = 𝟙 _ := rfl
+
+end Functor
+
+end CategoryTheory
+
+namespace Homotopy
+
+variable {C}
+
+/-- If `h : Homotopy φ₁ φ₂` and `n : ℤ`, this is the induced homotopy
+between `φ₁⟦n⟧'` and `φ₂⟦n⟧'`. -/
+def shift {K L : CochainComplex C ℤ} {φ₁ φ₂ : K ⟶ L} (h : Homotopy φ₁ φ₂) (n : ℤ) :
+    Homotopy (φ₁⟦n⟧') (φ₂⟦n⟧') where
+  hom i j := n.negOnePow • h.hom _ _
+  zero i j hij := by
+    dsimp
+    rw [h.zero, zsmul_zero]
+    intro hij'
+    dsimp at hij hij'
+    exact hij (by linarith)
+  comm := fun i => by
+    rw [dNext_eq _ (show (ComplexShape.up ℤ).Rel i (i + 1) by simp),
+      prevD_eq _ (show (ComplexShape.up ℤ).Rel (i - 1) i by simp)]
+    dsimp
+    simpa only [Preadditive.zsmul_comp, Preadditive.comp_zsmul, smul_smul,
+      Int.negOnePow_mul_self, one_smul,
+      dNext_eq _ (show (ComplexShape.up ℤ).Rel (i + n) (i + 1 + n) by dsimp; linarith),
+      prevD_eq _ (show (ComplexShape.up ℤ).Rel (i - 1 + n) (i + n) by dsimp; linarith)]
+        using h.comm (i + n)
+
+end Homotopy
+
+namespace HomotopyCategory
+
+instance : (homotopic C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ :=
+  ⟨fun n _ _ _ _ ⟨h⟩ => ⟨h.shift n⟩⟩
+
+noncomputable instance hasShift :
+    HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ := by
+  dsimp only [HomotopyCategory]
+  infer_instance
+
+noncomputable instance commShiftQuotient :
+    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ :=
+  Quotient.functor_commShift (homotopic C (ComplexShape.up ℤ)) ℤ
+
+end HomotopyCategory
