diagram chase map

Stream: Is there code for X?

[Kevin Buzzard]

Given the following commutative diagram
Screenshot 2025-07-28 at 13.33.59.png

in a (concrete) abelian category, with exact rows, I'd like to define the dotted morphism by "given $c$ in $C$, randomly pull back to $b\in B$, push down to $E$ and then along to $F$, and this is well-defined because if I choose another $b$ the difference is in $A$ which dies by the time it gets to $F$ because $D\to E\to F$ is the zero map", and I'd like to know that the square with the dotted side is commutative.

Is this the sort of thing we just have machinery for nowadays? I have formalized it as top and bottom : ShortComplex C and the hypothesis Epi (top.g) but I am flexible, I just don't want to do the diagram chase myself if it's already there, but I have no real idea about how to search for it. Loogling for CategoryTheory.Epi, CategoryTheory.ShortComplex gave me 123 results and the first few did not look like what I wanted.

[Markus Himmel]

If I'm not mistaken this should follow from docs#CategoryTheory.ShortComplex.Exact.desc

[Aaron Liu]

import Mathlib

universe u v
open CategoryTheory

variable {C : Type u} [Category.{v} C] [Preadditive C] [Balanced C] {top : ShortComplex C} {bot : ShortComplex C}
    (top_exact : top.Exact) [Epi top.g] {hom1 : top.X₁ ⟶ bot.X₁} {hom2 : top.X₂ ⟶ bot.X₂}
    (comm : CommSq top.f hom1 hom2 bot.f)

noncomputable def hom3 : top.X₃ ⟶ bot.X₃ :=
  top_exact.desc (hom2 ≫ bot.g) <| by
    rw [← Category.assoc, comm.w, Category.assoc, bot.zero, Limits.comp_zero]

theorem hom3_comm : CommSq top.g hom2 (hom3 top_exact comm) bot.g where
  w := top_exact.g_desc (hom2 ≫ bot.g) _

[Kevin Buzzard]

Thanks, yes, this will surely do. Somehow the more general question is how one can search for such a result without having to ask here, but right now I'm just happy I can proceed :-)

[Aaron Liu]

I did loogle and it gave me what I wanted

[Aaron Liu]

@loogle CategoryTheory.ShortComplex.Exact, |- _ ⟶ _

[loogle]

:search: CategoryTheory.ShortComplex.Exact.desc, CategoryTheory.ShortComplex.Exact.lift, and 2 more

[Aaron Liu]

first result :)

[Kevin Buzzard]

Aah I see, I should demand that the answer is a morphism. I see I also didn't ask for exactness in my attempt.

[Joël Riou]

The first line can be understood as a "colimit cokernel cofork" (C is the cokernel of the map from A to B). Then, the map from C can be constructed using docs#CategoryTheory.Limits.CokernelCofork.IsColimit.desc' (or by applying directly IsColimit.desc, which is what ShortComplex.Exact.desc does).
(One difficulty with the formalization of homological algebra is that there are many different ways to state properties of diagrams.)