The object homology f g w, where w : f ≫ g = 0, can be identified with either a cokernel or a kernel. The isomorphism with a cokernel is homologyIsoCokernelLift, which was obtained elsewhere. In the case of an abelian category, this file shows the isomorphism with a kernel as well.

We use these isomorphisms to obtain the analogous api for homology:

• homology.ι is the map from homology f g w into the cokernel of f.
• homology.π' is the map from kernel g to homology f g w.
• homology.desc' constructs a morphism from homology f g w, when it is viewed as a cokernel.
• homology.lift constructs a morphism to homology f g w, when it is viewed as a kernel.
• Various small lemmas are proved as well, mimicking the API for (co)kernels. With these definitions and lemmas, the isomorphisms between homology and a (co)kernel need not be used directly.

@[inline, reducible]

abbrev CategoryTheory.Abelian.homologyC {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : A

The cokernel of kernel.lift g f w. This is isomorphic to homology f g w. See homologyIsoCokernelLift.

@[inline, reducible]

abbrev CategoryTheory.Abelian.homologyK {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : A

The kernel of cokernel.desc f g w. This is isomorphic to homology f g w. See homologyIsoKernelDesc.

@[inline, reducible]

abbrev CategoryTheory.Abelian.homologyCToK {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Abelian.homologyC f g w ⟶ CategoryTheory.Abelian.homologyK f g w

The canonical map from homologyC to homologyK. This is an isomorphism, and it is used in obtaining the API for homology f g w in the bottom of this file.

instance CategoryTheory.Abelian.instMonoHomologyCHomologyKHomologyCToK {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Mono (CategoryTheory.Abelian.homologyCToK f g w)

instance CategoryTheory.Abelian.instEpiHomologyCHomologyKHomologyCToK {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Epi (CategoryTheory.Abelian.homologyCToK f g w)

instance CategoryTheory.Abelian.instIsIsoHomologyCHomologyKHomologyCToK {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.IsIso (CategoryTheory.Abelian.homologyCToK f g w)

def homologyIsoKernelDesc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : homology f g w ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc f g w)

The homology associated to f and g is isomorphic to a kernel.

def homology.π' {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.kernel g ⟶ homology f g w

The canonical map from the kernel of g to the homology of f and g.

def homology.ι {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : homology f g w ⟶ CategoryTheory.Limits.cokernel f

The canonical map from the homology of f and g to the cokernel of f.

def homology.desc' {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (e : CategoryTheory.Limits.kernel g ⟶ W) (he : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) e = 0) : homology f g w ⟶ W

Obtain a morphism from the homology, given a morphism from the kernel.

def homology.lift {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (e : W ⟶ CategoryTheory.Limits.cokernel f) (he : CategoryTheory.CategoryStruct.comp e (CategoryTheory.Limits.cokernel.desc f g w) = 0) : W ⟶ homology f g w

Obtain a moprhism to the homology, given a morphism to the kernel.

@[simp]

theorem homology.π'_desc'_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (e : CategoryTheory.Limits.kernel g ⟶ W) (he : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) e = 0) {Z : A} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (homology.π' f g w) (CategoryTheory.CategoryStruct.comp (homology.desc' f g w e he) h) = CategoryTheory.CategoryStruct.comp e h

@[simp]

theorem homology.π'_desc' {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (e : CategoryTheory.Limits.kernel g ⟶ W) (he : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) e = 0) : CategoryTheory.CategoryStruct.comp (homology.π' f g w) (homology.desc' f g w e he) = e

@[simp]

theorem homology.lift_ι_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (e : W ⟶ CategoryTheory.Limits.cokernel f) (he : CategoryTheory.CategoryStruct.comp e (CategoryTheory.Limits.cokernel.desc f g w) = 0) {Z : A} (h : CategoryTheory.Limits.cokernel f ⟶ Z) : CategoryTheory.CategoryStruct.comp (homology.lift f g w e he) (CategoryTheory.CategoryStruct.comp (homology.ι f g w) h) = CategoryTheory.CategoryStruct.comp e h

@[simp]

theorem homology.lift_ι {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (e : W ⟶ CategoryTheory.Limits.cokernel f) (he : CategoryTheory.CategoryStruct.comp e (CategoryTheory.Limits.cokernel.desc f g w) = 0) : CategoryTheory.CategoryStruct.comp (homology.lift f g w e he) (homology.ι f g w) = e

@[simp]

theorem homology.condition_π'_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : A} (h : homology f g w ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (CategoryTheory.CategoryStruct.comp (homology.π' f g w) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem homology.condition_π' {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (homology.π' f g w) = 0

@[simp]

theorem homology.condition_ι_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : A} (h : Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (homology.ι f g w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f g w) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem homology.condition_ι {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (homology.ι f g w) (CategoryTheory.Limits.cokernel.desc f g w) = 0

theorem homology.hom_from_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (a : homology f g w ⟶ W) (b : homology f g w ⟶ W) (h : CategoryTheory.CategoryStruct.comp (homology.π' f g w) a = CategoryTheory.CategoryStruct.comp (homology.π' f g w) b) : a = b

theorem homology.hom_to_ext {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {W : A} (a : W ⟶ homology f g w) (b : W ⟶ homology f g w) (h : CategoryTheory.CategoryStruct.comp a (homology.ι f g w) = CategoryTheory.CategoryStruct.comp b (homology.ι f g w)) : a = b

@[simp]

theorem homology.π'_ι_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : A} (h : CategoryTheory.Limits.cokernel f ⟶ Z) : CategoryTheory.CategoryStruct.comp (homology.π' f g w) (CategoryTheory.CategoryStruct.comp (homology.ι f g w) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) h)

@[simp]

theorem homology.π'_ι {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (homology.π' f g w) (homology.ι f g w) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.Limits.cokernel.π f)

@[simp]

theorem homology.π'_eq_π_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : A} (h : homology f g w ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso g).hom (CategoryTheory.CategoryStruct.comp (homology.π' f g w) h) = CategoryTheory.CategoryStruct.comp (homology.π f g w) h

@[simp]

theorem homology.π'_eq_π {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso g).hom (homology.π' f g w) = homology.π f g w

@[simp]

theorem homology.π'_map_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) {Z : A} (h : homology f' g' w' ⟶ Z) : CategoryTheory.CategoryStruct.comp (homology.π' f g w) (CategoryTheory.CategoryStruct.comp (homology.map w w' α β h) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map g g' α.right β.right (_ : CategoryTheory.CategoryStruct.comp g β.right = CategoryTheory.CategoryStruct.comp α.right g')) (CategoryTheory.CategoryStruct.comp (homology.π' f' g' w') h)

@[simp]

theorem homology.π'_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) : CategoryTheory.CategoryStruct.comp (homology.π' f g w) (homology.map w w' α β h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map g g' α.right β.right (_ : CategoryTheory.CategoryStruct.comp g β.right = CategoryTheory.CategoryStruct.comp α.right g')) (homology.π' f' g' w')

theorem homology.map_eq_desc'_lift_left {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) : homology.map w w' α β h = homology.desc' f g w (homology.lift f' g' w' (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) (CategoryTheory.Limits.cokernel.desc f' g' w') = 0)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (homology.lift f' g' w' (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) (CategoryTheory.Limits.cokernel.desc f' g' w') = 0)) = 0)

theorem homology.map_eq_lift_desc'_left {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) : homology.map w w' α β h = homology.lift f' g' w' (homology.desc' f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) = 0)) (_ : CategoryTheory.CategoryStruct.comp (homology.desc' f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp β.left (CategoryTheory.Limits.cokernel.π f'))) = 0)) (CategoryTheory.Limits.cokernel.desc f' g' w') = 0)

theorem homology.map_eq_desc'_lift_right {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) : homology.map w w' α β h = homology.desc' f g w (homology.lift f' g' w' (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) (CategoryTheory.Limits.cokernel.desc f' g' w') = 0)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (homology.lift f' g' w' (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) (CategoryTheory.Limits.cokernel.desc f' g' w') = 0)) = 0)

theorem homology.map_eq_lift_desc'_right {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) : homology.map w w' α β h = homology.lift f' g' w' (homology.desc' f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) = 0)) (_ : CategoryTheory.CategoryStruct.comp (homology.desc' f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.CategoryStruct.comp α.right (CategoryTheory.Limits.cokernel.π f'))) = 0)) (CategoryTheory.Limits.cokernel.desc f' g' w') = 0)

@[simp]

theorem homology.map_ι_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) {Z : A} (h : CategoryTheory.Limits.cokernel f' ⟶ Z) : CategoryTheory.CategoryStruct.comp (homology.map w w' α β h) (CategoryTheory.CategoryStruct.comp (homology.ι f' g' w') h) = CategoryTheory.CategoryStruct.comp (homology.ι f g w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map f f' α.left β.left (_ : CategoryTheory.CategoryStruct.comp f β.left = CategoryTheory.CategoryStruct.comp α.left f')) h)

@[simp]

theorem homology.map_ι {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) {X' : A} {Y' : A} {Z' : A} (f' : X' ⟶ Y') (g' : Y' ⟶ Z') (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') (β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g') (h : α.right = β.left) : CategoryTheory.CategoryStruct.comp (homology.map w w' α β h) (homology.ι f' g' w') = CategoryTheory.CategoryStruct.comp (homology.ι f g w) (CategoryTheory.Limits.cokernel.map f f' α.left β.left (_ : CategoryTheory.CategoryStruct.comp f β.left = CategoryTheory.CategoryStruct.comp α.left f'))

noncomputable def CategoryTheory.Functor.homologyIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {ι : Type u_1} {c : ComplexShape ι} {B : Type u_2} [CategoryTheory.Category.{u_3, u_2} B] [CategoryTheory.Abelian B] (F : CategoryTheory.Functor A B) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (C : HomologicalComplex A c) (j : ι) : F.obj (HomologicalComplex.homology C j) ≅ HomologicalComplex.homology ((CategoryTheory.Functor.mapHomologicalComplex F c).obj C) j

When F is an exact additive functor, F(Hᵢ(X)) ≅ Hᵢ(F(X)) for X a complex.

noncomputable def CategoryTheory.Functor.homologyFunctorIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {ι : Type u_1} {c : ComplexShape ι} {B : Type u_2} [CategoryTheory.Category.{u_3, u_2} B] [CategoryTheory.Abelian B] (F : CategoryTheory.Functor A B) [CategoryTheory.Functor.Additive F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (i : ι) : CategoryTheory.Functor.comp (homologyFunctor A c i) F ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F c) (homologyFunctor B c i)

If F is an exact additive functor, then F commutes with Hᵢ (up to natural isomorphism).