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
:
homology.ι
is the map fromhomology f g w
into the cokernel off
.homology.π'
is the map fromkernel g
tohomology f g w
.homology.desc'
constructs a morphism fromhomology f g w
, when it is viewed as a cokernel.homology.lift
constructs a morphism tohomology 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.
The cokernel of kernel.lift g f w
. This is isomorphic to homology f g w
.
See homology_iso_cokernel_lift
.
The kernel of cokernel.desc f g w
. This is isomorphic to homology f g w
.
See homology_iso_kernel_desc
.
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.
The homology associated to f
and g
is isomorphic to a kernel.
Equations
The canonical map from the kernel of g
to the homology of f
and g
.
Equations
- homology.π' f g w = category_theory.limits.cokernel.π (category_theory.limits.kernel.lift g f w) ≫ (homology_iso_cokernel_lift f g w).inv
The canonical map from the homology of f
and g
to the cokernel of f
.
Equations
- homology.ι f g w = (homology_iso_kernel_desc f g w).hom ≫ category_theory.limits.kernel.ι (category_theory.limits.cokernel.desc f g w)
Obtain a morphism from the homology, given a morphism from the kernel.
Equations
- homology.desc' f g w e he = (homology_iso_cokernel_lift f g w).hom ≫ category_theory.limits.cokernel.desc (category_theory.limits.kernel.lift g f w) e he
Obtain a moprhism to the homology, given a morphism to the kernel.
Equations
- homology.lift f g w e he = category_theory.limits.kernel.lift (category_theory.limits.cokernel.desc f g w) e he ≫ (homology_iso_kernel_desc f g w).inv