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: community: general

Topic: The projection formula

John Baez (Aug 27 2020 at 22:09):

I gave a proof of the "projection formula" that's so simple-minded even I could understand it:

• Frobenius reciprocity: In Wirthmüller contexts of six-operations yoga.

You don't need to know Frobenius reciprocity, Wirthmüller contexts, six operations or yoga to understand the statement and proof of Proposition 1.1. here.

John Baez (Aug 27 2020 at 22:09):

This is nothing new; it's just me trying to learn this stuff better by explaining it.

John Baez (Aug 27 2020 at 22:10):

I tweeted about it here:

https://twitter.com/johncarlosbaez/status/1299018669553459200

Hardcore math tweet: The "projection formula" or "Frobenius law" shows up in many branches of math, from logic to group representation theory to the study of sheaves. Let's see what it means in an example! (1/n) https://twitter.com/johncarlosbaez/status/1299018669553459200/photo/1

- John Carlos Baez (@johncarlosbaez)

David Michael Roberts (Sep 11 2020 at 07:48):

Heh, I've been using this recently in the context of base change for the self-indexing of a class category in algebraic set theory.

David Michael Roberts (Sep 11 2020 at 08:09):

Though, when I look at the nlab "proof", it's essentially

$f^\ast$ is a strong closed monoidal functor. This implies the projection formula, $\pi\colon f_!(f^*a\otimes c) \stackrel{\sim}{\to} a\otimes f_! c$

I can get the canonical map in the projection formula from tensoring the identity of $f^*a$ with the unit of $f_! \dashv f^*$, and using $f^*$ strong monoidal, to get $\pi\colon f^*a\otimes c \stackrel{\sim}{\to} f^*a\otimes f^*f_! c \simeq f^*(a\otimes f_! c)$, then use that $f_!$ is the left adjoint of $f^*$. But to get the isomorphism clearly one needs to use something else...

Rune Haugseng (Sep 11 2020 at 10:31):

If $f^*$ is a symmetric monoidal functor between closed symmetric monoidal categories, then some manipulation of adjunctions shows that the projection formula is equivalent to the natural map $f^* [x,y] \rightarrow [f^*x,f^*y]$ being an isomorphism (where I'm using square brackets for both internal Homs). I guess this is what is hidden in the assumption that $f^*$ is a closed symmetric monoidal functor.

John Baez (Sep 11 2020 at 20:27):

I don't know which nlab "proof" you're talking about. Did you look at the theorem I proved here?

• nLab, closed monoidal functors and the projection formula

John Baez (Sep 11 2020 at 20:28):

I hope this proof doesn't need quotation marks around it. :upside_down:

David Michael Roberts (Sep 12 2020 at 00:20):

Oh, then you linked in your original post to the wrong section. What I saw from

I gave a proof of the "projection formula" that's so simple-minded even I could understand it:

• Frobenius reciprocity: In Wirthmüller contexts of six-operations yoga.

You don't need to know Frobenius reciprocity, Wirthmüller contexts, six operations or yoga to understand the statement and proof of Proposition 1.1. here.

was

Screen-Shot-2020-09-12-at-9.47.07-am.png

And that left me entirely nonplussed, as I assumed that was what you had added! I agree that the actual proposition statement and proof attached, in the following section (linked to just now) is a proof!

David Michael Roberts (Sep 12 2020 at 00:27):

If I may be allowed to complain again, in the statement and proof, it keeps referring to natural transformations, but is silent on naturality in which slots of the component maps displayed. I can only guess that it is meant that the given maps are natural in all possible variables? So when there's an $a,b$ and $c$ appearing in the domain and codomain of an arrow, is the arrow supposed to be natural in all three?

David Michael Roberts (Sep 12 2020 at 00:29):

Maybe I don't like reading things like "let $x$ and $y$ be objects of a category. There is a natural transformation $x\to y$." I feel more comfortable reading "There is a natural map $x\to y$", for some reason.

John Baez (Sep 12 2020 at 01:28):

I rearranged the sections a couple of weeks after posting that... because I decided putting the proof in a section called "Wirthmüller contexts of six-operations yoga" was too off-putting.

John Baez (Sep 12 2020 at 01:29):

I can only guess that it is meant that the given maps are natural in all possible variables?

Sure, it's natural as can be. Otherwise I would have warned you.

John Baez (Sep 12 2020 at 01:44):

Feel free to improve anything you want...

David Michael Roberts (Sep 14 2020 at 01:22):

Will do! Just needed to get my bearings.

David Michael Roberts (Sep 14 2020 at 01:30):

Done. Only a minor tweak, but to me, at least, less confusing.

John Baez (Sep 14 2020 at 15:04):

Less confusing is good. (I won't look at it... I'm done with thinking about this for now.)