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: learning: questions

Topic: History of $$\dashv$$

Jules Hedges (Mar 10 2021 at 18:44):

Matteo Capucci (he/him) said:

Morgan Rogers (he/him) said:

In what context? You'll notice that when you write out the correspondence defining an adjunction, the left adjoint functor appears on the left of the arrow (assuming it's pointing from left to right). That is, an adjunction $L \dashv R$ give a correspondence between morphisms $LX \to Y$ and morphisms $X \to RY$.

I just noticed that $\dashv$ looks like an arrow $\to$, whose direction is the correct one (from the left adjoint to the right adjoint)

This makes me wonder, does anyone know who invented the symbol $\dashv$ (was it Kan?), and why they chose that symbol? Is it supposed to have any relation to the turnstile from logic, or was it just a random symbol? Maybe it was used for adjoints in linear algebra or somewhere else, earlier than adjoint functors?

Joe Moeller (Mar 10 2021 at 18:59):

I've never seen $\dashv$ in linear algebra.

Matteo Capucci (he/him) (Mar 10 2021 at 19:04):

Mmh I'd be surprised if it's not related to the logicians' $\vdash$

Fawzi Hreiki (Mar 10 2021 at 19:13):

The notation is introduced in the Kan’s paper on adjoint functors. The story goes that Eilenberg suggested the name adjoint because of some analogy with adjoint operators in functional analysis. So I’m guessing the notation comes from the notation for orthogonality in functional analysis

Matteo Capucci (he/him) (Mar 10 2021 at 19:18):

make sense

Matteo Capucci (he/him) (Mar 10 2021 at 19:18):

(we have a $\neg$ Kan emoj, but not a Kan one)

Fawzi Hreiki (Mar 10 2021 at 19:31):

I guess because we can just assume that everything is a Kan extension anyway

James Wood (Mar 10 2021 at 19:33):

Was it originally $\bot$ in a diagram?

Nathanael Arkor (Mar 10 2021 at 19:34):

Matteo Capucci (he/him) said:

(we have a $\neg$ Kan emoj, but not a Kan one)

That's because everything is assumed by default to be a Kan extension.

James Wood (Mar 10 2021 at 19:35):

I.e,

 /--F--v
A   ⊥   B
 ^--G--/

Fawzi Hreiki (Mar 10 2021 at 19:38):

No. In the paper the notation is introduced sideways as $F \dashv G$

John Baez (Mar 11 2021 at 07:28):

Wow, I never knew where this devilish symbol came from.

Jules Hedges (Mar 11 2021 at 12:14):

Objectively speaking, I think it's not that great of a symbol. Of course it can never be changed, but it might be fun to crowd-source a better choice of symbol for an adjunction

Fabrizio Genovese (Mar 11 2021 at 12:58):

Last time someone crowdsourced a name, a research ship of the Royal Navy was about to be called Boaty McBoatface...

Chad Nester (Mar 11 2021 at 13:04):

My attempt: $\stackrel{\to}{\leftrightsquigarrow}$

Chad Nester (Mar 11 2021 at 13:04):

so... it could be worse!

Jules Hedges (Mar 11 2021 at 13:05):

The Comprehensive LaTeX Symbol List or however it's called is my go-to document whenever I need to invent a symbol for something, and it definitely has some fun possibilities for joke answers.... there's definitely a package in there defining commands to draw Simpsons characters for example

Jules Hedges (Mar 11 2021 at 13:06):

Maybe F \Maggie G could catch on...

Matteo Capucci (he/him) (Mar 11 2021 at 13:21):

Maybe that way we'll get a couch gag on category theory

Ralph Sarkis (Mar 11 2021 at 13:25):

We have already seen string diagrams on Rick and Morty: image.png

Matteo Capucci (he/him) (Mar 11 2021 at 13:28):

:joy: Right, it wouldn't even be a first

Fawzi Hreiki (Mar 11 2021 at 13:41):

I think $\dashv$ is a pretty good notation. Apart from the entailment relation in logic, it doesn’t really clash with anything and it even looks like a weird L

Fawzi Hreiki (Mar 11 2021 at 13:42):

Plus it works well for diagrams with multiple adjunctions

Fabrizio Genovese (Mar 11 2021 at 14:51):

Ralph Sarkis said:

We have already seen string diagrams on Rick and Morty: image.png

I remember this very well. I don't think it's by chance, those are literally the snake equations done with spiders on Bob and Aleks ' book.

Matteo Capucci (he/him) (Mar 11 2021 at 14:52):

100% they Googled 'snake equations images', found those, and played along

Jules Hedges (Mar 11 2021 at 14:53):

If I remember correctly there's quite a bit more to it than that... but Bob may not want to talk about it in public

Ralph Sarkis (Mar 11 2021 at 14:57):

They are from Section 4 (p.24) of https://arxiv.org/pdf/1912.10049.pdf
And there is an extra $=$ sign which makes the derivation wrong.

Mike Shulman (Mar 11 2021 at 16:35):

I think $f: C\rightleftarrows D : g$ works pretty well.