mathlib3 documentation

category_theory.abelian.homology

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_iso_cokernel_lift, 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:

@[reducible]
noncomputable def category_theory.abelian.homology_c {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :
A

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

@[reducible]
noncomputable def category_theory.abelian.homology_k {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :
A

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

@[reducible]

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

noncomputable def homology_iso_kernel_desc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :

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

Equations
noncomputable def homology.π' {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :

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

Equations
noncomputable def homology.ι {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :

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

Equations
noncomputable def homology.desc' {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (e : category_theory.limits.kernel g W) (he : category_theory.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
noncomputable def homology.lift {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (e : W category_theory.limits.cokernel f) (he : e category_theory.limits.cokernel.desc f g w = 0) :
W homology f g w

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

Equations
@[simp]
theorem homology.π'_desc' {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (e : category_theory.limits.kernel g W) (he : category_theory.limits.kernel.lift g f w e = 0) :
homology.π' f g w homology.desc' f g w e he = e
@[simp]
theorem homology.π'_desc'_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (e : category_theory.limits.kernel g W) (he : category_theory.limits.kernel.lift g f w e = 0) {X' : A} (f' : W X') :
homology.π' f g w homology.desc' f g w e he f' = e f'
@[simp]
theorem homology.lift_ι {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (e : W category_theory.limits.cokernel f) (he : e category_theory.limits.cokernel.desc f g w = 0) :
homology.lift f g w e he homology.ι f g w = e
@[simp]
theorem homology.lift_ι_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (e : W category_theory.limits.cokernel f) (he : e category_theory.limits.cokernel.desc f g w = 0) {X' : A} (f' : category_theory.limits.cokernel f X') :
homology.lift f g w e he homology.ι f g w f' = e f'
@[simp]
theorem homology.condition_π' {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :
@[simp]
theorem homology.condition_π'_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' : A} (f' : homology f g w X') :
@[simp]
theorem homology.condition_ι {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :
@[simp]
theorem homology.condition_ι_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' : A} (f' : Z X') :
@[ext]
theorem homology.hom_from_ext {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (a b : homology f g w W) (h : homology.π' f g w a = homology.π' f g w b) :
a = b
@[ext]
theorem homology.hom_to_ext {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {W : A} (a b : W homology f g w) (h : a homology.ι f g w = b homology.ι f g w) :
a = b
@[simp]
theorem homology.π'_eq_π {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) :
@[simp]
theorem homology.π'_eq_π_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' : A} (f' : homology f g w X') :
@[simp]
theorem homology.π'_map {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) :
@[simp]
theorem homology.π'_map_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) {X'_1 : A} (f'_1 : homology f' g' w' X'_1) :
theorem homology.map_eq_desc'_lift_left {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) :
theorem homology.map_eq_lift_desc'_left {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) :
theorem homology.map_eq_desc'_lift_right {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) :
theorem homology.map_eq_lift_desc'_right {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) :
@[simp]
theorem homology.map_ι_assoc {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) {X'_1 : A} (f'_1 : category_theory.limits.cokernel f' X'_1) :
homology.map w w' α β h homology.ι f' g' w' f'_1 = homology.ι f g w category_theory.limits.cokernel.map f f' α.left β.left _ f'_1
@[simp]
theorem homology.map_ι {A : Type u} [category_theory.category A] [category_theory.abelian A] {X Y Z : A} (f : X Y) (g : Y Z) (w : f g = 0) {X' Y' Z' : A} (f' : X' Y') (g' : Y' Z') (w' : f' g' = 0) (α : category_theory.arrow.mk f category_theory.arrow.mk f') (β : category_theory.arrow.mk g category_theory.arrow.mk g') (h : α.right = β.left) :