Zulip Chat Archive
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