feat(category_theory/abelian/*): add some missing lemmas (#12839)

src/category_theory/abelian/exact.lean

@@ -172,6 +172,14 @@ lemma cokernel.desc.inv [epi g] (ex : exact f g) :
   g ≫ inv (cokernel.desc _ _ ex.w) = cokernel.π _ :=
 by simp
 
+instance [ex : exact f g] [mono f] : is_iso (kernel.lift g f ex.w) :=
+  is_iso_of_mono_of_epi (limits.kernel.lift g f exact.w)
+
+@[simp, reassoc]
+lemma kernel.lift.inv [mono f] (ex : exact f g) :
+  inv (kernel.lift _ _ ex.w) ≫ f = kernel.ι g :=
+by simp
+
 /-- If `X ⟶ Y ⟶ Z ⟶ 0` is exact, then the second map is a cokernel of the first. -/
 def is_colimit_of_exact_of_epi [epi g] (h : exact f g) :
   is_colimit (cokernel_cofork.of_π _ h.w) :=

src/category_theory/abelian/homology.lean

@@ -254,6 +254,16 @@ lemma map_eq_lift_desc'_right (α β h) : map w w' α β h =
   (by { ext, simp [h] }) :=
 by { rw map_eq_desc'_lift_right, ext, simp }
 
+@[simp, reassoc]
+lemma map_ι (α β h) :
+  map w w' α β h ≫ ι f' g' w' = ι f g w ≫ cokernel.map f f' α.left β.left (by simp [h, β.w.symm]) :=
+begin
+  rw [map_eq_lift_desc'_left, lift_ι],
+  ext,
+  simp only [← category.assoc],
+  rw [π'_ι, π'_desc', category.assoc, category.assoc, cokernel.π_desc],
+end
+
 end
 
 end homology