Definition of diagram. When you draw an actual, what I call "diagram" on paper, it may have:
- Duplicated objects and arrows which is still valid.
- You don't always put in the compositions, as that would make displaying the diagram impossible sometimes.
- In the subclass commutative diagrams, you can't even always compose and retain commutativity.
To see the last point, draw something that commutes, and then draw an arrow connecting to the diagram like a hair (the compositions aren't filled in, and only one end of the arrow meets the first diagram). So, even though that diagram commutes between any two paths sharing domain/codomain, you can't always fill in all compositions!
Thus, how should we define "drawn diagrams" formally, in order to distinguish them from the functor definition?
I think it would help out the theory a bit, since once you define drawn diagrams, you can define their basic properties. It is important for my work on BananaCats to make this distinction, since diagram drawing is a big part of the app.
In other words, the definition of drawn diagram should have a 1-1 correspondence with the items drawn on a canvas, where items are either: arrow, object, each of which has a label, and such that two distinct items are not equal when their labels are, though they map to a category in which the two items are equal.
Something like this:
A drawn diagram in the category $C$ is a directed, labeled graph $G = (E, V)$ and a map $F : E \cup V \to \text{hom}(C) \cup \text{ob}(C)$ such that if $f : u \to v$ is an edge in $G$, then $F(f) : F(u) \to F(v)$ in $C$.
A commutative drawn diagram in a category $C$ is a drawn diagram such that whenever $u_1 = v_1$, $u_n = v_m$, and $f := u_1 \xrightarrow{f_1} \cdots \xrightarrow{f_n} u_n$ and $g := v_1 \xrightarrow{g_1} \dots \xrightarrow{g_n} v_m$ are paths in $G$ then $\bigcirc_{i=1}^n F(f_i) = \bigcirc_{i=1}^m F(g_i)$.