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: theory: category theory

Topic: evil composition

dusko (May 08 2020 at 18:47):

Ha! I created a stream. The following might be of interest for public discussion.

Until a moment ago, I thought that complying with the basic principle of categorical ethics was easy: the arrows can be equal or not, but the objects can be isomorphic at best, and testing their equality is evil.

But the most basic operation of composition involves the object equality! The arrows $$f:A\to B$ and $g:C\to D$ can be composed if $B=C$, otherwise not. I do understand that I could implement categories so that the composition is defined with dependent types, using the definitional equality of the middle type. But what if there is some type-derivation going on on $B$ and $C$? What if they are vector spaces, given with no bases, but with the same dimension? Do I have to explicitly insert the isomorphism here? Being torn by moral doubts about evil aside, this would be a bit of a show stopper for doing linear algebra, wouldn't it?

Are there people here who still use tools with categories behind the screen? How do you handle this?

Morgan Rogers (he/him) (May 08 2020 at 19:27):

dusko said:

Ha! I created a stream. The following might be of interest for public discussion.

Congratulations! :tada: This looks like it would be more suitable (and get more attention) as a topic in a relevant existing stream, however. Did you know you can subscribe to streams you haven't been automatically subscribed to by clicking on the cog next to "STREAMS" and then clicking on "All Streams" in the top left?

Arthur Parzygnat (May 08 2020 at 20:49):

@dusko Can someone "drag" this stream and turn it into one of the topics on one of the streams already available? Or can you copy and paste what you wrote into one? The reason is because no one will see any discussions here unless they actively click on the stream (it does not show up in "all messages").
I had some thoughts about this a few years ago. Namely, what if a "functor" $F$ acting on $x\xrightarrow{\gamma}y$ does not respect sources and targets but does so only up to some coherent isomorphism. From what I recall, one could show that such a "functor" is "equivalent" (in a generalized sense) to an actual functor. So I stopped thinking about it since then haha.

sarahzrf (May 09 2020 at 01:08):

dusko said:

Do I have to explicitly insert the isomorphism here? Being torn by moral doubts about evil aside, this would be a bit of a show stopper for doing linear algebra, wouldn't it?

yes, you have to explicitly insert the iso; no, it's not a show-stopper

sarahzrf (May 09 2020 at 01:09):

i mean, a finite-dimensional vector space is isomorphic to its dual, but we certainly don't treat them as equivalent

sarahzrf (May 09 2020 at 01:10):

imo, definitional equality is absolutely the right way to think about the issue, and it's the reason why composition isn't evil

dusko (May 09 2020 at 03:22):

Morgan Rogers said:

dusko said:

Ha! I created a stream. The following might be of interest for public discussion.

Congratulations! :tada: This looks like it would be more suitable (and get more attention) as a topic in a relevant existing stream, however. Did you know you can subscribe to streams you haven't been automatically subscribed to by clicking on the cog next to "STREAMS" and then clicking on "All Streams" in the top left?

It would have saved me some learning if I found a stream that might be related to this. "Related" is of course relative, but I thought that dropping an unrelated question would be worse than creating a related stream. But if there is a related one, lets join this one there. Or simply shut it?

dusko (May 09 2020 at 03:23):

Arthur Parzygnat said:

dusko Can someone "drag" this stream and turn it into one of the topics on one of the streams already available? Or can you copy and paste what you wrote into one? The reason is because no one will see any discussions here unless they actively click on the stream (it does not show up in "all messages").
I had some thoughts about this a few years ago. Namely, what if a "functor" $F$ acting on $x\xrightarrow{\gamma}y$ does not respect sources and targets but does so only up to some coherent isomorphism. From what I recall, one could show that such a "functor" is "equivalent" (in a generalized sense) to an actual functor. So I stopped thinking about it since then haha.

i don't know how to do it. if anyone else does, or can do it, lets do it.

dusko (May 09 2020 at 03:41):

Arthur Parzygnat said:

dusko
I had some thoughts about this a few years ago. Namely, what if a "functor" $F$ acting on $x\xrightarrow{\gamma}y$ does not respect sources and targets but does so only up to some coherent isomorphism. From what I recall, one could show that such a "functor" is "equivalent" (in a generalized sense) to an actual functor. So I stopped thinking about it since then haha.

two functors can be equivalent, but the isomorphisms may be hard to construct. i think one could find simple examples where they are not computable. so a general equivalence proof may not help with the actual calculation. just like with the strictifications: e.g., every monoidal category can be made strictly associative and unitary, but that usually does not buy you anything practical. on the other extreme, $f:A\to B$ may land in one $n$-dim space $g:B'\to C$ may take inputs from another $n$-dim space. Sometimes it may be good to spell out the change of base from $B$ to $B'$ explicitly. But if we tell a mathematician that they cannot compose $f$ and $g$ unless they know the bases of $B$ and $B'$, and explain that this is because saying that $B$ and $B'$ are the same space is evil, they might give us a very careful, worried look.

sarahzrf (May 09 2020 at 04:20):

dusko said:

Morgan Rogers said:

dusko said:

Ha! I created a stream. The following might be of interest for public discussion.

Congratulations! :tada: This looks like it would be more suitable (and get more attention) as a topic in a relevant existing stream, however. Did you know you can subscribe to streams you haven't been automatically subscribed to by clicking on the cog next to "STREAMS" and then clicking on "All Streams" in the top left?

It would have saved me some learning if I found a stream that might be related to this. "Related" is of course relative, but I thought that dropping an unrelated question would be worse than creating a related stream. But if there is a related one, lets join this one there. Or simply shut it?

i think this is perfectly on-topic for #theory: category theory

sarahzrf (May 09 2020 at 04:21):

and again, i don't think they would give you a look

sarahzrf (May 09 2020 at 04:21):

do you really expect a typical mathematician to be happy with, say, applying a differential form to a cotangent vector instead of a tangent vector? (let's assume we're not given a riemannian structure or anything for converting between the two)

sarahzrf (May 09 2020 at 04:22):

the choice of isomorphism changes what the result of the composition is

sarahzrf (May 09 2020 at 04:22):

you can't just handwave it

sarahzrf (May 09 2020 at 04:23):

not unless you've fixed one ahead of time

sarahzrf (May 09 2020 at 04:25):

or, even better example:

sarahzrf (May 09 2020 at 04:27):

say p is a point in S²; then T_p S² is a 2d real vector space, so it is isomorphic to R². call it V. then id_V : V → V and id_{R²} : R² → R², so we can compose them and get a function V → R², right?

sarahzrf (May 09 2020 at 04:28):

then we can compose them in the other direction and get one R² → V, right? and compose those two, R² → V and then V → R², and end up with something R² → R²?

sarahzrf (May 09 2020 at 04:28):

now what's the determinant of this?