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: contravariant strengths

Asad Saeeduddin (Jan 08 2022 at 13:35):

In his comment here, @Todd Trimble mentions that C.S. Peirce first understood strengths, and that he additionally worked out a notion of contravariant strength. I've been unable to dig up any sources that explain this further. Would anyone happen to know of what Todd is referring to?

Todd Trimble (Jan 08 2022 at 14:45):

Do you know about existential graphs, Asad? This is the topic of my paper with Gerry Brady, A categorical interpretation of C. S. Peirce's System Alpha. Journal of Pure and Applied Algebra, 149: 213-239, 2000. Hopefully it explains what I had in mind.

Also, please bear in mind that I said, within the relaxed and casual atmosphere of the Cafe, that he "intuitively understood" strengths. Maybe if I were trying to be more careful, I would have said instead this: he would have found very obvious the idea of a covariant strength as expressing inferences in the language of Boolean algebras

$p(x) \wedge y \to p(x \wedge y)$

if $p$ is a covariant unary operator definable in that language, and a contravariant strength

$p(x \wedge y) \wedge y \to p(x)$

if $p$ is a contravariant unary operator in that language. Only, he very cleverly wrote down instead inference rules that he called iteration/deiteration, that get at both cases at once. These roughly say

$p(x) \wedge y \leftrightarrow p(x \wedge y) \wedge y$

where the forward direction is called "iteration" and the backward direction is called "deiteration". These rules, combined with rules of type $a \wedge b \to a$ (which he called "weakening" (!)), give us rules for covariant and contravariant strength within this language. One other feature of his system is that he did all this diagrammatically, using a graphical notation which looks strikingly like string diagrams.

(So what I was getting at in the nLab comment is that similarly, any covariant unary operator definable in the language of symmetric monoidal closed categories has a canonical strength, and so do contravariant unary operators, although I'm not sure that contravariant strengths are in common currency.)

Asad Saeeduddin (Jan 08 2022 at 15:58):

Do you know about existential graphs, Asad?

I do not, but I have been learning since I encountered your comment!

Asad Saeeduddin (Jan 08 2022 at 15:59):

Thanks for the paper reference, I'll dig that up now

Asad Saeeduddin (Jan 08 2022 at 16:10):

Hmm. Am I to understand correctly that the reliance on weakening is somehow involving cartesian structure (if I were to attempt to transport this to a setting besides Boolean algebras)? Is there a way to restrict ourselves to using only closed monoidal structure in defining contravariant strength?

Todd Trimble (Jan 08 2022 at 16:24):

Yes. Suppose we have a symmetric monoidal category $\mathcal{C}$. If you know the connection between strengths and enrichments for (covariant) functors $F: \mathcal{C} \to \mathcal{C}$, then you can probably figure out how to get from a $C$-enrichment for a functor $F: \mathcal{C}^{op} \to \mathcal{C}$ to this proposed notion of contravariant strength, whose structure is given by a map $F(x \otimes y) \otimes y \to F(x)$ that is natural in $x$ and extranatural in $y$.

I'd be happy to go into details when I feel like I have more time, but for now you can take this as a hint (which I hope is followable). :-)

Todd Trimble (Jan 08 2022 at 16:54):

Well, "more time" means getting up to grab a pen and some paper and scribble things down, so I will say a little more now. :-)

In the Cafe comment, I described one direction, which takes you from a strength to an enrichment for a functor $F: \mathcal{C} \to \mathcal{C}$. I left the other way as an exercise, but I'll write down a partial solution here. Given a $\mathcal{C}$-enrichment on $F$, i.e., a collection of maps

$[x, y] \to [Fx, Fy]$

in $\mathcal{C}$ that are natural in $x, y$ and satisfying some axioms, you can get a strength on $F$ by forming the composite

$x \to [y, x \otimes y] \to [Fy, F(x \otimes y)]$

where the first map is the component $\eta_x$ of the counit $\eta$ for the adjunction $- \otimes y \dashv [y, -]$. This composite transforms to a natural family of maps

$x \otimes Fy \to F(x \otimes y)$

and this defines the associated strength, at least in the case of covariant $F$.

Similarly, in the case of $F: \mathcal{C}^{op} \to \mathcal{C}$, a $\mathcal{C}$-enrichment of $F$ means we have a natural family of maps

$[x, y] \to [Fy, Fx]$

satisfying some enriched functoriality axioms. As before, we can then form a composite

$x \to [y, x \otimes y] \to [F(x \otimes y), Fy]$

and then these transform to maps

$x \otimes F(x \otimes y) \to Fy$

that are natural in $x$ and dinatural in $y$, and one can translate the enriched functoriality axioms one by one into contravariant strength axioms. For example, one will obtain an axiom that says the constraint

$(x \otimes y) \otimes F((x \otimes y) \otimes z) \to Fz$ can be decomposed into two such constraints

$x \otimes y \otimes F(x \otimes y \otimes z) \to y \otimes F(y \otimes z) \to Fz$.

I don't recall ever seeing this in print, but I've found it useful, at least in private calculations.

Todd Trimble (Jan 08 2022 at 16:59):

"I don't recall ever seeing this in print, but I've found it useful, at least in private calculations."

Well, it might be in that paper with Gerry; I don't remember right now.

John Baez (Jan 08 2022 at 18:41):

This is the topic of my paper with Gerry Brady, A categorical interpretation of C. S. Peirce's System Alpha. Journal of Pure and Applied Algebra, 149: 213-239, 2000.

By the way, that paper is available here.

Asad Saeeduddin (Jan 08 2022 at 21:15):

@Todd Trimble thanks very much, that's super helpful. i was for some reason getting hung up on the fact that C^op is not closed, when that is not actually a necessary feature for having an enrichment of the contravariant functor