Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

August 3, 2021

The Two Cultures Challenge Revisited

Posted by David Corfield

Since I was reminded of the ‘Two cultures’ discussions (I and II) while replying to John on the other thread, I wonder if with the advantage of 14 more years we can now meet Terry Tao’s challenge to provide a category-theoretic proof of

If f:XYf: X \to Y is a function between finite sets, then |X× fX||X| 2/|Y||X \times_{f} X| \geq |X|^2/|Y|.

We were also given a simpler and a more general version:

If XX and YY are disjoint sets, then (X×X)(Y×Y)(X \times X) \cup (Y \times Y) is at least as large as (X×Y)(Y×X)(X \times Y) \cup (Y \times X).

If f:XYf: X \to Y and g:ZYg: Z \to Y then (X× YX)×(Z× YZ)(X \times_Y X) \times (Z \times_Y Z) is at least as large as (X× YZ)×(Z× YX)(X \times_Y Z) \times (Z \times_Y X).

Terry’s summary here is handy, pointing out that Robin Houston had got us part of the way, here.

I see back then Urs was wondering if Tom’s new ideas on cardinality were relevant.

Something for the automated theorem provers, perhaps.

Posted at August 3, 2021 3:07 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3341

19 Comments & 0 Trackbacks

Re: The Two Cultures Challenge Revisited

Maybe we can categorify the argument by replacing the inequality |X×Y|+|Y×X||X×X|+|Y×Y||X\times Y|+|Y\times X|\leq|X\times X|+|Y\times Y| by the set of injections Inj(X×Y+Y×X,X×X+Y×Y)Inj(X\times Y + Y\times X,X\times X + Y\times Y)?

The overall form of the “proof” would be a map (what kind?)

$In

Posted by: Spencer Breiner on August 4, 2021 2:13 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Blarg! Posting error. As I was saying…

Replace

|X×Y|+|Y×X||X×X|+|Y×Y||X\times Y|+|Y\times X|\leq |X\times X|+|Y\times Y|

with

Inj(X×Y+Y×XX×X+Y×Y)Inj(X\times Y + Y\times X\rightarrowtail X\times X+Y\times Y)?

The “proof” would then take the form of a function (functor?)

Inj(XY)+Iso(X,Y)Inj(YX)Inj(X×Y+Y×XX×X+Y×Y)Inj(X\rightarrowtail Y) \underset{Iso(X,Y)}{+} Inj(Y\rightarrowtail X) \longrightarrow Inj(X\times Y + Y\times X\rightarrowtail X\times X+Y\times Y)

The set on the left is always inhabited, so the dependence on the left-hand side gets washed out propositionally. The nice thing about this, I think, is that it should generalize straightaway to the slice category Sets/Z\mathbf{Sets}/Z, and the choice of inhabitant on the left gives you the fibre-dependency that Tao mentions in his comment.

Posted by: Spencer Breiner on August 4, 2021 2:25 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Thanks, Spencer. Could this strategy be made to work with Robin Houston’s idea?

Posted by: David Corfield on August 4, 2021 6:25 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

I’m glad you’ve brought this back up, David, because I find Terry’s challenge highly thought-provoking. It shows up our ignorance deliciously.

For all that we know about the categorification of identities (with the theory of species etc.), we seem to know almost nothing about the categorification of inequalities.

One of the thoughts that Terry’s challenge provokes in me is “what exactly are we trying to do?” Let’s take something even simpler and more basic than Cauchy–Schwarz, the mother of all inequalities:

x 20. x^2 \geq 0.

How could one categorify it? Well, if we interpret “X 20X^2 \geq 0” as “there exists an injection from the empty set to the cartesian square of any set XX” then it’s obviously true, but so too is X0X \geq 0. So that makes it clear (if it wasn’t already) that sets are “nonnegative objects” and shouldn’t be treated as analogues of arbitrary real numbers.

And that makes us think about formal differences XYX - Y of sets (whatever that means), and then the inequality (XY) 20(X - Y)^2 \geq 0 rearranges to

X×X+Y×YX×Y+Y×X, X \times X + Y \times Y \geq X \times Y + Y \times X,

which is one of the ones you listed in your post, David.

Now there are no natural transformations

X×X+Y×YX×Y+Y×X X \times X + Y \times Y \leftrightarrows X \times Y + Y \times X

(I mean, natural in X,YSetX, Y \in Set) in either direction, except for four non-injective ones from right to left. (They all send (x,y)(x, y) to either (x,x)(x, x) or (y,y)(y, y), and similarly (y,x)(y, x).) And if there are no natural transformations, what possible help could category theory be?

There is a possibility, though. Time spent playing the game of converting identities in rings into identities in semirings (or rig categories) taught me that often a “thickening” occurs. The most famous case is the implication

t=t 2+1t 6=1, t = t^2 + 1 \implies t^6 = 1,

which holds in any ring. But in a semiring, the closest we can get is

t=t 2+1t 7=t t = t^2 + 1 \implies t^7 = t

(Andreas Blass’s Seven trees in one). The conclusion has been “thickened” by a factor of tt. So who knows, maybe there’s some injective natural transformation like

6XY+(X 3+Y 3)2XY6XY+(X 3+Y 3)(X 2+Y 2) 6X Y + (X^3 + Y^3)2 X Y \to 6X Y + (X^3 + Y^3)(X^2 + Y^2)

(where the thickening is just something random I made up). If there is, would it be helpful, though?

Posted by: Tom Leinster on August 4, 2021 10:46 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Thanks, Tom. I remember “thickening” came up in Todd’s comment to your ‘A Visual Telling of Joyal’s Proof Of Cayley’s Formula’ post.

Further back in time, John Baez and James Dolan were telling us about two ways to categorify substraction and the integers: (i) their and Joyal’s way via the sphere spectrum (“to properly categorify subtraction, we need to categorify not just once but infinitely many times!”), and (ii) Schanuel’s way via (0,1)(0,1) as 1-1.

The latter is in

  • Negative sets have Euler characteristic and dimension, Lec-ture Notes in Mathematics 1488, Springer Verlag, Berlin, 1991, pp.379-385,

and shows that the Burnside rig of bounded polyhedra is [X]/(X2X+1)\mathbb{N}[X]/(X \sim 2X +1).

Have these lines of enquiry gone anywhere since?

Posted by: David Corfield on August 5, 2021 9:22 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Schanuel’s paper is often cited (and deservedly so), but my impression is that it’s more often for the general points made than the specifics. I don’t know of work that develops his specific categories and rigs of polyhedra. Though I may, of course, just not know of it, and I’d be happy to be proved wrong.

Posted by: Tom Leinster on August 5, 2021 10:54 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

I have intermittently wondered if the “right way” to get negative numbers and subtraction out of decategorifying something is to start with Joyal’s category of combinatorial games. There, the surreal numbers arise as equivalence classes of game positions, when positions that lead to what Knuth called “pseudo-numbers” are excluded; the real numbers can in turn be obtained by imposing conditions that eliminate infinite and infinitesimal numbers. The nice thing is that negative integers arise just as easily as positive dyadic rationals do.

Posted by: Blake Stacey on August 9, 2021 11:48 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

There’s a related game-rational tangle connection, as discussed in this thesis.

I remember wondering here whether there might be a coalgebraic notion of real tangle.

Posted by: David Corfield on August 10, 2021 8:16 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Digging back through the Café archives, I see we had Mike’s post Combinatorial-Game Categories, and, yet further back, John discussing ‘Holodeck games’ here.

Posted by: David Corfield on August 10, 2021 8:52 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Regarding the following…

If f:XYf: X \to Y is a function between finite sets, then |X× fX||X| 2/|Y|\left| X \times_{f} X \right| \geq \left| X \right|^{2} / \left| Y \right|.

…perhaps it may be helpful to try to write down in a reasonably direct way any monomorphism X 2Y×(X× fX)X^{2} \rightarrow Y \times \left( X \times_{f} X \right), whether or not it is immediately category theoretic. To this end, I wonder if the following works.

As a preliminary step, for any pair (y,y)Y×Y(y, y') \in Y \times Y such that |f 1(y)||f 1(y)|\left| f^{-1}(y) \right| \leq \left| f^{-1}(y') \right|, choose any monomorphism f 1(y)f 1(y)f^{-1}(y) \rightarrow f^{-1}(y'), and denote it by i y,yi_{y,y'}.

Take (x 1,x 2)X 2(x_1, x_2) \in X^{2}. Suppose that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right|. In this case, send (x 1,x 2)(x_1, x_2) to (f(x 1),(i f(x 1),f(x 2)(x 1),x 2))\left( f(x_1), \left( i_{f(x_1), f(x_2)}(x_1), x_2 \right) \right). Otherwise, namely if |f 1(f(x 1))||f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \geq \left| f^{-1} \left( f(x_2) \right) \right|, send (x 1,x 2)(x_1, x_2) to (f(x 1),(x 1,i f(x 2),f(x 1)(x 2)))\left( f(x_1), \left( x_1, i_{f(x_2), f(x_1)}(x_2) \right) \right).

I think that this defines a monomorphism. To see this, take (x 1,x 2)(x_1, x_2) and (x 1,x 2)(x_1', x_2') in X 2X^{2} which map to the same thing in Y×(X× fX)Y \times \left( X \times_{f} X \right). Observe first that it is impossible that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right| but that |f 1(f(x 1))||f 1(f(x 2))|\left| f^{-1} \left( f(x_1') \right) \right| \geq \left| f^{-1} \left( f(x_2') \right) \right|. Indeed, we would then have that f(x 1)=f(x 1)f(x_1) = f(x_1'), and also that i f(x 1),f(x 2)(x 1)=x 1i_{f(x_1), f(x_2)}(x_1) = x_1'. But i f(x 1),f(x 2)(x 1)i_{f(x_1), f(x_2)}(x_1) is in f 1(f(x 2))f^{-1}\left(f(x_2) \right) whereas x 1x_1' is in f 1(f(x 1))=f 1(f(x 1))f^{-1}\left( f(x_1') \right) = f^{-1}\left( f(x_1) \right), so we would then have that f(x 2)=f(x 1)f(x_2) = f(x_1), which contradicts our assumption that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right|.

An entirely analogous argument demonstrates that it is impossible that |f 1(f(x 1))||f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \geq \left| f^{-1} \left( f(x_2) \right) \right| but that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1') \right) \right| \lt \left| f^{-1} \left( f(x_2') \right) \right|. Indeed, we would then have that f(x 1)=f(x 1)f(x_1) = f(x_1'), and also that i f(x 1),f(x 2)(x 1)=x 1i_{f(x_1'), f(x_2')}(x_1') = x_1, from which, as above, we would be able to deduce that f(x 2)=f(x 1)f(x_2') = f(x_1'), contradicting our assumption that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1') \right) \right| \lt \left| f^{-1} \left( f(x_2') \right) \right|.

Suppose now that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right| and that |f 1(f(x 1))|<|f 1(f(x 2))|\left| f^{-1} \left( f(x_1') \right) \right| \lt \left| f^{-1} \left( f(x_2') \right)\right|. Then x 2=x 2x_2 = x_2', and moreover f(x 1)=f(x 1)f(x_1) = f(x_1') and i f(x 1),f(x 2)(x 1)=i f(x 1),f(x 2)(x 1)i_{f(x_1), f(x_2)}(x_1) = i_{f(x_1'), f(x_2')}(x_1'). Putting all of these facts together, we obtain that i f(x 1),f(x 2)(x 1)=i f(x 1),f(x 2)(x 1)i_{f(x_1), f(x_2)}(x_1) = i_{f(x_1), f(x_2)}(x_1'), which, since i f(x 1),f(x 2)i_{f(x_1), f(x_2)} is a monomorphism, implies that x 1=x 1x_1 = x_1'. Hence (x 1,x 2)=(x 1,x 2)(x_1, x_2) = (x_1', x_2'), as required.

An entirely analogous argument demonstrates that (x 1,x 2)=(x 1,x 2)(x_1, x_2) = (x_1', x_2') also holds if |f 1(f(x 1))|>|f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| \gt \left| f^{-1} \left( f(x_2) \right) \right| and |f 1(f(x 1))|>|f 1(f(x 2))|\left| f^{-1} \left( f(x_1') \right) \right| \gt \left| f^{-1} \left( f(x_2') \right) \right|.

Finally, if |f 1(f(x 1))|=|f 1(f(x 2))|\left| f^{-1} \left( f(x_1) \right) \right| = \left| f^{-1} \left( f(x_2) \right) \right| and |f 1(f(x 1))|=|f 1(f(x 2))|\left| f^{-1} \left( f(x_1') \right) \right| = \left| f^{-1} \left( f(x_2') \right) \right|, then it is immediate that (x 1,x 2)=(x 1,x 2)(x_1, x_2) = (x_1', x_2'), as required.

How ‘category theoretic’ is this monomorphism? Actually I think it is constructible category theoretically. We have (purely category theoretically) that X 2X^{2} is isomorphic to yY yYf 1(y)×f 1(y)\bigsqcup_{y \in Y} \bigsqcup_{y' \in Y} f^{-1}(y) \times f^{-1}(y'). Thus it suffices to construct a map f 1(y)×f 1(y)Y×(X× fX)f^{-1}(y) \times f^{-1}(y') \rightarrow Y \times \left( X \times_{f} X \right) for every (y,y)Y 2(y,y') \in Y^{2}. To do this in the way I did above, the only thing one really needs is that one of |f 1(y)|<|f 1(y)|\left| f^{-1}(y) \right| \lt \left| f^{-1}(y') \right|, |f 1(y)|>|f 1(y)|\left| f^{-1}(y) \right| \gt \left| f^{-1}(y') \right|, or |f 1(y)|=|f 1(y)|\left| f^{-1}(y) \right| = \left| f^{-1}(y') \right| must hold. If one defines all of the ingredients in the last sentence in a category theoretic way (e.g. defining a finite set to be one isomorphic to n1\bigsqcup_{n} 1 for some nn \in \mathbb{N}, where 11 is a one element set), this will reduce to the fact that, for any pair of natural numbers nn and nn', one of nnn \leq n', nnn \geq n', or n=nn = n' must hold, which will be perfectly true when working category theoretically as well. Once one has this, everything else in my definition of the map is straightforwardly expressible ‘category theoretically’ (in terms of arrows between sets), as is the proof that we have a monomorphism.

I think it would be naïve to imagine that one can construct a monomorphism by only some immediate application of some ‘doctrinal’ properties of the category of sets. The formulation of the problem only really makes sense because of the fact that one can express a finite set as a coproduct of 11’s, so I think one has to expect a non-trivial result to dig down to that level. This does not preclude of course that it might be possible to formulate some useful greater level of generality in which one can carry out the same kind of argument.

This is all off the cuff, so I hope I have not made some egregious error(s); apologies in advance if so! I have not thought about how this argument relates to usual proofs of the Cauchy-Schwartz inequality, I just came up with it directly.

Posted by: Richard Williamson on August 5, 2021 12:38 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Just reading through again, the following…

Finally, if |f 1(f(x 1))|=|f 1(f(x 2))|\left| f^{-1}\left( f(x_1) \right) \right|=\left| f^{-1}\left(f(x_2)\right) \right| and |f 1(f(x 1))|=|f 1(f(x 2))|\left| f^{-1}\left(f(x_1')\right) \right|=\left| f^{-1}\left(f(x_2') \right) \right|, then it is immediate that (x 1,x 2)=(x 1,x 2)(x_1,x_2)=(x_1',x_2'), as required.

…needs more care (I tweaked something at some point, and forgot to address this paragraph). Maybe one can adjust the definition of the monomorphism to get it to work somehow, but I’m out of time for the moment! Perhaps the idea of the construction will spark some thoughts for someone anyhow.

Posted by: Richard Williamson on August 5, 2021 1:39 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

The codomain of the desired map can be rewritten as yY yYf 1(y)×f 1(y) \bigsqcup_{y\in Y}\bigsqcup_{y'\in Y} f^{-1}(y)\times f^{-1}(y) so one can seek a permutation σ\sigma of Y 2Y^2 and a family of injections f 1(y)×f 1(y)f 1(pr 1(σ(y,y))) 2f^{-1}(y)\times f^{-1}(y') \hookrightarrow f^{-1}(pr_1(\sigma(y,y')))^2 with disjoint image.

This is more like seeking an monomorphism in the arrow category from f 2:X 2Y 2f^2\colon X^2 \to Y^2 to id×(fpr 1):Y×X× YXY 2id\times (f\circ pr_1)\colon Y\times X\times_Y X \to Y^2. Moreover, I feel like the fact YY admits a total order, and given two total orders they are uniquely isomorphic as ordered sets, should be important here. Given any monomorphism of the sort we seek, one can permute Y 2Y^2 and get another one. So why not choose an auxiliary total order on YY, treat it as {1,,N}\{1,\ldots,N\}, and the mere existence of the monomorphism doesn’t depend on this choice.

In this case, one could also alter the chosen ordering on YY so that there is a chain of injections f 1(1)f 1(2)f 1(N)f^{-1}(1) \hookrightarrow f^{-1}(2) \hookrightarrow \cdots \hookrightarrow f^{-1}(N). Hence one could interpret ff as arising from the Grothendieck construction on a functor from the thin category arising from YY with the ordering to finite sets and injections. I’m not sure this helps at all, but it at least gives the data in a form that’s amenable to categorical construction.

Posted by: David Roberts on August 5, 2021 9:10 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

The argument by Robin gives a wonderful categorical proof that (X×X)(Y×Y)(X \times X) \sqcup (Y \times Y) is at least as large as (X×Y)(Y×X)(X \times Y) \sqcup (Y \times X) in the category of sets.

Terry Tao then showed how to deduce from this the relative version, that (X× YX)(Z× YZ)(X \times_Y X) \sqcup (Z \times_Y Z) is at least as large as (X× YZ)(Z× YX)(X \times_Y Z) \sqcup (Z \times_Y X). The idea is to apply Robin’s proof in each fiber associated to an element yYy \in Y. One of the problems is then to turn Terry Tao’s argument into a categorical proof.

I would say that his argument is already categorical to a large degree. Below is a rephrasing of the same argument to make it look a bit more categorical.

In a Grothendieck topos \mathcal{E} we could define the size |X||X| of an object XX in the topos as the disjoint union of the fibers p *(E)p^*(E), where pp goes over the isomorphism classes of points of the topos. For example, in the category of sets (or GG-sets for GG a group), the size is just the underlying set. If you take a sheaf on a sober topological space XX, then the size of the sheaf is the underlying set of YY, where YXY \to X is the local homeomorphism (étale space) associated to the sheaf. The functor |.||.| that sends an object XX to its size |X||X| preserves colimits and pullbacks (but not necessarily binary products or the terminal object).

Because the functor p *p^* preserves disjoint unions and products and |.||.| preserves coproducts, the equality |X×X|+|Y×Y||X×Y|+|Y×X||X \times X| + |Y \times Y| \geq |X \times Y| + |Y \times X| then holds in any topos. If you apply this to the slice topos over YY, then you get the equality |X× YX|+|Z× YZ||X× YZ|+|Z× YX||X \times_Y X| + |Z \times_Y Z| \geq |X \times_Y Z| + |Z \times_Y X|. Here we say ABA \geq B if the cardinality of AA is greater than or equal to the cardinality of BB.

For the original problem, you can use that |.||.| preserves pullbacks, and then you get |X× YX|=|X|× |Y||X||X \times_Y X| = |X| \times_{|Y|} |X| which is bigger than |X| 2/|Y||X|^2/|Y| using the result for sets.

Posted by: Jens Hemelaer on August 5, 2021 12:43 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

There is a mistake in my comment above: it’s not necessary true that the size of XYX \to Y in the slice topos /Y\mathcal{E}/Y is the same as the size of XX in \mathcal{E}. The problem is that the points of the slice topos /Y\mathcal{E}/Y corresponding to the pairs (p,y)(p,y) and (p,y)(p,y') can be isomorphic, for different elements of y,yp *(Y)y,y' \in p^*(Y), and then they get counted only once, while they should be counted both times.

To resolve this problem, you can use the alternative definition of ‘size’ as follows. For a topos \mathcal{E} you fix a family of points SS of \mathcal{E} and then define the size of XX as the disjoint union of the fibers p *(X)p^\ast(X), for pSp \in S. Then for the slice topos /Y\mathcal{E}/Y the corresponding family S YS_Y should consist of the family of points of the form (p,y)(p,y) for all pSp \in S and all yp *(Y)y \in p^*(Y).

With this modified definition, the functor |.||.| still preserves colimits and pullbacks, so the rest of the argument still goes through.

Posted by: Jens Hemelaer on August 5, 2021 2:03 PM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Even for the simpler version, and taking XX to be a finite set of cardinality n3n \ge 3 and Y=1Y = 1, there’s no equivariant embedding X+XX×X+1X + X \hookrightarrow X \times X + 1.

To see this, we can work in HoTT: Consider first equivariant maps XX×X+1X \to X \times X + 1. These are elements of the type

(1) X:BS n(XX×X+1) A:BS n1((A+1)×(A+1)+1) A:BS n1((A×A+A+A+1+1) \prod_{X : BS_n}(X \to X \times X + 1) \simeq \prod_{A : BS_{n-1}}((A+1)\times(A+1)+1) \simeq \prod_{A : BS_{n-1}}((A\times A +A+A+1+1)

(Here I take as a classifying type for the symmetric group, BS nBS_n, the type of nn-element sets.)

Since BS n1BS_{n-1} is connected, any element on the right must factor through one of the 5 coproduct inclusions. But since n12n-1\ge2, there are no elements in the type A:BS n1A\prod_{A:BS_{n-1}}A (no fixed point of an (n1)(n-1)-element set under permutation), so the only choices are the constant map to the final unit type, or the constant map to the penultimate one, and the latter corresponds to the diagonal map X:BS n(XX×X)\prod_{X:BS_n}(X \to X\times X).

So if we have an embedding, it must be the diagonal. But that means there’s no element of the type

(2) X:BS n(X+XX×X+1), \prod_{X:BS_n}(X + X \hookrightarrow X \times X + 1),

since both compositions with the coproduct inclusions XX+XX \hookrightarrow X + X must be the diagonal.

Posted by: Ulrik Buchholtz on August 6, 2021 10:10 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

I should add that it was Egbert Rijke’s idea to look at this special case (XX finite, Y=1Y=1). He also calculated that if n=2n=2, then the type in (2) above has cardinality 88.

Also, in case it wasn’t clear, in the first equivalence in (1) above, we use the equivalence X:BS nXBS n1\sum_{X:BS_n}X \simeq BS_{n-1} that comes from the fact that to give an nn-element set with a point is the same as giving the (n1)(n-1)-element complement.

Posted by: Ulrik Buchholtz on August 6, 2021 11:25 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

Thanks, Ulrik!

So where does that leave us? Any prospect of Tom’s thickening, or should we take the hint that something more radical is needed?

If the type theorists are to help out, I see there’s a notion of a negative type

  • Roshan P. James, Amr Sabr, The Two Dualities of Computation:Negative and Fractional Types, pdf,

where negation corresponds to the reversal of time. There’s even a discussion of the isomorphism between seven binary trees and one that Tom mentioned.

Posted by: David Corfield on August 6, 2021 11:25 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

A recent paper on this theme:

  • Chao-Hong Chen, Amr Sabry, A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative andFractional Types, (pdf)
Posted by: David Corfield on August 6, 2021 11:41 AM | Permalink | Reply to this

Re: The Two Cultures Challenge Revisited

So where does that leave us? Any prospect of Tom’s thickening, or should we take the hint that something more radical is needed?

Ah, so Tom remarked as well that there are no equivariant embeddings.

But yes, thickening works: For instance, we can thicken with the type of cyclic orders on XX, C(X)C(X). (That gives an equivalence X:BS nC(X)BC n\sum_{X:BS_n}C(X) \simeq BC_n.)

For n2n\ge 2, we can give an element of the type

(1) X:BS n(X+X)×C(X)X×X×C(X) \prod_{X:BS_n} (X+X)\times C(X) \hookrightarrow X\times X \times C(X)

as follows. We can map a left summand xx to the diagonal (x,x)(x,x) and a right summand xx to (x,next(x))(x,next(x)), preserving the element of C(X)C(X). Here, next:XXnext: X\to X comes from the cyclic order.

More trivially, we can thicken with a trivialization of XX, i.e., an equivalence X{0,1,,n1}X \simeq \{0,1,\ldots,n-1\}.

I don’t know whether it’s possible to do it by thickening with a polynomial.

Posted by: Ulrik Buchholtz on August 6, 2021 11:55 AM | Permalink | Reply to this

Post a New Comment