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 0AfBgC0 \xrightarrow[]{} A \xrightarrow[]{f} B \xrightarrow[]{g} C and a h:DBh : D\rightarrow B such that gh=0gh=0. I want a map h:DAh' : D \rightarrow A such that fh=hf h' = h. My method of creating such hh' 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 hh' 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