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:
homology.ιis the map fromhomology f g winto the cokernel off.homology.π'is the map fromkernel gtohomology f g w.homology.desc'constructs a morphism fromhomology f g w, when it is viewed as a cokernel.homology.liftconstructs 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.
@[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]
noncomputable
def
category_theory.abelian.homology_c_to_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) :
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.
@[protected, instance]
def
category_theory.abelian.homology_c_to_k.category_theory.mono
{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) :
@[protected, instance]
def
category_theory.abelian.homology_c_to_k.category_theory.epi
{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) :
@[protected, instance]
def
category_theory.abelian.homology_c_to_k.category_theory.is_iso
{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) :
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) :
category_theory.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 = category_theory.limits.cokernel.π (category_theory.limits.kernel.lift g f w) ≫ (homology_iso_cokernel_lift f g w).inv
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) :
homology f g w ⟶ category_theory.limits.cokernel f
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)
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) :
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
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) :
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
@[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) :
category_theory.limits.kernel.lift g f w ≫ homology.π' f g w = 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') :
category_theory.limits.kernel.lift g f w ≫ homology.π' f g w ≫ f' = 0 ≫ 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) :
homology.ι f g w ≫ category_theory.limits.cokernel.desc f g w = 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') :
homology.ι f g w ≫ category_theory.limits.cokernel.desc f g w ≫ f' = 0 ≫ f'
@[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.π'_ι
{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) :
homology.π' f g w ≫ homology.ι f g w = category_theory.limits.kernel.ι g ≫ category_theory.limits.cokernel.π f
@[simp]
theorem
homology.π'_ι_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' : category_theory.limits.cokernel f ⟶ X') :
homology.π' f g w ≫ homology.ι f g w ≫ f' = category_theory.limits.kernel.ι g ≫ category_theory.limits.cokernel.π f ≫ f'
@[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) :
(category_theory.limits.kernel_subobject_iso g).hom ≫ homology.π' f g w = homology.π f g w
@[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') :
(category_theory.limits.kernel_subobject_iso g).hom ≫ homology.π' f g w ≫ f' = homology.π f g w ≫ f'
@[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) :
homology.π' f g w ≫ homology.map w w' α β h = category_theory.limits.kernel.map g g' α.right β.right _ ≫ homology.π' f' g' w'
@[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) :
homology.π' f g w ≫ homology.map w w' α β h ≫ f'_1 = category_theory.limits.kernel.map g g' α.right β.right _ ≫ homology.π' f' g' w' ≫ f'_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) :
homology.map w w' α β h = homology.desc' f g w (homology.lift f' g' w' (category_theory.limits.kernel.ι g ≫ β.left ≫ category_theory.limits.cokernel.π f') _) _
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) :
homology.map w w' α β h = homology.lift f' g' w' (homology.desc' f g w (category_theory.limits.kernel.ι g ≫ β.left ≫ category_theory.limits.cokernel.π f') _) _
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) :
homology.map w w' α β h = homology.desc' f g w (homology.lift f' g' w' (category_theory.limits.kernel.ι g ≫ α.right ≫ category_theory.limits.cokernel.π f') _) _
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) :
homology.map w w' α β h = homology.lift f' g' w' (homology.desc' f g w (category_theory.limits.kernel.ι g ≫ α.right ≫ category_theory.limits.cokernel.π f') _) _
@[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) :
homology.map w w' α β h ≫ homology.ι f' g' w' = homology.ι f g w ≫ category_theory.limits.cokernel.map f f' α.left β.left _
noncomputable
def
category_theory.functor.homology_iso
{A : Type u}
[category_theory.category A]
[category_theory.abelian A]
{ι : Type u_1}
{c : complex_shape ι}
{B : Type u_2}
[category_theory.category B]
[category_theory.abelian B]
(F : A ⥤ B)
[F.additive]
[category_theory.limits.preserves_finite_limits F]
[category_theory.limits.preserves_finite_colimits F]
(C : homological_complex A c)
(j : ι) :
When F is an exact additive functor, F(Hᵢ(X)) ≅ Hᵢ(F(X)) for X a complex.
Equations
- 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) _
noncomputable
def
category_theory.functor.homology_functor_iso
{A : Type u}
[category_theory.category A]
[category_theory.abelian A]
{ι : Type u_1}
{c : complex_shape ι}
{B : Type u_2}
[category_theory.category B]
[category_theory.abelian B]
(F : A ⥤ B)
[F.additive]
[category_theory.limits.preserves_finite_limits F]
[category_theory.limits.preserves_finite_colimits F]
(i : ι) :
homology_functor A c i ⋙ F ≅ F.map_homological_complex c ⋙ homology_functor B c i
If F is an exact additive functor, then F commutes with Hᵢ (up to natural isomorphism).
Equations
- F.homology_functor_iso i = category_theory.nat_iso.of_components (λ (X : homological_complex A c), F.homology_iso X i) _