Compatibilities of the homology functor with the shift

This files studies how homology of cochain complexes behaves with respect to the shift: there is a natural isomorphism (K⟦n⟧).homology a ≅ K.homology a when n + a = a'. This is summarized by instances (homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ in the CochainComplex and HomotopyCategory namespaces.

def CochainComplex.shiftShortComplexFunctor' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).comp (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℤ) i j k) ≅ HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℤ) i' j' k'

The natural isomorphism (K⟦n⟧).sc' i j k ≅ K.sc' i' j' k' when n + i = i', n + j = j' and n + k = k'.

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom

noncomputable def CochainComplex.shiftShortComplexFunctorIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') : (shiftFunctor C n).comp (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) i) ≅ HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) i'

The natural isomorphism (K⟦n⟧).sc i ≅ K.sc i' when n + i = i'.

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ) : ((shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom

theorem CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (a : ℤ) (K : CochainComplex C ℤ) : (shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K = (HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)

theorem CochainComplex.shiftShortComplexFunctorIso_add'_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n m mn : ℤ) (hmn : m + n = mn) (a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'') (K : CochainComplex C ℤ) : (shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.shortComplexFunctor C (ComplexShape.up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K)) (CategoryTheory.CategoryStruct.comp ((shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K)) ((shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K))

noncomputable def CochainComplex.ShiftSequence.shiftIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a) ≅ HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) a'

The natural isomorphism (K⟦n⟧).homology a ≅ K.homology a'when n + a = a.

theorem CochainComplex.ShiftSequence.shiftIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) : (shiftIso C n a a' ha').hom.app K = CategoryTheory.ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K)

theorem CochainComplex.ShiftSequence.shiftIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) : (shiftIso C n a a' ha').inv.app K = CategoryTheory.ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)

noncomputable instance CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ

theorem CochainComplex.quasiIsoAt_shift_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n i j : ℤ) (h : n + i = j) : QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j

theorem CochainComplex.quasiIso_shift_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ) ↔ QuasiIso φ

instance CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] : QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map φ)

instance CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ

theorem CochainComplex.homologyFunctor_shift (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n : ℤ) : (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shift n = HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n

theorem CochainComplex.liftCycles_shift_homologyπ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i) (j : ℤ) (hj : (ComplexShape.up ℤ).next i = j) (hf : CategoryTheory.CategoryStruct.comp f (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j) = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf) (HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp f (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i') (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K))

theorem CochainComplex.liftCycles_shift_homologyπ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i) (j : ℤ) (hj : (ComplexShape.up ℤ).next i = j) (hf : CategoryTheory.CategoryStruct.comp f (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j) = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') {Z : C} (h : HomologicalComplex.homology ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp f (K.shiftFunctorObjXIso n i i' ⋯).hom) j' hj' ⋯) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i') (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K) h))

noncomputable instance HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] : (homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ

theorem HomotopyCategory.homologyShiftIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) : ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app ((quotient C (ComplexShape.up ℤ)).obj K) = CategoryTheory.CategoryStruct.comp ((homologyFunctor C (ComplexShape.up ℤ) a).map (((quotient C (ComplexShape.up ℤ)).commShiftIso n).inv.app K)) (CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K)) (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app K) ((homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app K)))

theorem HomotopyCategory.homologyFunctor_shiftMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ) (h : n + a = a') : (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap (CategoryTheory.CategoryStruct.comp ((quotient C (ComplexShape.up ℤ)).map f) (((quotient C (ComplexShape.up ℤ)).commShiftIso n).hom.app L)) a a' h = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app K) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h) ((homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app L))

theorem HomotopyCategory.homologyFunctor_shiftMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (a a' : ℤ) (h : n + a = a') {Z : C} (h✝ : ((homologyFunctor C (ComplexShape.up ℤ) 0).shift a').obj ((quotient C (ComplexShape.up ℤ)).obj L) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap (CategoryTheory.CategoryStruct.comp ((quotient C (ComplexShape.up ℤ)).map f) (((quotient C (ComplexShape.up ℤ)).commShiftIso n).hom.app L)) a a' h) h✝ = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app K) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h) (CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C (ComplexShape.up ℤ) a').inv.app L) h✝))