THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
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.ιis the map from
homology f g winto the cokernel of
homology.π'is the map from
homology f g w.
homology.desc'constructs a morphism from
homology f g w, when it is viewed as a cokernel.
homology.liftconstructs 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.
The cokernel of
kernel.lift g f w. This is isomorphic to
homology f g w.
The kernel of
cokernel.desc f g w. This is isomorphic to
homology f g w.
The canonical map from
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
g is isomorphic to a kernel.
The canonical map from the kernel of
g to the homology of
- 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
g to the cokernel of
- 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.
- 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.
- 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
F is an exact additive functor,
F(Hᵢ(X)) ≅ Hᵢ(F(X)) for
X a complex.
- F.homology_iso C j = category_theory.limits.preserves_cokernel.iso F (image_to_kernel (C.d_to j) (C.d_from j) _) ≪≫ category_theory.limits.cokernel.map_iso (F.map (image_to_kernel (C.d_to j) (C.d_from j) _)) (image_to_kernel (((F.map_homological_complex c).obj C).d_to j) (((F.map_homological_complex c).obj C).d_from j) _) (F.map_iso (category_theory.limits.image_subobject_iso (C.d_to j)) ≪≫ (category_theory.preserves_image.iso F (C.d_to j)).symm ≪≫ (category_theory.limits.image_subobject_iso (F.map (C.d_to j))).symm) (F.map_iso (category_theory.limits.kernel_subobject_iso (C.d_from j)) ≪≫ category_theory.limits.preserves_kernel.iso F (C.d_from j) ≪≫ (category_theory.limits.kernel_subobject_iso (F.map (C.d_from j))).symm) _
F is an exact additive functor, then
F commutes with
Hᵢ (up to natural isomorphism).
- F.homology_functor_iso i = category_theory.nat_iso.of_components (λ (X : homological_complex A c), F.homology_iso X i) _