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 homology'IsoCokernelLift, 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.

Note: As part of the homology refactor, it is planned to remove the definitions in this file, because it can be replaced by the content of Algebra.Homology.ShortComplex.Homology.

@[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.

Equations

• CategoryTheory.Abelian.homologyC f g w = CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift g f w)

@[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.

Equations

• CategoryTheory.Abelian.homologyK f g w = CategoryTheory.Limits.kernel (CategoryTheory.Limits.cokernel.desc f g w)

@[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.

Equations

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

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)

Equations

• (_ : CategoryTheory.Mono (CategoryTheory.Abelian.homologyCToK f g w)) = (_ : 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)

Equations

• (_ : CategoryTheory.Epi (CategoryTheory.Abelian.homologyCToK f g w)) = (_ : 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)

Equations

• (_ : CategoryTheory.IsIso (CategoryTheory.Abelian.homologyCToK f g w)) = (_ : CategoryTheory.IsIso (CategoryTheory.Abelian.homologyCToK f g w))

def homology'IsoKernelDesc {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.

Equations

• homology'IsoKernelDesc f g w = homology'IsoCokernelLift f g w ≪≫ CategoryTheory.asIso (CategoryTheory.Abelian.homologyCToK f g w)

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.

Equations

• homology'.π' f g w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.lift g f w)) (homology'IsoCokernelLift f g w).inv

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.

Equations

• homology'.ι f g w = CategoryTheory.CategoryStruct.comp (homology'IsoKernelDesc f g w).hom (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.desc f g w))

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.

Equations

• homology'.desc' f g w e he = CategoryTheory.CategoryStruct.comp (homology'IsoCokernelLift f g w).hom (CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.lift g f w) e he)

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 morphism to the homology, given a morphism to the kernel.

Equations

• homology'.lift f g w e he = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.desc f g w) e he) (homology'IsoKernelDesc f g w).inv

@[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.homology'Iso {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.toPrefunctor.obj (HomologicalComplex.homology' C j) ≅ HomologicalComplex.homology' ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj C) j

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

Equations

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

noncomputable def CategoryTheory.Functor.homology'FunctorIso {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 (homology'Functor A c i) F ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F c) (homology'Functor B c i)

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

Equations

• CategoryTheory.Functor.homology'FunctorIso F i = CategoryTheory.NatIso.ofComponents fun (X : HomologicalComplex A c) => CategoryTheory.Functor.homology'Iso F X i