Compatibilities of the homology functor with the shift

This file 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.{v_1, 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'.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{v_1, 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.{v_1, 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'_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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'.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{v_1, 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.{v_1, 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_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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 (K⟦m⟧)) ((shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K))

noncomputable def CochainComplex.ShiftSequence.shiftIso (C : Type u_1) [CategoryTheory.Category.{v_1, 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'.

Equations

• One or more equations did not get rendered due to their size.

theorem CochainComplex.ShiftSequence.shiftIso_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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.{v_1, 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)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

theorem CochainComplex.quasiIsoAt_shift_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n i j : ℤ) (h : n + i = j) : QuasiIsoAt (φ⟦n⟧') i ↔ QuasiIsoAt φ j

theorem CochainComplex.quasiIso_shift_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : QuasiIso (φ⟦n⟧') ↔ QuasiIso φ

instance CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] : QuasiIso (φ⟦n⟧')

instance CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso {C : Type u_1} [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ K⟦n⟧.X i) (j : ℤ) (hj : (ComplexShape.up ℤ).next i = j) (hf : CategoryTheory.CategoryStruct.comp f (K⟦n⟧.d i j) = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (K⟦n⟧) f j hj hf) (HomologicalComplex.homologyπ (K⟦n⟧) 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.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ K⟦n⟧.X i) (j : ℤ) (hj : (ComplexShape.up ℤ).next i = j) (hf : CategoryTheory.CategoryStruct.comp f (K⟦n⟧.d i j) = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') {Z : C} (h : HomologicalComplex.homology (K⟦n⟧) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles (K⟦n⟧) f j hj hf) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (K⟦n⟧) 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))

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

theorem HomotopyCategory.homologyShiftIso_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, 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 ((CategoryTheory.Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app K)) (CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C (ComplexShape.up ℤ) a).hom.app (K⟦n⟧)) (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.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') : (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap (CategoryTheory.ShiftedHom.map f (quotient C (ComplexShape.up ℤ))) 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.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (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.ShiftedHom.map f (quotient C (ComplexShape.up ℤ))) a a' h) h✝ = CategoryTheory.CategoryStruct.comp (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))) h✝