Ramana Kumar comments on Multiplicative Operations on Cartesian Frames

Ramana Kumar 17 Dec 2020 14:49 UTC
LW: 3 AF: 2
AF
Since we have already established commutativity, it suffices to show that $(C_{0} \otimes C_{1}) \otimes C_{2} ≅ (C_{0} \otimes C_{2}) \otimes C_{1}$ .
For the confused reader, the argument in more detail here is:
$\begin{matrix} C_{0} \otimes (C_{1} \otimes C_{2}) ≅ (C_{1} \otimes C_{2}) \otimes C_{0} & comm ≅ (C_{1} \otimes C_{0}) \otimes C_{2} & lemma ≅ (C_{0} \otimes C_{1}) \otimes C_{2} & comm, iso \end{matrix}$
where $comm$ is commutativity of tensor, $lemma$ is the fact claimed to suffice above, and $iso$ is the implicitly assumed lemma that $C_{0} ≅ C_{1}$ and $D_{0} ≅ D_{1}$ implies $C_{0} \otimes D_{0} ≅ C_{1} \otimes D_{1}$ (this is proved later but only for $≃$ ).