## Stream: new members

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

#### Jujian Zhang (Dec 03 2021 at 09:55):

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 (Dec 03 2021 at 10:46):

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

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

#### Jujian Zhang (Dec 03 2021 at 11:29):

Thank you! This is a much nicer solution.

#### Jujian Zhang (Dec 03 2021 at 16:38):

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 (Dec 03 2021 at 17:16):

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

#### Johan Commelin (Dec 03 2021 at 17:16):

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

Last updated: Dec 20 2023 at 11:08 UTC