Complete speculation here but nonetheless very interesting.
The cup and cap can be seen as lollipopped unital laws as shown below:
Once you lollipop the unital law you can add in two identity morphisms that are dual of each other and the tensor product of the two is the identity matrix. This is interesting because this complex was an identity morphism to start off with!
We can add a real morphism A into the picture as below:
You can add the morphism on either side and you will have the same result, an morphism going from \\(y^\ast \rightarrow x^\ast\\). But we can once again introduce the inverse of A to make the whole complex become a identity morphism and we get \\(A^{-1}A = I = AA^{-1}\\)!
Maybe someone with more experience can verify if this checks out and/or explain the details further? I was trying to figure out where \\(A^{-1}A = I = AA^{-1}\\) and \\(x^\ast I x = x^\ast (A^{-1}A) x\\) in comment 28 above was coming from and entered this hall of mirrors LOL. Would be great if someone can take us down the rabbit hole a little deeper.
The cup and cap can be seen as lollipopped unital laws as shown below:
Once you lollipop the unital law you can add in two identity morphisms that are dual of each other and the tensor product of the two is the identity matrix. This is interesting because this complex was an identity morphism to start off with!
We can add a real morphism A into the picture as below:
You can add the morphism on either side and you will have the same result, an morphism going from \\(y^\ast \rightarrow x^\ast\\). But we can once again introduce the inverse of A to make the whole complex become a identity morphism and we get \\(A^{-1}A = I = AA^{-1}\\)!
Maybe someone with more experience can verify if this checks out and/or explain the details further? I was trying to figure out where \\(A^{-1}A = I = AA^{-1}\\) and \\(x^\ast I x = x^\ast (A^{-1}A) x\\) in comment 28 above was coming from and entered this hall of mirrors LOL. Would be great if someone can take us down the rabbit hole a little deeper.
Version 2.1.8p2
