My question
I thought the author of this question was really pushing for what I'm asking here and I don't think it was ever fully addressed in other questions (happy to be wrong!).
My main question is Is there a way to prove associativity of the tensor product using only mapping diagrams and the universal property?
My setup and preferences
I'm happy to see how I didn't understand how to translate a traditional proof into this style but I don't want any uses of freeness, element analysis in the tensor product, or bases. To avoid confusion, below I'll give my definitions and be clear about what I want here.
Categories Vect and Set: I assume that I have a category Vect whose objects are vector spaces and morphisms are linear maps, with a forgetful functor $\text{Fo}: {\bf Vect} \to {\bf Set}$, and that ${\bf Set}$ is a unital associative monoidal category under the cartesian product, $(X,Y) \mapsto X \times Y$. In particular below I'll use the unitor isomorphism $X \xrightarrow{i} \{\star\} \times X$. Note that the forget functor allows me to talk about when a function between vector spaces is a linear map, which I'll need below.
Defininig bilinearity: Next I assume that I have the following notion of bilinear map: Given three vector spaces $V$,$W$, and $Z$ in ${\bf Vect}$, a morphism $b: \text{Fo}(V)\times \text{Fo}(W) \to \text{Fo}(Z)$ is called bilinear if
- for any choice of set function (i.e base point) $p: \{ \star\} \to \text{Fo}V$, the composition $$\text{Fo}W \xrightarrow{i} \{\star\} \times \text{Fo}W \xrightarrow{p \times id} \text{Fo}V \times \text{Fo}W \xrightarrow{\text{Fo}b} \text{Fo}Z$$ is in the image of the forgetful functor (i.e. is a linear map).
- similarly for any choice of base point in $\text{Fo}W$ we have an analogous linear map.
The universal property:. We assume in ${\bf Vect}$ that for each pair of vector spaces $V$ and $W$ there exists a vector space $V \otimes W$ and a bilinear map $t: \text{Fo}V \times \text{Fo}W \to \text{Fo}(V \otimes W)$ satisfying:
For any vector space $Z$ and bilinear map $b: \text{Fo}V \times \text{Fo}W \to \text{Fo}Z$ there exists a unique linear map $L_b: V \otimes W \to Z$ making the induced triangular diagram in ${\bf Set}$ commute (i.e. $\text{Fo}(L_b) \circ t = b$).
Why I'm so bothered by this
I see how to prove all of the following about the tensor product except for associativity.
- The tensor product is commutativity up to isomorphism
- The tensor product over $\mathbb{F} = \mathbb{R}, \mathbb{C}$ is unital up to isomorphism with unit being $\mathbb{F}$. Perhaps this is where everything falls apart, but if I assume the axioms for a vector space, we do have a pairing $\mathbb{R} \times V \to V$ and I can use this and the commutative diagrams of the axioms to achieve the result. (I almost deleted this entire question when I got to this part so feel free to pick it apart :) )
- If we had a particular choice of $V \otimes W$ so that we could change the words "there exists" to "we assign" or something, then we have a unital bifunctor on ${\bf Vect}$.
So it seems to me that even if I have to go out of my way to do it, there ought to be some proof for associativity in similar styles. Please help!
In category theory tensor products are bi-functors $$\ast \otimes \ast : \text{Mod}\!-\!A \times A\!-\!\text{Mod} \longrightarrow \text{Ab}.$$
where Ab denotes the category of abelian groups, $A$ a ring, $A$-Mod the left $A$-modules and Mod-$A$ the right $A$-modules (in your case $A = k$ your ambiant field and vector spaces are $k$-bimodules since $k$ is commutative). Its definition (unique up to natural bi-isomorphism) is given by its universal property of factorisation of bilinear maps. I won't bother rewriting it. You seem to have found a "nice" way to depict bilinear maps (but you still make choices within it).
Then the associativity is a direct consequence of the associativity of the cartesian product (you don't need to work on the elements $m \otimes n \otimes l$) so it remains to show the associativity of the cartesian product without working on elements, which seems complicated if you work with axioms of Z-F).
I don't know if it was helpful, maybe we need to make all the work for the Set category I have no idea, you can check some references e.g. book about category theory or homological algebra, it may lie within one of these...