Is there a better way to define this? (category theory)

Stream: new members

[Jujian Zhang]

In an abelian category, given an exact sequence $0 \xrightarrow[]{} A \xrightarrow[]{f} B \xrightarrow[]{g} C$ and a $h : D\rightarrow B$ such that $gh=0$. I want a map $h' : D \rightarrow A$ such that $f h' = h$. My method of creating such $h'$ involves rewriting equality between kernel subobject and image subobject so it is very difficult to use it when proving commutativity. Is there any way to create $h'$ without using eq.mp? Thank you very much.

import category_theory.abelian.exact

noncomputable theory

open category_theory
open category_theory.limits

universes v u

variables {V : Type u} [category.{v} V] [abelian V]

open_locale zero_object


variables {A B C D : V}

/--
                D
                |
                h
                |
                v
0 ---> A --f--> B --g--> C
-/

variables {f : A ⟶ B} {g : B ⟶ C} {h : D ⟶ B} [exact f g] [mono f]
variables (eq_zero : h ≫ g = 0)


include g eq_zero

example : ∃ h' : D ⟶ A, h' ≫ f = h :=
begin
  have eq0 : (D ⟶ kernel_subobject g) = (D ⟶ image_subobject f),
    rw (abelian.exact_iff_image_eq_kernel f g).1 (by apply_instance),

  set h' : D ⟶ A :=
    (eq.mp eq0
      (kernel.lift g h eq_zero ≫ (kernel_subobject_iso g).inv)) ≫ (image_subobject_iso f).hom
      ≫ image.lift (mono_factorisation.self f) with h'_eq,
  use h',
  have eq1 : (mono_factorisation.self f).m = f := rfl,
  have : image.lift (mono_factorisation.self f) ≫ f = image.lift (mono_factorisation.self f) ≫ (mono_factorisation.self f).m,
    rw eq1,
  rw [h'_eq, category.assoc, category.assoc, this, image.lift_fac, image_subobject_arrow],

  sorry
end

[Andrew Yang]

I'm no expert in the library of abelian categories, but I would try this :

import category_theory.abelian.exact

noncomputable theory

open category_theory
open category_theory.limits

universes v u

variables {V : Type u} [category.{v} V] [abelian V]

open_locale zero_object


variables {A B C D : V}

/--
                D
                |
                h
                |
                v
0 ---> A --f--> B --g--> C
-/

variables (f : A ⟶ B) (g : B ⟶ C) {h : D ⟶ B} [exact f g] [mono f]
variables (eq_zero : h ≫ g = 0)

lemma is_kernel : is_limit (kernel_fork.of_ι f (show f ≫ g = 0, by simp)) :=
begin
  haveI : is_iso ((abelian.is_limit_image f g).lift
    (kernel_fork.of_ι f (show f ≫ g = 0, by simp))),
  { convert category_theory.abelian.images.is_iso_factor_thru_image f using 1 },
  exact (abelian.is_limit_image f g).of_point_iso
end

include g eq_zero

example : ∃ h' : D ⟶ A, h' ≫ f = h :=
begin
  have := kernel_fork.is_limit.lift' (is_kernel f g) h eq_zero,
  exact ⟨this.1, this.2⟩,
end

IMO the first lemma should be in mathlib, but I couldn't find it.

[Jujian Zhang]

Thank you! This is a much nicer solution.

[Jujian Zhang]

In this repo, I attempt to prove snake lemma. Now I have defined the connecting map modulo some sorrys like above and exactness everywhere except at connecting map. But the code are badly written, so does any one want to give me some advice on refactoring? Thank you!
https://github.com/jjaassoonn/mathlib

[Johan Commelin]

@Jujian Zhang Note that snake is also done in the LTE repo

[Johan Commelin]

I hope that it will move to mathlib in the next two months