Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: event: NYC Category Theory

Topic: Picturing Quantum Processes

Spencer Whitt (May 11 2020 at 00:05):

I took a stab at solving the type issue in question 3.38. I started by rephrasing the given rules for $0$ more clearly. I've labeled the types and numbered $f_1 f_2 f_3 f_4$ to show that they need not be the same. I've also repeated the rule twice, once $0_1$ and once for $0_2$. This makes it clear that each $0_i$ is actually a family of processes - there is a separate process $0_i$ for each type $A \to B$, and they are related by the given rules - but crucially the given rules do not indicate any explicit relationship between $0_1$ and $0_2$. With this established, the proof is straight forward and demonstrates that $0_1 = 0_2$ for any arbitrary types A and C. @Oliver Shetler @Wenbo Gao CCI05102020.jpg

Wenbo Gao (May 11 2020 at 00:24):

Yeah I think you are right. The first f should be different from the second f and similarly for 0s.

Oliver Shetler (May 11 2020 at 00:49):

image-720fa46c-21da-4a01-a6c3-0b8fba542c0c.jpg

Oliver Shetler (May 11 2020 at 00:49):

This works. If we add the diagram with the parallel composition with zero, we can prove the insertion induction too.

Spencer Whitt (May 11 2020 at 02:03):

What is "insertion induction"? Are you asserting that this diagram proves the theorem? I can see that it's a true diagram, but I don't see how it proves the theorem - after all, it only has one type of 0. It needs two different 0's in order to prove they are equal. Here is a version of my proof using 0 numbers for comparison. IMG_20200510_215944.jpg

Oliver Shetler (May 11 2020 at 14:35):

What I'm saying is that if you include the additional condition and prove that all zero processes of all types are equivelant to multiplying any process by the unique number zero, you get the result I posted. In fact, you get the even stronger induction that any diagram with the same input and output wires multiplied by zero is the same as any insertion of any admissable type of zero process.

Spencer Whitt (May 11 2020 at 15:55):

Are you able to establish that the number 0 is unique, without the use of the proofs I posted?

Oliver Shetler (May 11 2020 at 16:32):

Why would I be? I said if we add the extra equation, we get the induction from your proofs.

Spencer Whitt (May 11 2020 at 17:31):

Ahh ok I was just misunderstanding you. I think we're on the same page now. All of this does indeed follow.