feat(algebra/homology,category_theory/abelian): exact_comp_mono_iff (#…

…14410)

From LTE.

src/algebra/homology/exact.lean

@@ -198,13 +198,17 @@ begin
   apply_instance,
 end
 
+/-- The dual of this lemma is only true when `V` is abelian, see `abelian.exact_epi_comp_iff`. -/
+lemma exact_comp_mono_iff [mono h] : exact f (g ≫ h) ↔ exact f g :=
+begin
+  refine ⟨λ hfg, ⟨zero_of_comp_mono h (by rw [category.assoc, hfg.1]), _⟩, λ h, exact_comp_mono h⟩,
+  rw ← (iso.eq_comp_inv _).1 (image_to_kernel_comp_mono _ _ h hfg.1),
+  haveI := hfg.2, apply_instance
+end
+
 @[simp]
 lemma exact_comp_iso [is_iso h] : exact f (g ≫ h) ↔ exact f g :=
-⟨λ w, begin
-    rw [←category.comp_id g, ←is_iso.hom_inv_id h, ←category.assoc],
-    exactI exact_comp_mono w,
-  end,
-  λ w, exact_comp_mono w⟩
+exact_comp_mono_iff
 
 lemma exact_kernel_subobject_arrow : exact (kernel_subobject f).arrow f :=
 begin

src/category_theory/abelian/exact.lean

@@ -121,6 +121,17 @@ begin
     is_iso.comp_right_eq_zero _ (cokernel_comparison f F)],
 end
 
+/-- The dual result is true even in non-abelian categories, see
+    `category_theory.exact_epi_comp_iff`. -/
+lemma exact_epi_comp_iff {W : C} (h : W ⟶ X) [epi h] : exact (h ≫ f) g ↔ exact f g :=
+begin
+  refine ⟨λ hfg, _, λ h, exact_epi_comp h⟩,
+  let hc := is_cokernel_of_comp _ _ (colimit.is_colimit (parallel_pair (h ≫ f) 0))
+    (by rw [← cancel_epi h, ← category.assoc, cokernel_cofork.condition, comp_zero]) rfl,
+  refine (exact_iff' _ _ (limit.is_limit _) hc).2 ⟨_, ((exact_iff _ _).1 hfg).2⟩,
+  exact zero_of_epi_comp h (by rw [← hfg.1, category.assoc])
+end
+
 /-- If `(f, g)` is exact, then `images.image.ι f` is a kernel of `g`. -/
 def is_limit_image (h : exact f g) :
   is_limit