feat: the shift on the category of cochain complexes (#6626)

This PR constructs the shift on the category of cochain complexes.



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

Mathlib.lean

@@ -223,6 +223,7 @@ import Mathlib.Algebra.Homology.Homology
 import Mathlib.Algebra.Homology.Homotopy
 import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
+import Mathlib.Algebra.Homology.HomotopyCategory.Shift
 import Mathlib.Algebra.Homology.ImageToKernel
 import Mathlib.Algebra.Homology.LocalCohomology
 import Mathlib.Algebra.Homology.ModuleCat

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -361,6 +361,14 @@ end
 
 noncomputable section
 
+@[reassoc]
+lemma XIsoOfEq_hom_naturality {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') :
+    φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n' := by subst h; simp
+
+@[reassoc]
+lemma XIsoOfEq_inv_naturality {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') :
+    φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n := by subst h; simp
+
 -- porting note: removed @[simp] as the linter complained
 /-- If `C.d i j` and `C.d i j'` are both allowed, then we must have `j = j'`,
 and so the differentials only differ by an `eqToHom`.

Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean

@@ -0,0 +1,186 @@
+/-
+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.GroupPower.NegOnePow
+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 ℤ)) ℤ]`.
+
+-/
+
+universe v u
+
+open CategoryTheory
+
+variable (C : Type u) [Category.{v} C] [Preadditive C]
+
+namespace CochainComplex
+
+open HomologicalComplex
+
+attribute [local simp] XIsoOfEq_hom_naturality
+
+/-- The shift functor by `n : ℤ` on `CochainComplex C ℤ` which sends a cochain
+complex `K` to the complex which is `K.X (i + n)` in degree `i`, and which
+multiplies the differentials by `(-1)^n`. -/
+@[simps]
+def shiftFunctor (n : ℤ) : CochainComplex C ℤ ⥤ CochainComplex C ℤ where
+  obj K :=
+    { X := fun i => K.X (i + n)
+      d := fun i j => n.negOnePow • K.d _ _
+      d_comp_d' := by
+        intros
+        simp only [Preadditive.comp_zsmul, Preadditive.zsmul_comp, d_comp_d, smul_zero]
+      shape := fun i j hij => by
+        dsimp
+        rw [K.shape, smul_zero]
+        intro hij'
+        apply hij
+        dsimp at hij' ⊢
+        linarith }
+  map φ :=
+    { f := fun i => φ.f _
+      comm' := by
+        intros
+        dsimp
+        simp only [Preadditive.comp_zsmul, Hom.comm, Preadditive.zsmul_comp] }
+  map_id := by intros; rfl
+  map_comp := by intros; rfl
+
+instance (n : ℤ) : (shiftFunctor C n).Additive where
+
+variable {C}
+
+/-- The canonical isomorphism `((shiftFunctor C n).obj K).X i ≅ K.X m` when `m = i + n`. -/
+@[simp]
+def shiftFunctorObjXIso (K : CochainComplex C ℤ) (n i m : ℤ) (hm : m = i + n) :
+    ((shiftFunctor C n).obj K).X i ≅ K.X m := K.XIsoOfEq hm.symm
+
+variable (C)
+
+/-- The shift functor by `n` on `CochainComplex C ℤ` identifies to the identity
+functor when `n = 0`. -/
+@[simps!]
+def shiftFunctorZero' (n : ℤ) (h : n = 0) :
+    shiftFunctor C n ≅ 𝟭 _ :=
+  NatIso.ofComponents (fun K => Hom.isoOfComponents
+    (fun i => K.shiftFunctorObjXIso _ _ _ (by linarith))
+    (fun _ _ _ => by simp [h])) (by aesop_cat)
+
+/-- The compatibility of the shift functors on `CochainComplex C ℤ` with respect
+to the addition of integers. -/
+@[simps!]
+def shiftFunctorAdd' (n₁ n₂ n₁₂ : ℤ) (h : n₁ + n₂ = n₁₂ ) :
+    shiftFunctor C n₁₂ ≅ shiftFunctor C n₁ ⋙ shiftFunctor C n₂ :=
+  NatIso.ofComponents (fun K => Hom.isoOfComponents
+    (fun i => K.shiftFunctorObjXIso _ _ _ (by linarith))
+    (fun _ _ _ => by
+      subst h
+      dsimp
+      simp only [add_comm n₁ n₂, Int.negOnePow_add, Preadditive.zsmul_comp,
+        Preadditive.comp_zsmul, d_comp_XIsoOfEq_hom, smul_smul, XIsoOfEq_hom_comp_d]))
+    (by aesop_cat)
+
+attribute [local simp] XIsoOfEq
+
+instance : HasShift (CochainComplex C ℤ) ℤ := hasShiftMk _ _
+  { F := shiftFunctor C
+    zero := shiftFunctorZero' C _ rfl
+    add := fun n₁ n₂ => shiftFunctorAdd' C n₁ n₂ _ rfl }
+
+instance (n : ℤ) :
+    (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).Additive :=
+  (inferInstance : (CochainComplex.shiftFunctor C n).Additive)
+
+variable {C}
+
+@[simp]
+lemma shiftFunctor_map_f' {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n p : ℤ) :
+    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p+n) := rfl
+
+@[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
+
+lemma shiftFunctorAdd_inv_app_f (K : CochainComplex C ℤ) (a b n : ℤ) :
+    ((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n =
+      (K.XIsoOfEq (by dsimp; rw [add_comm a, add_assoc])).hom := rfl
+
+lemma shiftFunctorAdd_hom_app_f (K : CochainComplex C ℤ) (a b n : ℤ) :
+    ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n =
+      (K.XIsoOfEq (by dsimp; rw [add_comm a, add_assoc])).hom := by
+  have : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n) := by
+    rw [shiftFunctorAdd_inv_app_f]
+    infer_instance
+  rw [← cancel_mono (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n),
+    ← comp_f, Iso.hom_inv_id_app, id_f, shiftFunctorAdd_inv_app_f]
+  simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans, eqToHom_refl]
+
+lemma shiftFunctorAdd'_inv_app_f' (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) :
+    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n =
+      (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom := by
+  subst h
+  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_inv_app_f]
+
+lemma shiftFunctorAdd'_hom_app_f' (K : CochainComplex C ℤ) (a b ab : ℤ) (h : a + b = ab) (n : ℤ) :
+    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n =
+      (K.XIsoOfEq (by dsimp; rw [← h, add_assoc, add_comm a])).hom := by
+  subst h
+  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]
+
+lemma shiftFunctorZero_inv_app_f (K : CochainComplex C ℤ) (n : ℤ) :
+    ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n =
+      (K.XIsoOfEq (by dsimp; rw [add_zero])).hom := rfl
+
+lemma shiftFunctorZero_hom_app_f (K : CochainComplex C ℤ) (n : ℤ) :
+    ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n =
+      (K.XIsoOfEq (by dsimp; rw [add_zero])).hom := by
+  have : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n) := by
+    rw [shiftFunctorZero_inv_app_f]
+    infer_instance
+  rw [← cancel_mono (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n), ← comp_f,
+    Iso.hom_inv_id_app, id_f, shiftFunctorZero_inv_app_f]
+  simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans, eqToHom_refl]
+
+lemma XIsoOfEq_shift (K : CochainComplex C ℤ) (n : ℤ) {p q : ℤ} (hpq : p = q) :
+    (K⟦n⟧).XIsoOfEq hpq = K.XIsoOfEq (show p + n = q + n by rw [hpq]) := rfl
+
+variable (C)
+
+lemma shiftFunctorAdd'_eq (a b c : ℤ) (h : a + b = c) :
+    CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h =
+      shiftFunctorAdd' C a b c h := by
+  ext
+  simp only [shiftFunctorAdd'_hom_app_f', XIsoOfEq, eqToIso.hom, shiftFunctorAdd'_hom_app_f]
+
+lemma shiftFunctorAdd_eq (a b : ℤ) :
+    CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b _ rfl := by
+  rw [← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq]
+
+lemma shiftFunctorZero_eq :
+    CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ = shiftFunctorZero' C 0 rfl := by
+  ext
+  rw [shiftFunctorZero_hom_app_f, shiftFunctorZero'_hom_app_f]
+
+variable {C}
+
+lemma shiftFunctorComm_hom_app_f (K : CochainComplex C ℤ) (a b p : ℤ) :
+    ((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p =
+      (K.XIsoOfEq (show p + b + a = p + a + b
+        by rw [add_assoc, add_comm b, add_assoc])).hom := by
+  rw [shiftFunctorComm_eq _ _ _ _ rfl]
+  dsimp
+  rw [shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_hom_app_f']
+  simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans]
+
+end CochainComplex