The proof of the following fact is trivial to most Arrow theorists / Linear algebraists, but I'm developing software that needs to "understand" in a sense this basic fact, because it is called upon all the time, so should be provable to the users of the software, in the software itself.
We are given the following diagram and the user is told that it commutes by definition.
The goal diagram is the following:
Using only the rules:
- Definition of kernel / image: What should we use here?
- Gluing two CD's along a common subdiagram and the resulting diagram is a CD.
- Deleting arrows in a CD and the diagram will still be a CD.
- You can compose along two paths in a CD with common endpoints and the resulting arrows are equal.
- Any others we require.
So I'm wondering about the definition of Kernel / Image. Clearly I'm using the one in which kernel / image are spaces, not maps. What is the most light-weight, yet most diagrammatic definitions of these.
Finally, how would the diagrammatic proof go given that, for example, the diagrams are of $R$-modules and $R$-module map?.
To create a visual diagram I used https://q.uiver.app. From there, create the diagram, turn off the grid and take a screenshot of it with Windows + Shift + S (or similar on other OS's), selecting a small region containing just the diagram, and then paste into the insert-image tool here.
Note: in the system language, dashed arrow means "there exists" whereas a normal arrow means "for all such" if it doesn't appear in surrounding text or it is simply the exact thing that the surrounding text talks about. So in the first diagram, $f,g$ both appear in the text, so they are "bound" whereas other variables might be "free to roam".
Edit. I got the vocabulary of "free" vs "bound" variable backwards. A bound variable is either a "there exists" or a "for all" variable for example (there are other variable-binding operators), where as a free variable is the one that occurs in the text for example "Definition of equalizer morphism $e$ is ..." so in the ... $e$ would be free. We can think of this nicely as bound variables are introduced inside the "box of a diagram" whereas free variables are "free from the box" and are typically introduced outside of a diagram.