Cycles and augmented resolutions of diagrams of complexes

For a diagram K : D ⥤ HomologicalComplex A c, the cycles in degree i form a diagram in A. Their inclusions and the differentials corestricted to cycles are natural transformations, forming the short complex Zⁱ(K) ⟶ Kⁱ ⟶ Zʲ(K). At any object where K is exact in degree j, this sequence is short exact if c.Rel i j.

An augmentation ε : P ⋙ CochainComplex.single₀ A ⟶ K gives the short complex P ⟶ K⁰ ⟶ Z¹(K). It is short exact at any object where ε is a quasi-isomorphism in degrees zero and one. These sequences split an augmented resolution into short exact sequences, allowing objectwise dimension shifting without imposing exactness at every object of the diagram.

noncomputable def CategoryTheory.Functor.iCycles {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i : ι) : K.comp (HomologicalComplex.cyclesFunctor A c i) ⟶ K.comp (HomologicalComplex.eval A c i)

The natural inclusion of the diagram of degree-i cycles into the degree-i terms.

@[simp]

theorem CategoryTheory.Functor.iCycles_app {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i : ι) (Y : D) : (K.iCycles i).app Y = (K.obj Y).iCycles i

noncomputable def CategoryTheory.Functor.toCycles {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : K.comp (HomologicalComplex.eval A c i) ⟶ K.comp (HomologicalComplex.cyclesFunctor A c j)

The differential from degree i corestricted to the diagram of degree-j cycles.

@[simp]

theorem CategoryTheory.Functor.toCycles_app {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) (Y : D) : (K.toCycles i j).app Y = (K.obj Y).toCycles i j

noncomputable def CategoryTheory.Functor.cyclesShortComplex {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : ShortComplex (Functor D A)

The short complex Zⁱ(K) ⟶ Kⁱ ⟶ Zʲ(K) of diagrams of cycles and terms.

@[simp]

theorem CategoryTheory.Functor.cyclesShortComplex_X₁ {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : (K.cyclesShortComplex i j).X₁ = K.comp (HomologicalComplex.cyclesFunctor A c i)

@[simp]

theorem CategoryTheory.Functor.cyclesShortComplex_X₂ {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : (K.cyclesShortComplex i j).X₂ = K.comp (HomologicalComplex.eval A c i)

@[simp]

theorem CategoryTheory.Functor.cyclesShortComplex_X₃ {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : (K.cyclesShortComplex i j).X₃ = K.comp (HomologicalComplex.cyclesFunctor A c j)

@[simp]

theorem CategoryTheory.Functor.cyclesShortComplex_f {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : (K.cyclesShortComplex i j).f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (K.iCycles i) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Functor.cyclesShortComplex_g {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) : (K.cyclesShortComplex i j).g = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (K.toCycles i j) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Functor.map_cyclesShortComplex {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) (Y : D) : (K.cyclesShortComplex i j).map ((evaluation D A).obj Y) = { X₁ := (K.obj Y).cycles i, X₂ := (K.obj Y).X i, X₃ := (K.obj Y).cycles j, f := (K.obj Y).iCycles i, g := (K.obj Y).toCycles i j, zero := ⋯ }

theorem CategoryTheory.Functor.shortExact_map_cyclesShortComplex {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Preadditive A] [CategoryWithHomology A] {ι : Type u_3} {c : ComplexShape ι} (K : Functor D (HomologicalComplex A c)) (i j : ι) (hij : c.Rel i j) {Y : D} (hY : (K.obj Y).ExactAt j) : ((K.cyclesShortComplex i j).map ((evaluation D A).obj Y)).ShortExact

The cycle sequence is short exact at an object where the complex is exact in the next degree. No exactness is required at the other objects of the diagram.

noncomputable def CategoryTheory.NatTrans.augmentationι {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) : P ⟶ K.comp (HomologicalComplex.eval A (ComplexShape.up ℕ) 0)

The degree-zero component of an augmentation, as a morphism of diagrams in A.

@[simp]

theorem CategoryTheory.NatTrans.augmentationι_app {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) (Y : D) : (augmentationι ε).app Y = CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 (P.obj Y)).inv ((ε.app Y).f 0)

noncomputable def CategoryTheory.NatTrans.augmentationShortComplex {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] : ShortComplex (Functor D A)

The short complex P ⟶ K⁰ ⟶ Z¹(K) cut out by an augmented diagram of cochain complexes.

@[simp]

theorem CategoryTheory.NatTrans.augmentationShortComplex_X₁ {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] : (augmentationShortComplex ε).X₁ = P

@[simp]

theorem CategoryTheory.NatTrans.augmentationShortComplex_X₂ {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] : (augmentationShortComplex ε).X₂ = K.comp (HomologicalComplex.eval A (ComplexShape.up ℕ) 0)

@[simp]

theorem CategoryTheory.NatTrans.augmentationShortComplex_X₃ {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] : (augmentationShortComplex ε).X₃ = K.comp (HomologicalComplex.cyclesFunctor A (ComplexShape.up ℕ) 1)

@[simp]

theorem CategoryTheory.NatTrans.augmentationShortComplex_f {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] : (augmentationShortComplex ε).f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (augmentationι ε) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.NatTrans.augmentationShortComplex_g {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] : (augmentationShortComplex ε).g = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (K.toCycles 0 1) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.NatTrans.map_augmentationShortComplex {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Limits.HasZeroMorphisms A] [Limits.HasZeroObject A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) [CategoryWithHomology A] (Y : D) : (augmentationShortComplex ε).map ((evaluation D A).obj Y) = { X₁ := P.obj Y, X₂ := (K.obj Y).X 0, X₃ := HomologicalComplex.cycles (K.obj Y) 1, f := CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 (P.obj Y)).inv ((ε.app Y).f 0), g := HomologicalComplex.toCycles (K.obj Y) 0 1, zero := ⋯ }

theorem CategoryTheory.NatTrans.shortExact_map_augmentationShortComplex {D : Type u_1} {A : Type u_2} [Category.{v_1, u_1} D] [Category.{v_2, u_2} A] [Preadditive A] [Limits.HasZeroObject A] [CategoryWithHomology A] {P : Functor D A} {K : Functor D (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) {Y : D} (h₀ : QuasiIsoAt (ε.app Y) 0) (h₁ : QuasiIsoAt (ε.app Y) 1) : ((augmentationShortComplex ε).map ((evaluation D A).obj Y)).ShortExact

The augmented sequence is short exact at any object where the augmentation is a quasi-isomorphism in degrees zero and one. No condition on its higher cohomology is needed.