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

Topic: Piecewise-linear subspaces diagrammatically?

Guillaume Boisseau (May 27 2021 at 11:14):

We've been having a cool conversation on twitter (https://twitter.com/guillaume_bso/status/1397524819252584457) with @Cole Comfort @Jules Hedges and @Robin Piedeleu, let's continue here!

@cole_comfort @rwolffoot @mattecapu An interesting fact is that we can make transistors out of diodes and the aforementioned measurement-controlled sources, which are a linear element: http://ecee.colorado.edu/~bart/ecen3320/newbook/chapter5/ch5_3.htm#5_3_3 So adding diodes seems enough to get all of electronics

- Guillaume Boisseau (@guillaume_bso)

Guillaume Boisseau (May 27 2021 at 11:15):

We're asking what happens if we add a gadget to GAA that allows us to model diodes. So far it appears this is equivalent to extending the theory of polyhedra (https://arxiv.org/abs/2105.10946) with a gadget that gives the union of x=0 and y=0

Guillaume Boisseau (May 27 2021 at 11:17):

We conjecture this gives us something like piecewise-linear subspaces. So far I've convinced myself that we can build arbitrary R->R piecewise linear functions (https://twitter.com/guillaume_bso/status/1397661569937518593) and the boundary of any polyhedron (https://twitter.com/guillaume_bso/status/1397704652087496709)

@rwolffoot @_julesh_ @cole_comfort @mattecapu Got it! From that I think we can build many piecewise linear stuff if we have the affine fragment. Not sire what we can do without it https://twitter.com/guillaume_bso/status/1397661569937518593/photo/1

- Guillaume Boisseau (@guillaume_bso)

@rwolffoot @_julesh_ @cole_comfort @mattecapu Hahaha yeeee I can do it! We need to replace all the ≥s at the same time. Behold (the sideways triangle denotes ≥) https://twitter.com/guillaume_bso/status/1397704652087496709/photo/1

- Guillaume Boisseau (@guillaume_bso)

Guillaume Boisseau (May 27 2021 at 11:18):

@Robin Piedeleu has a conjecture for how to model those subspaces https://twitter.com/rwolffoot/status/1397870805275582466

Cole Comfort (May 27 2021 at 11:18):

Robin's twitter is private btw

Guillaume Boisseau (May 27 2021 at 11:19):

oh right I forgot

Guillaume Boisseau (May 27 2021 at 11:19):

well, his idea is based on this https://www.emis.de/journals/BAG/vol.43/no.1/b43h1ovc.pdf

Guillaume Boisseau (May 27 2021 at 11:28):

I've found some resources on piecewise linear manifolds but it's all a mess of topology and simplical complexes

Robin Piedeleu (May 27 2021 at 11:36):

Cole Comfort said:

Robin's twitter is private btw

I've opened it now if that makes it easier for everyone to follow what we wrote.

Robin Piedeleu (May 27 2021 at 11:37):

(I may close it again in a while)

Robin Piedeleu (May 27 2021 at 11:42):

Beyond arbitrary PL functions $\mathbb R\rightarrow \mathbb R$, would we also need to express max/min: $\mathbb{R}^2\rightarrow \mathbb R$, with a view to exploit the representation of PL functions given above?

Robin Piedeleu (May 27 2021 at 11:44):

They certainly both look like PL relations, at least intuitively (as long as we have not pinned down the precise meaning of PL relation).

Robin Piedeleu (May 27 2021 at 11:45):

But then, I'm a bit worried about finding a rewriting procedure to normal form for completeness, because I remember things getting quickly undecidable with + and max together.

Guillaume Boisseau (May 27 2021 at 11:46):

I think it's even worse: piecewise linear subspace means essentially the triangulation of an arbitrary manifold, right?

Guillaume Boisseau (May 27 2021 at 11:47):

We can get things with holes

Guillaume Boisseau (May 27 2021 at 11:47):

Which feels a lot stronger than min/max and a lot less normalizable

Cole Comfort (May 27 2021 at 11:49):

Robin Piedeleu said:

They certainly both look like PL relations, at least intuitively (as long as we have not pinned down the precise meaning of PL relation).

There is a definition of piecewise linear functions, and there is an obvious way to compose them. Then there is a category, so I guess we can check if this category is regular and then maybe this will be the right notion of piecewise linear relations? Linear relations arise in this way, and affine relations are just the full subcategory of nonempty such things...

Guillaume Boisseau (May 27 2021 at 11:51):

Oh, cool!

Guillaume Boisseau (May 27 2021 at 11:51):

I'm not following that last bit: affine relations can be empty

Cole Comfort (May 27 2021 at 11:52):

If you consider an affine subspace as possibly being empty, then affine relations can be characterized in terms of the full subcategory of relations of finite dimensional affine vector spaces where the objects are nonempty.

Guillaume Boisseau (May 27 2021 at 11:52):

I see

Cole Comfort (May 27 2021 at 11:52):

Because essentially you are trying to take relations of affine matrices, but this doesn't exist because you can get the zero scalar which stops you from taking pullbacks. But if you allow affine spaces to be empty, zero can live as a subobject

Guillaume Boisseau (May 27 2021 at 11:54):

do you have an analogue thing for cones and polyhedra?

Guillaume Boisseau (May 27 2021 at 11:56):

to be more precise: cones arise when we add the comparison gadget to GLA. We get "conic relations" which are convex subspaces of R^n closed under positive addition

Cole Comfort (May 27 2021 at 11:56):

I have to think about this a bit more. But I think most of these relational calculi are just projections of categories of relations (which are multisorted props), down to props by considering a full subcategory thereof.

Guillaume Boisseau (May 27 2021 at 11:57):

Is there a good notion of conic function that would give that?

Guillaume Boisseau (May 27 2021 at 11:57):

why multisorted?

Cole Comfort (May 27 2021 at 11:58):

Like in the case of affine relations, it is multisorted, because there are empty objects as well as free ones. So you have forget the empty ones at the level of objects by taking a full subcategory.

Robin Piedeleu (May 27 2021 at 11:58):

For additive relations, there is a section of my thesis that shows it's a subcategory of a category of relations.

Robin Piedeleu (May 27 2021 at 11:58):

There must be a way of showing the same for conic relations.

Cole Comfort (May 27 2021 at 11:58):

Yes, I think it is a recurring theme

Guillaume Boisseau (May 27 2021 at 11:59):

well, it's a subcategory of Rel. I assume you mean something stronger?

Cole Comfort (May 27 2021 at 11:59):

Something like a full subcategory of relations of additive (affine) monoids where the objects are freely generated?

Robin Piedeleu (May 27 2021 at 11:59):

Sorry, yes. I mean a subcategory of the category of relations (obtained via the standard construction) for the structured functions you started with.

Robin Piedeleu (May 27 2021 at 12:01):

For additive relations, the starting point is some subcategory of the category of commutative monoid homomorphisms.

Guillaume Boisseau (May 27 2021 at 12:01):

hm interesting, so maybe cone homomorphisms?

Cole Comfort (May 27 2021 at 12:02):

My hope is that thinking of things this way will allow one to give a modular presentation of such categories. If certain conditions hold then there is such a modular presentation; however, it isn't always going to be nice enough to care about.

Cole Comfort (May 27 2021 at 12:04):

Guillaume Boisseau said:

hm interesting, so maybe cone homomorphisms?

If I recall correctly, in both the affine and the additive cases, the props of relations arise as a full subcategory of some larger category of relations, so I think it would be something similar

Guillaume Boisseau (May 27 2021 at 12:05):

well, if that gives us something useful would be cool. But I personally would be fine with a crudely hand-constructed category too

Robin Piedeleu (May 27 2021 at 12:06):

Nothing wrong with an old-fashioned hand-crafted category! :)

Cole Comfort (May 27 2021 at 12:07):

I think it would be nice to know merely because then we will know what we are actually working with. In the case of affine relations, we are really working with an extra object which we just can't access directly, and this manifests itself in terms of the zero scalar. Maybe in more exotic cases this would reveal something enlightening

Robin Piedeleu (May 27 2021 at 12:07):

Cole Comfort said:

If I recall correctly, in both the affine and the additive cases, the props of relations arise as a full subcategory of some larger category of relations, so I think it would be something similar

Yes, you're right, I think it was indeed a full subcategory for the additive case.

Robin Piedeleu (May 27 2021 at 12:13):

Coming back to my initial worry about how expressive these things are, it would also mean that we can represent the ReLU function $\lambda x. max(0,x)$, commonly used in machine learning as an activation function for neural networks. Does this mean we can approximate arbitrary continuous functions by just throwing in this diode-like element?

Robin Piedeleu (May 27 2021 at 12:14):

I guess piecewise linear means we can have as many linear pieces as we want...It's a bit scary but does not necessarily preclude a normal form argument.

Cole Comfort (May 27 2021 at 12:15):

Robin Piedeleu said:

Coming back to my initial worry about how expressive these things are, it would also mean that we can represent the ReLU function $\lambda x. max(0,x)$, commonly used in machine learning as an activation function for neural networks. Does this mean we can approximate arbitrary functions by just throwing in this diode-like element?

As in, do you just get all of relations instead of some extension of linear relations

Guillaume Boisseau (May 27 2021 at 12:16):

Pretty sure we can get a triangulation of an arbitrary manifold, which includes approximating any function

Guillaume Boisseau (May 27 2021 at 12:17):

Also we can express transistors so arbitrary logical circuits

Robin Piedeleu (May 27 2021 at 12:17):

I was not even talking about relations, just continuous functions.

Cole Comfort (May 27 2021 at 12:18):

Which would imply the case of relations, I guess

Guillaume Boisseau (May 27 2021 at 12:18):

also just continuous functions yeah

Guillaume Boisseau (May 27 2021 at 12:18):

we can definitely approximate any continuous R->R function since we have all piecewise linear R->R fns

Guillaume Boisseau (May 27 2021 at 12:21):

as in, I know how to draw an explicit diagram for an arbitrary piecewise linear R->R fn

Guillaume Boisseau (May 27 2021 at 12:40):

also I showed how to get the absolute value function. From that we can get max(x,y)=(abs(x-y)+x+y)/2

Chad Nester (May 27 2021 at 12:49):

what's a piecewise-linear subspace?

Guillaume Boisseau (May 27 2021 at 12:49):

that's one of the things we're trying to figure out ^^

Guillaume Boisseau (May 27 2021 at 12:51):

we want to generalize piecewise-linear functions to relations, and the result is probably piecewise-linear submanifolds of R^n

Guillaume Boisseau (May 27 2021 at 12:54):

what those looks like is manifolds made from straight lines/polyhedra

Guillaume Boisseau (May 27 2021 at 12:54):

probably

Reid Barton (May 27 2021 at 12:58):

Do you actually want to restrict to manifolds? What about the following subset of the plane: three line segments with a common endpoint, like the letter Y.

Guillaume Boisseau (May 27 2021 at 12:59):

is that not a manifold? cause you're right, I want that too

Guillaume Boisseau (May 27 2021 at 13:00):

(I know very little about manifolds)

Joe Moeller (May 27 2021 at 13:00):

no, the joining point is not locally Euclidean.

Joe Moeller (May 27 2021 at 13:00):

You may want "stratified spaces"

Reid Barton (May 27 2021 at 13:01):

Manifold means it should locally look like R^d (where d is the dimension of the manifold).

Reid Barton (May 27 2021 at 13:05):

And I'm guessing you are only interested in closed subsets (because the graph of a function is closed exactly when the function is continuous)?

Guillaume Boisseau (May 27 2021 at 13:07):

yep

Joe Moeller (May 27 2021 at 13:09):

To give more of a sense of what manifolds are like you can list all of them in dimensions 0, 1, and 2:
0: any discrete space, countably infinite at most
1: R, a circle, countable disjoint unions of those
2: R^2, sphere, torus, 2-hole torus, ..., n-hole torus, Klein bottle, projective plane, connected sums of those, countable disjoint unions of those

Did I get everything? Is there some redundancy in listing Klein bottle, projective plane, and connected sums?

Guillaume Boisseau (May 27 2021 at 13:11):

also btw we want finitely-generated things, which should be easier than the general notion

Reid Barton (May 27 2021 at 13:14):

So it sounds like you want to consider semilinear (= can be described by a formula of first-order logic involving $+$, scalar multiplication, constants, and $<$) sets that are closed, which I think are the same thing as finite unions of what you call polyhedra (but beware that term has various slightly different meanings in related contexts).

Guillaume Boisseau (May 27 2021 at 13:14):

yeah, we might just want "a union of some polyhedra that fit together in a nice way"

Reid Barton (May 27 2021 at 13:15):

At least, when a closed semilinear set is bounded then I know it's a finite union of closed simplices; I'm less used to thinking about the unbounded case.

Guillaume Boisseau (May 27 2021 at 13:17):

if you want to think in terms of formulas it's easier: the actual problem we have is what we get if we add a certain gadget to the graphical language of Graphical Affine Algebra. In terms of equations we have constants,+,multiplication by a constant,existential quantification,>= and the gadget which offers a limited form of alternation, namely "x=0 or y=0"

Reid Barton (May 27 2021 at 13:18):

There actually aren't any non-nice ways for polyhedra to fit together, which is not obvious. For example if you take the union of the underlying sets of two simplicial complexes in R^n, then it is also the underlying set of a simplicial complex in R^n, but you might need to add more vertices and subdivide some of the original simplices, if they overlap awkwardly.

Guillaume Boisseau (May 27 2021 at 13:18):

hm, that makes intuitive sense

Guillaume Boisseau (May 27 2021 at 13:19):

nice!

Guillaume Boisseau (May 27 2021 at 13:19):

our setting does seem to force connectedness though

Reid Barton (May 27 2021 at 13:19):

Right, it is intuitive but not so easy to prove, and it would definitely not be true for the union of two submanifolds of R^n, say (because they could be wiggly near their intersection).

Guillaume Boisseau (May 27 2021 at 13:23):

That's really cool, because "finite union of polyhedra" sounds like a simple enough notion

Reid Barton (May 27 2021 at 13:57):

So let me see if I understand the problem. We have a bunch of basic relations on various $R^{n_i}$, which you listed above. First, we want to understand all the relations that can be built from them by composition (which I guess correspond to the formulas that can be built from them using regular logic). Then we want to give a generators-and-relations presentation of the resulting category of relations. Is that a reasonable summary?

Reid Barton (May 27 2021 at 14:01):

Can you build "x = 0 or y = 0 or z = 0"?

Reid Barton (May 27 2021 at 14:01):

If so I think you can build any finite union of polyhedra, because for a polyhedron $P$ you can build a function which is zero precisely on $P$.

Guillaume Boisseau (May 27 2021 at 14:05):

Reid Barton said:

So let me see if I understand the problem. We have a bunch of basic relations on various $R^{n_i}$, which you listed above. First, we want to understand all the relations that can be built from them by composition (which I guess correspond to the formulas that can be built from them using regular logic). Then we want to give a generators-and-relations presentation of the resulting category of relations. Is that a reasonable summary?

Yes, exactly!

Guillaume Boisseau (May 27 2021 at 14:09):

Reid Barton said:

Can you build "x = 0 or y = 0 or z = 0"?

Yes: if R(x,y) is "x=0 or y=0", then "x = 0 or y = 0 or z = 0" iff "exists a,b, R(x,a) and R(y,b) and z=a+b"

Guillaume Boisseau (May 27 2021 at 14:19):

Reid Barton said:

If so I think you can build any finite union of polyhedra, because for a polyhedron $P$ you can build a function which is zero precisely on $P$.

Ohhh that's perfect! Indeed we can use one of the normal forms from this paper https://arxiv.org/abs/2105.10946 to get a total relation that gives a polyhedron when the output is set to zero :o

Robin Piedeleu (May 27 2021 at 14:19):

How do we depict finite unions of polyhedra in this syntax, @Guillaume Boisseau ? Is it just some white-black convolution operation (potentially guarded by some of the choice operation)?

Guillaume Boisseau (May 27 2021 at 14:24):

gimme a sec

Guillaume Boisseau (May 27 2021 at 14:24):

hm, can't send a pic from my phone

Robin Piedeleu (May 27 2021 at 14:26):

Reid Barton said:

If so I think you can build any finite union of polyhedra, because for a polyhedron $P$ you can build a function which is zero precisely on $P$.

What if their intersection is empty? Isn't one invariant of our setting that all these subsets are connected?

Guillaume Boisseau (May 27 2021 at 14:26):

turns out I was wrong about connectedness

Guillaume Boisseau (May 27 2021 at 14:27):

if I could just figure out how to send a pic ><

Guillaume Boisseau (May 27 2021 at 14:34):

IMG_20210527_153341.jpg

Guillaume Boisseau (May 27 2021 at 14:36):

as an example of non-connected thing, take for P1 and P2 the functions x-1 and x-2. The result is the set {1,2}

Robin Piedeleu (May 27 2021 at 14:36):

I see! Very cool

Robin Piedeleu (May 27 2021 at 14:38):

In the $\mathbb N$-linear (additive) case there was already a similar behaviour with the sum; affine constant diagram, that implemented a limited form of choice. This here seems to be arbitrary finite unions.

Guillaume Boisseau (May 27 2021 at 14:39):

Also this diagram looks like a potential normal form :D

Robin Piedeleu (May 27 2021 at 14:39):

Absolutely!

Guillaume Boisseau (May 27 2021 at 14:45):

I'm very excited :D

Robin Piedeleu (May 27 2021 at 14:45):

So we have to find equations that allow us to always place the choice generator in this position. Let's see:

• it does not commute with copy,
• we have choice; discard = co-zero and co-discard ; choice = zero.

Guillaume Boisseau (May 27 2021 at 14:46):

It has the inequalities of abelian bicategories

Jules Hedges (May 27 2021 at 14:46):

Damn, I wish I had enough time to keep up with this..... and that I remembered how graphical affine algebra works :D

Robin Piedeleu (May 27 2021 at 14:46):

Yes! It's the interaction with addition that is more interesting.

Guillaume Boisseau (May 27 2021 at 14:48):

It should be the colorswap of its interaction with copy

Robin Piedeleu (May 27 2021 at 14:49):

Yes, was going to write this! And it's self transpose

Guillaume Boisseau (May 27 2021 at 14:49):

Indeed

Guillaume Boisseau (May 27 2021 at 14:49):

And self-colorswap

Cole Comfort (May 27 2021 at 14:49):

It is invariant under colour swapping, so this is dual

Guillaume Boisseau (May 27 2021 at 14:50):

I can't find something that would pin it down though, so far this seems generic

Robin Piedeleu (May 27 2021 at 14:53):

co-zero ; zero $\leq$ choice $\leq$ discard ; co-discard

Robin Piedeleu (May 27 2021 at 14:54):

somehow, it's precisely between those two in some sense

Robin Piedeleu (May 27 2021 at 14:54):

but that's maybe a consequence of something else

Guillaume Boisseau (May 27 2021 at 14:54):

anything is between those two

Robin Piedeleu (May 27 2021 at 14:54):

right, i'm an idiot

Robin Piedeleu (May 27 2021 at 14:54):

:)

Guillaume Boisseau (May 27 2021 at 14:55):

so far that's all just axioms of additive relations aka abelian bicats, except the part where we plug a zero or discard into it

Guillaume Boisseau (May 27 2021 at 14:55):

ah, also if we plug a nonzero scalar into it, the scalar disappears

Cole Comfort (May 27 2021 at 14:56):

Wait, is this the same type of additive relations as in Robin's thesis?

Robin Piedeleu (May 27 2021 at 14:56):

I think Guillaume means polyhedral

Guillaume Boisseau (May 27 2021 at 14:56):

I can check if you have a link

Robin Piedeleu (May 27 2021 at 14:57):

we're assuming white Frobenius here (abelian bicat.) so this is different

Guillaume Boisseau (May 27 2021 at 14:57):

what I actually mean is frobenius theories and the colorswap of that

Cole Comfort (May 27 2021 at 14:58):

Is an abelian bicategory just an ab-encriched bicategory?

Guillaume Boisseau (May 27 2021 at 14:59):

I've been wondering that

Cole Comfort (May 27 2021 at 14:59):

Do you have a reference for this notion, because I am a bit confused

Guillaume Boisseau (May 27 2021 at 15:00):

I'm looking but got nothing, I only heard @Pawel Sobocinski use that term

Robin Piedeleu (May 27 2021 at 15:01):

I think it's at the end of Carboni and Walters original paper

Guillaume Boisseau (May 27 2021 at 15:02):

ie: https://core.ac.uk/download/pdf/82513341.pdf

Cole Comfort (May 27 2021 at 15:02):

Ah I see, I remember this, just not the name for it

Guillaume Boisseau (May 27 2021 at 15:03):

I can't follow most of that paper x) hope it answers the question

Cole Comfort (May 27 2021 at 15:04):

I thought it was something much more complicated, haha

Guillaume Boisseau (May 27 2021 at 15:06):

afk to see a friend, I hope there's still something left for me to figure out when I come back ^^

Cole Comfort (May 27 2021 at 15:07):

I need to take a few days to read this paper on polyhedral relations. Looks very exciting

Guillaume Boisseau (May 27 2021 at 15:09):

It's really cool!

Robin Piedeleu (May 27 2021 at 15:09):

Ok, I've got a property:

Robin Piedeleu (May 27 2021 at 15:10):

copy; (id $\otimes$ choice) ; co-copy = co-zero ; zero

Robin Piedeleu (May 27 2021 at 15:10):

(and the color-swap)

Robin Piedeleu (May 27 2021 at 15:10):

does that follow from something else?

Robin Piedeleu (May 27 2021 at 15:10):

(am I being stupid again?)

Guillaume Boisseau (May 27 2021 at 15:11):

Nice, not stupid

Guillaume Boisseau (May 27 2021 at 15:14):

Actually the polyhedra paper has a very interesting axiom: totality of the order is an "or" kind of thing that's hard to express diagrammatically. The axiom that does that job is the spider axiom, which is frankly unexpected

Guillaume Boisseau (May 27 2021 at 15:15):

I'm expecting we get similarly a very non-obvious axiom that captures something about this making choices

Guillaume Boisseau (May 27 2021 at 15:15):

(I plan to tweet about the spider axiom in the coming days also)

Cole Comfort (May 27 2021 at 15:16):

By spider, do you mean the frobenius law?

Cole Comfort (May 27 2021 at 15:17):

Oh I see, it is this kind of bialgebra law.

Cole Comfort (May 27 2021 at 15:19):

"a spider with four legs"

Cole Comfort (May 27 2021 at 15:22):

what did you do to that poor spider's other four legs

Guillaume Boisseau (May 27 2021 at 15:22):

It's alright, this generalizes to an arbitrary number of legs ^^

Robin Piedeleu (May 27 2021 at 15:24):

A lot of properties of orders can be nicely captured in the category of posets and monotone relations (relations $R\subseteq X\times Y$ such that $(x,y)\in R$, and $x'\leq x$, $y\leq y'$ imply $(x',y')\in R$). This is a bicategory of relations and its discrete objects (those for which copy, discard etc. are a Frobenius algebra) are those posets for which the order relation is equality. But there's much more: if the poset is a lattice, intersection is adjoint (in the 2-categorical sense) to copy. In fact you also get a dual operation and all these adjunctions:
image.png
And if the lattice is a Boolean algebra, then the white structure is a Frobenius algebra (but black is not)! So being a Boolean algebra is dual to being a set with equality in this sense.

Robin Piedeleu (May 27 2021 at 15:25):

There's a lot of interesting things that happen when moving to this category!

Guillaume Boisseau (May 27 2021 at 15:29):

Oh: choice;choice=choice

Guillaume Boisseau (May 27 2021 at 15:31):

Robin: oh, very interesting

Guillaume Boisseau (May 27 2021 at 15:33):

x=-y is not very monotone tho

Cole Comfort (May 27 2021 at 15:33):

The idempotency of choice is definitely really important. As a partial function, it is a restriction idempotent, which is of particular interest to me.

Reid Barton (May 27 2021 at 15:33):

Guillaume Boisseau said:

Actually the polyhedra paper has a very interesting axiom: totality of the order is an "or" kind of thing that's hard to express diagrammatically. The axiom that does that job is the spider axiom, which is frankly unexpected

Oh that's interesting. So I noticed at one point that if $<$ is a strict total order, then $<$ being a "nonempty dense linear order without endpoints" is equivalent to saying that for any $L_1, \ldots, L_m$ and $R_1, \ldots, R_n$ (we allow $m = 0$ and/or $n = 0$) then

$$(\exists x.\, L_1 < x \wedge \cdots \wedge L_m < x \wedge x < R_1 \wedge \cdots \wedge x < R_n) \iff (\forall i \, j.\, L_i < R_j)$$

which is typically the exact thing you need in quantifier elimination--here eliminating the quantifier $\exists x$. (Model theorists seem to prefer $<$ over $\le$ for some reason, and also tend to implicitly assume their models are nonempty.)

But in fact, maybe you're saying that we could start with even less than the assumption that $<$ is a strict total order. For example, now I see that transitivity also follows from this condition (take $m = n = 1$). But how do you prove the order is total?

Robin Piedeleu (May 27 2021 at 15:34):

Guillaume Boisseau said:

x=-y is not very monotone tho

Yes, it was just a side comment about characterising properties of orders in a diagrammatic context :)

Cole Comfort (May 27 2021 at 15:36):

One thing that I expect to hold, which I have not managed to calculate, is that it should commute with cocopying and copying. Is this an identity already?

Robin Piedeleu (May 27 2021 at 15:36):

Do you mean choice? It should not hold because it's not a function

Robin Piedeleu (May 27 2021 at 15:37):

Or, more precisely, it only holds laxely, like in any Cartesian bicategory

Cole Comfort (May 27 2021 at 15:38):

No I mean, not that it is copied, but that it commutes with the multiplication like copy; (1 x choice) = choice;copy

Cole Comfort (May 27 2021 at 15:40):

Hmmm wait, maybe I am wrong. It choice a subset of the identity?

Robin Piedeleu (May 27 2021 at 15:42):

No

Cole Comfort (May 27 2021 at 15:42):

scratch that, then

John Baez (May 27 2021 at 15:50):

Cole Comfort said:

My hope is that thinking of things this way will allow one to give a modular presentation of such categories. If certain conditions hold then there is such a modular presentation; however, it isn't always going to be nice enough to care about.

What's a "modular presentation" of a category?

Cole Comfort (May 27 2021 at 15:52):

John Baez said:

Cole Comfort said:

My hope is that thinking of things this way will allow one to give a modular presentation of such categories. If certain conditions hold then there is such a modular presentation; however, it isn't always going to be nice enough to care about.

What's a "modular presentation" of a category?

Like in terms of distributive laws of props (seen as monads in Mon-Prof) as well as pushouts when necessary

Cole Comfort (May 27 2021 at 15:52):

Like in the style of composing props of Lack

John Baez (May 27 2021 at 15:53):

Okay. "Modular" means so many things in math, from modular lattices to modular tensor categories.

Cole Comfort (May 27 2021 at 15:54):

Here is one more identity which may have already been written down.

copy;(choice $\otimes$ choice);add = choice

Cole Comfort (May 27 2021 at 15:55):

John Baez said:

Okay. "Modular" means so many things in math, from modular lattices to modular tensor categories.

Maybe I should have said "compositionally." Like in the way that linear relations can be presented in terms of a distributive law.

Cole Comfort (May 27 2021 at 16:12):

Also if you conjugate copy with choice, then this relates all the legs to each other.

Guillaume Boisseau (May 27 2021 at 17:14):

@Reid Barton ooh I'd like to understand this better. Transitivity does indeed follow. I can prove that the order is total but only by appealing to completeness of the axioms or in other words by using the normal form. I'd love to find a more direct way

Guillaume Boisseau (May 27 2021 at 17:15):

Cole Comfort said:

Here is one more identity which may have already been written down.

copy;(choice $\otimes$ choice);add = choice

that's also part of the cartesian bicategory structure

Guillaume Boisseau (May 27 2021 at 17:15):

Cole Comfort said:

Also if you conjugate copy with choice, then this relates all the legs to each other.

what do you mean by this?

Cole Comfort (May 27 2021 at 17:17):

Guillaume Boisseau said:

Cole Comfort said:

Also if you conjugate copy with choice, then this relates all the legs to each other.

what do you mean by this?

choice; copy; (choice $\otimes$ choice) = d;(d ${}^T \otimes$ d ${}^T$)

where d is the discard.

Guillaume Boisseau (May 27 2021 at 17:18):

ah nice

Guillaume Boisseau (May 27 2021 at 17:19):

also oops, it's not idempotent: $choice;choice = d;d^T$

Cole Comfort (May 27 2021 at 17:20):

Wow really, it just looks so much like it would be idempotent!

Guillaume Boisseau (May 27 2021 at 17:20):

We can generalize this to any black spider surrounded by choices

Guillaume Boisseau (May 27 2021 at 17:20):

I know!

Cole Comfort (May 27 2021 at 17:20):

Oh yes, I suppose this is the binary case of the thing that I just stated

Guillaume Boisseau (May 27 2021 at 17:20):

Cole Comfort said:

Wow really, it just looks so much like it would be idempotent!

But being able to make independent choices breaks the correlation

Guillaume Boisseau (May 27 2021 at 17:24):

hm, it appears we can't colorswap naively actually: $choice;discard = choice;zero = discard$

Cole Comfort (May 27 2021 at 17:26):

wait, shouldn't composing choice with a counit just always produce the discard instead of colour swapping

Cole Comfort (May 27 2021 at 17:26):

because the union of discard and cozero is discard

Guillaume Boisseau (May 27 2021 at 17:26):

yeah indeed, that's what I just stated

Cole Comfort (May 27 2021 at 17:27):

Oh yes it is, haha. Maybe I have to re-check my other calculations, now haha

Guillaume Boisseau (May 27 2021 at 17:28):

might have sth to do with the fact that colorswap also flips the 2-cells i.e. the inclusion order

Guillaume Boisseau (May 27 2021 at 17:36):

shit we don't have abelian bicat axioms either, namely choice doesn't slide laxly along the white spider

Guillaume Boisseau (May 27 2021 at 17:36):

which to be fair was rather surprising

Guillaume Boisseau (May 27 2021 at 17:37):

in my head choice was the superposition of discard;cozero and zero;codiscard, so any property shared by those two things would hold for choice. But if I calculate that doesn't appear to be true

Cole Comfort (May 27 2021 at 17:37):

I think this means that the colour swap doesn't extend to a functor in this fragment, at least in the way I am thinking.

Guillaume Boisseau (May 27 2021 at 17:38):

yeah

Guillaume Boisseau (May 27 2021 at 17:38):

maybe if it mapped choice to something else?

Cole Comfort (May 27 2021 at 17:39):

Is there a generator which takes units to zero?

Cole Comfort (May 27 2021 at 17:39):

The transpose of which would be the obvious candidate if it exists...

Guillaume Boisseau (May 27 2021 at 17:42):

Cole Comfort said:

Is there a generator which takes units to zero?

what do you mean by this?

Cole Comfort (May 27 2021 at 17:44):

Like that takes $z\mapsto z$ , $d^T \mapsto z$

Cole Comfort (May 27 2021 at 17:44):

where the action is just post-composition

Cole Comfort (May 27 2021 at 17:45):

But we don't want it to be something silly like $z^T;z$

Guillaume Boisseau (May 27 2021 at 17:46):

hm, good question

Guillaume Boisseau (May 27 2021 at 17:47):

IMG_20210527_184441.jpg

Guillaume Boisseau (May 27 2021 at 17:47):

here's a cool one: ^

Cole Comfort (May 27 2021 at 17:50):

Guillaume Boisseau said:

IMG_20210527_184441.jpg

"At least one leg must be zero"

Guillaume Boisseau (May 27 2021 at 17:50):

from which I can deduce that if choice has a colorswap, it must be a subset of cozero;zero

Guillaume Boisseau (May 27 2021 at 17:51):

from which I deduce that there is no extension of colorswap that includes choice, because cozero;zero doesn't respect all the colorswapped properties of choice :(

Cole Comfort (May 27 2021 at 18:00):

I am thinking of a potential way to prove completeness as opposed to going straight to a normal form.

First, prove completeness for the prop of matrices with this generator adjoined wrt to the interpretation into piecewise linear maps between f.d. vector spaces.

Second, show (hope) that this category is finitely complete, and show that the category of spans thereof arises in terms of a distributive law.

Third show (hope) it is regular and then take a quotient to get you from spans to relations.

Guillaume Boisseau (May 27 2021 at 18:02):

I see, so go the same way as the Interacting Hopf Algebras approach

Robin Piedeleu (May 27 2021 at 18:02):

We also need the order generator, right? So we need not just matrices+choice.

Guillaume Boisseau (May 27 2021 at 18:03):

that might work for just matrices plus this. But if we also want comparison I'm not sure it'll work then

Guillaume Boisseau (May 27 2021 at 18:03):

yeah that

Guillaume Boisseau (May 27 2021 at 18:03):

I'm still very curious what we'd get with IH+choice or matrices+choice

Robin Piedeleu (May 27 2021 at 18:03):

And the order and choice generators are both very non-function-like.

Cole Comfort (May 27 2021 at 18:03):

I feel like getting choice+affine would be very easy from choice+linear

Robin Piedeleu (May 27 2021 at 18:04):

Which leaves me with little hope that the category you get would be sufficiently well-behaved.

Guillaume Boisseau (May 27 2021 at 18:04):

affine is generally easy yeah; comparison is hairier

Robin Piedeleu (May 27 2021 at 18:04):

Btw, have you looked at the interaction between the order and choice?

Guillaume Boisseau (May 27 2021 at 18:05):

there's not much as far as I can tell

Robin Piedeleu (May 27 2021 at 18:05):

Yeah, couldn't see much; that's why I asked :)

Cole Comfort (May 27 2021 at 18:06):

yeah mixing the 2-cells with the union is confusing to me

Cole Comfort (May 27 2021 at 18:07):

2-cells are obviously like implication and union is like disjunction, but trying to compute these things is so hairy

Guillaume Boisseau (May 27 2021 at 18:08):

oh, I understood that as choice+comparison, which is where I haven't found many interesting things

Guillaume Boisseau (May 27 2021 at 18:09):

choice+2-cells gives the cartesian bicat things, but apart from that not much either

Cole Comfort (May 27 2021 at 18:10):

I mean, just trying to calculate things is harder in this case

Cole Comfort (May 27 2021 at 18:12):

Also there is one obvious identity I think we have missed. Choice eats up scalars

Guillaume Boisseau (May 27 2021 at 18:13):

ah yeah there's that too

Guillaume Boisseau (May 27 2021 at 18:17):

Actually choice+2-cells is the only one that seems to somewhat pin down what choice does, cause we have $discard;zero \subset choice$ and the symmetric

Guillaume Boisseau (May 27 2021 at 18:19):

Can we somehow express that choice is the minimal such thing?

Guillaume Boisseau (May 27 2021 at 18:20):

Many axioms are compatible with choice=codiscard;discard. The main one that isn't is where self-connected choice gives zero, that Robin mentioned a while back

Guillaume Boisseau (May 27 2021 at 18:23):

Yeah, intuitively those two things together seem to pin choice down: it must accept one or the other input being zero, and if both are equal they must be zero. Can we derive the other things from them?

Reid Barton (May 27 2021 at 18:29):

@Guillaume Boisseau Perhaps totality of the order actually lies outside the scope of the completeness theorem? After all, as a logical formula, $x \le y \vee y \le x$ is not in the fragment of regular logic; and the graph of the function $\max \{x,y\}$ isn't a polyhedron.

Guillaume Boisseau (May 27 2021 at 18:32):

I can prove something that looks close to totality, namely that for a relation expressible in the language, $\exists y, R(x,y)$ iff $\exists x_1 x_2 y_1 y_2, x=x_1+x_2, R(x_1, y_1), R(x_2, y_2), y_1 \leq 0, y_2 \geq 0$

Guillaume Boisseau (May 27 2021 at 18:33):

so I can case-split on whether y is positive or negative, but instead of having a real "or" I sum the corresponding x's

Reid Barton (May 27 2021 at 18:36):

Is this in the linear or the affine setting?

Guillaume Boisseau (May 27 2021 at 18:36):

that's in the linear+comparison setting, i.e. cones

Guillaume Boisseau (May 27 2021 at 18:40):

in the affine/polyhedra setting I think only the colorswap of this still holds, which is $R(x,0)$ iff $\exists y_1 y_2, R(x, y_1), R(x, y_2), y_1 \leq 0, y_2 \geq 0$. In the linear/cones setting both hold.

Reid Barton (May 27 2021 at 18:40):

I see. And I assume $x$ could be any number of variables, for example zero, in which case it says that any $y$ can be written as the sum of something nonnegative and something nonpositive.

Guillaume Boisseau (May 27 2021 at 18:40):

absolutely

Guillaume Boisseau (May 27 2021 at 18:42):

but that in itself doesn't give totality, right?

Reid Barton (May 27 2021 at 18:43):

Right, for example if we give R^2 the componentwise partial order, then it's still true (since we can write each component that way)

Guillaume Boisseau (May 27 2021 at 18:43):

only if we could ensure that one of the two is zero, which we can with the choice gadget! So maybe choice can express totality more directly

Guillaume Boisseau (May 27 2021 at 18:47):

IMG_20210527_194652.jpg

Guillaume Boisseau (May 27 2021 at 18:47):

here's totality expressed using the choice operator ^

Guillaume Boisseau (May 27 2021 at 18:48):

namely that every x can be written as the sum of a positive thing and a negative one, one of which must be zero

Reid Barton (May 27 2021 at 18:56):

But there's a subtlety in that this only really expresses a disjunction "$x \le y$ or $y \le x$" to the extent that the choice operator has the intended semantics that either the first argument is zero or the second argument is zero

Guillaume Boisseau (May 27 2021 at 18:57):

indeed. That would be if we were adding comparison to an established setting that includes choice I guess

Reid Barton (May 27 2021 at 18:59):

For example, I could give R^2 the componentwise choice relation, sending $(x_1, x_2), (y_1, y_2)$ to "($x_1 = 0$ or $y_1 = 0$) and ($x_2 = 0$ or $y_2 = 0$)"

Guillaume Boisseau (May 27 2021 at 19:01):

nice example! yeah we'd need other axioms to pin down choice to what we want first

Reid Barton (May 27 2021 at 19:02):

I think you cannot rule out this kind of componentwise construction as long as you have only axioms that can be expressed in regular logic... though I'm not very confident about this.

Guillaume Boisseau (May 27 2021 at 19:04):

oh, that would rule out our entire endeavour :o EDIT: wait, maybe not

Reid Barton (May 27 2021 at 19:04):

So, I think it's probably best to accept that totality might fail "externally" but it still holds "internally" in the sense that there is a function $\max\{x, y\}$ which satisfies all the expected relations.

Reid Barton (May 27 2021 at 19:05):

It's just that, from the external point of view, $\max\{x, y\}$ might not equal either $x$ or $y$.

Reid Barton (May 27 2021 at 19:06):

By the way, I should mention these slides of Marra and Menni: https://math.unice.fr/tacl/assets/2019/contributed/s3/4/4-marra-menni.pdf
What they are doing is at least one or two steps removed from what you are doing, but there's clearly some relationship there.

Guillaume Boisseau (May 27 2021 at 19:06):

I see. We can live with that

Robin Piedeleu (May 27 2021 at 19:09):

Is adding max directly as a $2\rightarrow 1$ generator instead of the choice generator equally expressive?

Guillaume Boisseau (May 27 2021 at 19:11):

I think equally: using max we can build the absolute value function, and by rotating the absolute value we can recover the initial diode-like generator we had, from which we can build choice

Robin Piedeleu (May 27 2021 at 19:14):

Ok, this seems much more standard then. We should look for results that might rule out what we're trying to do. For example, is there a quantifier elimination result for max,+ (aka tropical) arithmetic?

Guillaume Boisseau (May 27 2021 at 19:15):

what's the link between quantifier elimination and what we're trying to do?

Reid Barton (May 27 2021 at 19:30):

I claim the following describe the same class of subsets of R^n:
(a) Sets definable (in full first-order logic with quantifiers) using $+$, scalar multiplication, constants and $<$, that are closed in R^n.
(b) Finite unions of polyhedra.
(c) Sets cut out by a formula of the form $F(x_1, \ldots, x_n) = 0$, where $F$ is a function built from $\max$ and affine linear combinations.

The sets of the form (b) are closed under projection, because the projection of an individual polyhedron is one (I think?)

Reid Barton (May 27 2021 at 19:32):

It's actually a bit peculiar to the piecewise linear setting that this works for closed subsets (as opposed to closed+bounded subsets). For example, suppose we also allow multiplication as an operation. Then the set $\{(x,y) \mid xy = 1\}$ has projection $R - \{0\}$, which is not closed.

Robin Piedeleu (May 27 2021 at 19:42):

Guillaume Boisseau said:

what's the link between quantifier elimination and what we're trying to do?

Its not entirely clear to me either but it might provide clues. So would (un)decidability of the corresponding first-order theory. As I understand it, quantifier elimination is kind of the standard model-theoretic version of the sort of normal form argument we use to prove completeness for these diagrammatic theories (which are restricted to the regular logic fragment). For example, for polyhedra, i.e. the logic of the reals as an ordered abelian group, quantifier elimination is proved by Fourier-Motzkin elimination, which is also what you use for the diagrammatic proof. One way to see it is that it gives a procedure to go from conjunctions of equations with some existentially quantified variables (span form) and an equivalent formula without existential quantifiers (cospan form). This is a bit hand-wavy but maybe someone more knowledgeable could make the connection more precise.

Guillaume Boisseau (May 27 2021 at 19:49):

@Reid Barton if I'm following right, (b) closed under projection means we have quantifier elimination? That's cool!

Guillaume Boisseau (May 27 2021 at 19:52):

@Robin Piedeleu I see, thanks

Guillaume Boisseau (May 27 2021 at 21:00):

ah, so we do know that the theory of polyhedra is closed under projection. So we can deduce that the theory of union of polyhedra is too

Guillaume Boisseau (May 27 2021 at 21:05):

ah, that's not quite quantifier elimination: it only says that plugging a black dot into the diagram for some union of polyhedra still gives some union of polyhedra. We still need to prove (c), namely that any union of polyhedra can be described by a quantifier-free formula. Presumably we know that for a single polyhedron?

Guillaume Boisseau (May 27 2021 at 21:06):

(I'm just untangling what you guys said because that stuff is new to me)

Guillaume Boisseau (May 27 2021 at 21:28):

good news: the axioms we've mentioned so far are enough to pin down choice if we know we're interpreting into R^n. It's not too hard to see: using the scalar and self-loop axioms, if $y \neq 0, R(x,y) \iff R(x,y*x/y) \iff R(x,x) \iff x=0$. And we also have $R(x,0)$ as an axiom.

Guillaume Boisseau (May 27 2021 at 21:31):

that doesn't mean they're enough to derive everything we want diagrammatically. In fact they don't look enough

John Baez (May 28 2021 at 00:32):

"Closed under projection" is the same as existential quantifier elimination, since the effect of projection on a subset is to produce a new subset defined with an existential quantifier.

A famous fact about subsets of $\mathbb{R}^n$ defined using inequalities ($\le$ and $\lt$), boolean connectives ($\vee, \wedge, \neg, \to$) and polynomial functions is that they are closed under projection. This is called the Tarski-Seidenberg theorem.

Also the complement of any such subset is again such a subset.

So, if you have any subset of $\mathbb{R}^n$ defined using inequalities ($\le$ and $\lt$), polynomial functions, boolean connectives and quantifiers, you can eliminate all the quantifiers and define your set using just inequalities ($\le$ and $\lt$), polynomial functions and boolean connectives!

John Baez (May 28 2021 at 00:35):

One spinoff is that if you compose two relations between $\mathbb{R}^n$'s defined using inequalities, polynomial functions and boolean connectives, you get another such relation.

I used this fact in my work with Blake Pollard on black-boxing reaction networks.

John Baez (May 28 2021 at 00:37):

The result @Reid Barton is claiming should be good for proving some similar theorems.

Guillaume Boisseau (May 28 2021 at 02:16):

ah you're right we only eliminate existential quantifiers that way. The good thing is, our graphical syntax only allows existential quantifiers anyways. I wonder if universal quantifiers would allow more subsets to be described

Guillaume Boisseau (May 28 2021 at 02:29):

here's one approach to axiomatizing this mess: remember we defined SMITs to be like SMTs except axioms could be inclusions instead of equalities. We could define SMUTs similarly, where axioms can include the union operator. Then we don't even need to add choice, and I expect that natural axioms for how union works should be enough to prove completeness of the SMUT of polyhedra

Guillaume Boisseau (May 28 2021 at 02:32):

Once we have that, we can still study the choice operator within normal (in)equational theories. We'd only have to define the union in terms of it and check that it respects the relevant axioms. The same way we can have equational theories that have a natural order arising from a Frobenius structure, I expect we'd get an inequational theory that has a natural union arising from a choice structure

Guillaume Boisseau (May 28 2021 at 03:12):

Would that work?

Robin Piedeleu (May 28 2021 at 08:28):

Guillaume Boisseau said:

here's one approach to axiomatizing this mess: remember we defined SMITs to be like SMTs except axioms could be inclusions instead of equalities. We could define SMUTs similarly, where axioms can include the union operator. Then we don't even need to add choice, and I expect that natural axioms for how union works should be enough to prove completeness of the SMUT of polyhedra

Sounds reasonable---there's plenty of diagrammatic calculi out there that exploit semiring structure on the homsets and use some form of sum of diagrams.

Robin Piedeleu (May 28 2021 at 08:30):

Guillaume Boisseau said:

Once we have that, we can still study the choice operator within normal (in)equational theories. We'd only have to define the union in terms of it and check that it respects the relevant axioms. The same way we can have equational theories that have a natural order arising from a Frobenius structure, I expect we'd get an inequational theory that has a natural union arising from a choice structure

I'm not sure I understand what you mean here. You'd want to show some sort of equivalence between two categories, one defined as a SMUT, the other a standard SMT with choice? Wouldn't that be equivalent to axiomatising choice directly as an SMT?

Cole Comfort (May 28 2021 at 09:18):

Is this a bimonoidal category?

If so, you could use their proof sheets: https://arxiv.org/pdf/2010.13361.pdf

However, in the case when both tensor products are symmetric, this isn't proven to be complete

Guillaume Boisseau (May 28 2021 at 09:33):

Robin Piedeleu said:

Guillaume Boisseau said:
I'm not sure I understand what you mean here. You'd want to show some sort of equivalence between two categories, one defined as a SMUT, the other a standard SMT with choice? Wouldn't that be equivalent to axiomatising choice directly as an SMT?

Yeah that's equivalent to axiomatizing choice as a SMT (probably SMIT actually), since that's what we want to do. But I'm hoping going through the SMUT would make completeness a lot nicer

Guillaume Boisseau (May 28 2021 at 09:34):

Cole Comfort said:

Is this a bimonoidal category?

Really looks like it

Guillaume Boisseau (May 28 2021 at 10:05):

assuming I have a well-behaved union operator, I can easily make unions of polyhedra. A naive normal form would be just to independently take the normal form of each polyhedron in the union. That doesn't feel enough. Is there some canonical way to split our subset into polyhedra? Simplical complexes maybe?

Guillaume Boisseau (May 28 2021 at 10:07):

in my head there should be a somewhat unique triangulation with minimal number of simplices, is that remotely the case?

Guillaume Boisseau (May 28 2021 at 10:08):

yeah no obviously not, the square has two non-obviously equal triangulations

Guillaume Boisseau (May 28 2021 at 10:21):

Can't even show that [1,2]U[2,3]=[1,3] :exhausted:

Guillaume Boisseau (May 28 2021 at 11:05):

ah, yeah I can: not hard to reduce it to the case of $[-\infty,b] \cup [b,\infty]$, which itself is just totality

Guillaume Boisseau (May 28 2021 at 11:27):

This generalizes! Assume A and B are subspaces separated by a hyperplane $H(x)=0$. Then using totality I can case-split on which side of the hyperplane we are, and reduce $A \cup B = C$ to $A(x) \iff C(x) \land H(x) \geq 0$ and $B(x) \iff C(x) \land H(x) \leq 0$. Now if we can reduce any union of polyhedra to a union where the polyhedra don't intersect too much, then that should give us completeness! So new normal form is: either a simple polyhedron, or a union $A \cup B$ of normal forms where A and B are separated by a hyperplane.

Guillaume Boisseau (May 28 2021 at 11:29):

Yeah pretty sure we can do all that diagrammatically. The only axioms I used are those of the theory of polyhedra, obvious generic axioms about union, and one axiom that uses the union: totality

Robin Piedeleu (May 28 2021 at 12:01):

Guillaume Boisseau said:

This generalizes! Assume A and B are subspaces separated by a hyperplane $H(x)=0$. Then using totality I can case-split on which side of the hyperplane we are, and reduce $A \cup B = C$ to $A(x) \iff C(x) \land H(x) \geq 0$ and $B(x) \iff C(x) \land H(x) \leq 0$. Now if we can reduce any union of polyhedra to a union where the polyhedra don't intersect too much, then that should give us completeness! So new normal form is: either a simple polyhedron, or a union $A \cup B$ of normal forms where A and B are separated by a hyperplane.

That's exciting! The intersection might be non-convex, but we can always express it as a finite union of convex regions by cutting it further with auxilary hyperplanes. Then I suppose starting from the union of A and B, we can always obtain a decomposition in which the component polyhedra intersect pariwise along a single hyperplane by cutting the intersection into smaller polyhedra using these auxilary hyperplanes. This is entirely geometric intuition for the moment, though.

Robin Piedeleu (May 28 2021 at 12:02):

So the thing to do is find the equation for these extra hyperplanes.

Guillaume Boisseau (May 28 2021 at 12:04):

a convex polyhedron is defined by a bunch of hyperplane boundaries, and we can always choose one of those to cut along

Guillaume Boisseau (May 28 2021 at 12:04):

they are easy to read out from the normal form too

Robin Piedeleu (May 28 2021 at 12:06):

What I'm saying is that to obtain your normal form for the union of two polyhedra, we night need more, to make sure we separate the pieces into polyhedra that intersect at most along a single hyperplane. Wasn't that what you were trying to say?

Guillaume Boisseau (May 28 2021 at 12:06):

yes I agree. I was only pointing out that it's easy to find the equation for the hyperplanes

Robin Piedeleu (May 28 2021 at 12:06):

But not necessarily of these extra hyperplanes.

Guillaume Boisseau (May 28 2021 at 12:07):

why not?

Guillaume Boisseau (May 28 2021 at 12:07):

if two polyhedra intersect non-trivially, there is a face of say A that has some B on both sides. Cut B along the hyperplane corresponding to that face. Repeat

Robin Piedeleu (May 28 2021 at 12:09):

I see, that makes sense.

Guillaume Boisseau (May 28 2021 at 12:09):

my geometric intuition says that works. I wouldn't know how to make this precise though

Guillaume Boisseau (May 28 2021 at 12:11):

actually this still works if A and B are themselves unions of polyhedra. We can still choose a face of A to split B

Guillaume Boisseau (May 28 2021 at 12:14):

so to normalize AUB, find a face of A that cuts B into B1 and B2, then take normalize(A U B1) U normalize(B2) as a normal form. Does this terminate?

Robin Piedeleu (May 28 2021 at 12:18):

It should? A face of A is given by a hyperplane and you have only finitely many hyperplanes that describe A and B. The same face cannot be used twice because in A U Bi the face of A you used does not cut each Bi further, right?

Guillaume Boisseau (May 28 2021 at 12:24):

Yeah that sounds right :)

Guillaume Boisseau (May 28 2021 at 12:25):

So if we're right this gives a complete SMUT for union of polyhedra. To get a complete SMT, we could just define a union operator using choice and assert as axioms that it behaves properly! So we also get a complete SMT! Only remains to pick prettier axioms

Cole Comfort (May 28 2021 at 12:30):

Guillaume Boisseau said:

So if we're right this gives a complete SMUT for union of polyhedra. To get a complete SMT, we could just define a union operator using choice and assert as axioms that it behaves properly! So we also get a complete SMT! Only remains to pick pretty axioms

I think that a complete "SMUT" could still be a ways away from yielding a complete "SMT."

Consider the case of the bimonoidal category of matrices over a ring. The bimonoidal theory can be described in terms of the embedding of the monoidal theory generated the bicommutative bialgebra which generates the additive fragment. However, a symmetric monoidal theory for the multiplicative tensor is much more complicated.

Robin Piedeleu (May 28 2021 at 12:31):

So the union operator we get from choice is the one that operates on the underlying polyhedral normal form (where you replace the co-zero with a sum of choices gadget)? We need a proper union operation that does not refer to this form, no?

Robin Piedeleu (May 28 2021 at 12:32):

Hmm...maybe that does not matter actually

Robin Piedeleu (May 28 2021 at 12:39):

What we want is an equivalence between the SMUT and the SMT (well the free things quotiented by these theories). The union operator is a way of describing one direction of this equivalence, SMUT $\rightarrow$ SMT. The other direction is the decomposition of choice as a union of two lines. Is this the strategy?

Guillaume Boisseau (May 28 2021 at 12:39):

@Cole Comfort indeed I don't think you can always get a complete SMT from a complete SMUT. But we're in a lucky case because we know how to reify union as an operation on diagrams

Guillaume Boisseau (May 28 2021 at 12:40):

@Robin Piedeleu Yeah something like that

Cole Comfort (May 28 2021 at 12:41):

Robin Piedeleu said:

What we want is an equivalence between the SMUT and the SMT (well the free things quotiented by these theories). The union operator is a way of describing one direction of this equivalence, SMUT $\rightarrow$ SMT. The other direction is the decomposition of choice as a union of two lines. Is this the strategy?

Ah, I see

Robin Piedeleu (May 28 2021 at 14:56):

A bit more precisely, let $\mathcal{P}$ be the free (semi)lattice-enriched prop, quotiented by the SMUT of polyhedral relations and let $\mathcal C$ be the free prop quotiented by the SMT for unions of polyhedra (that we still have to figure out in full). Let $F : \mathcal{C}\rightarrow\mathcal{P}$ be the identity on all generators except choice, which is mapped to (co-zero; co-discard) U (discard ; zero). Let $G : \mathcal{P}\rightarrow\mathcal{C}$ be the mapping induced by the union operator that Guillaume constructed here. We'll need the right axioms on choice to check that this functorial and monoidal.

Then $F\circ G$ is the identity, again by what Guillaume showed here which requires going through the normal form for polyhedral relations.

For $G\circ F$, we just check it is the identity for all generators of $\mathcal C$ (which is trivial except for choice)?

Spencer Breiner (May 28 2021 at 16:55):

Guillaume Boisseau said:

here's one approach to axiomatizing this mess: remember we defined SMITs to be like SMTs except axioms could be inclusions instead of equalities. We could define SMUTs similarly, where axioms can include the union operator. Then we don't even need to add choice, and I expect that natural axioms for how union works should be enough to prove completeness of the SMUT of polyhedra

Allowing inclusion axioms as opposed to equations sounds a lot like allowing sequents as axioms in a logical theory rather than logical equivalences. In that case, though, we can always replace a sequent $\varphi\vdash\psi$ with an equivalent equivalence $\varphi\iff\varphi\wedge\psi$. This makes the process of building a quotient theory easier.

Can we do something similar here? If not, what goes wrong, and how do you get around it to define the quotient SMIT?

Guillaume Boisseau (May 28 2021 at 17:01):

Yes, we can do something similar not for all SMITs but for Frobenius theories, i.e. those with a well-behaved Frobenius algebra. More details here: https://arxiv.org/pdf/1711.08699.pdf . The Frob algebra allows the definition of a join and then we can recover the order like you mentioned

Guillaume Boisseau (May 28 2021 at 17:02):

and indeed, I'm trying to do the corresponding thing for SMUTs: somehow find a way to express the extra structure (here the semilattice) equationally

Guillaume Boisseau (May 28 2021 at 17:58):

the quotient SMIT is described is at the beginning of part 3 in the paper I just linked. Tbh there aren't a lot of details

Spencer Breiner (May 28 2021 at 22:11):

Ah. I've read & cited this paper before :upside_down:

Here we're leaning on the enrichment in Pos to interpret inequalities. Naively, this looks like a different strategy from the approach I described above, which gets rid of the inequalities/sequents altogether. I'm still curious whether there's a connection.

The logical equivalence I wrote down only makes sense in a semicartesian setting, since the implication $\varphi\wedge\psi\Rightarrow\varphi$ is just discarding on the right.

Assuming that is given, then the content of the equivalence is replacing a generator $p:\varphi\to\psi$ (switching to monoidal notation), by another $q:\varphi\to\varphi\otimes\psi$, recovering $p$ by discarding on the left.

Naively, I would expect this to form a section/retraction pair: $q$ followed by discarding on the right is the identity, but thinking proof-relevantly I wouldn't expect the reverse to be true.

Guillaume Boisseau (May 29 2021 at 07:54):

the problem is that you require some cartesian-like structure right? Unless you can get it for free somehow I don't expect this to work in general

Guillaume Boisseau (May 29 2021 at 23:31):

Btw, I figured out how to define union without talking about normal forms. This is sooo much more convenient x)

Guillaume Boisseau (May 29 2021 at 23:31):

Kinda obvious in retrospect

Guillaume Boisseau (May 29 2021 at 23:31):

IMG_20210530_003046.jpg

Guillaume Boisseau (May 29 2021 at 23:48):

interestingly, it seems the many-legged choice thing can be defined from the one-legged one in the theory of cones/polyhedra, but not in plain GLA/GAA. I expect we can get the SMUT for GLA/GAA/cones/polyhedra equationally in one swoop by axiomatizing the many-legged version

Guillaume Boisseau (May 29 2021 at 23:49):

or maybe even axiomatizing this new thing that's the union of the identity and the unit, since that requires only a single Frobenius algebra

Guillaume Boisseau (May 29 2021 at 23:55):

help I need notation for the new thing and I'm out of quick-to-draw shapes :cry:

Guillaume Boisseau (May 30 2021 at 02:32):

Much better. I have axioms on this new choice thing that guarantee (in the linear case) that the corresponding union is indeed a union wrt the order.
Only problem is distributivity of choice over composition: the weird part is that the last equality only holds when b and c don't have outgoing wires. That's not a pretty axiom but I can't find better things to replace it

Guillaume Boisseau (May 30 2021 at 02:32):

IMG_20210530_032906.jpg

Robin Piedeleu (May 30 2021 at 09:02):

Guillaume Boisseau said:

interestingly, it seems the many-legged choice thing can be defined from the one-legged one in the theory of cones/polyhedra, but not in plain GLA/GAA. I expect we can get the SMUT for GLA/GAA/cones/polyhedra equationally in one swoop by axiomatizing the many-legged version

Which part of the definition of union above requires polyhedral relations specifically? It does not use the comparison generator as far as I can see, just the one-legged choice, copy and (co)addition. There's something I must be missing...

Robin Piedeleu (May 30 2021 at 09:04):

Guillaume Boisseau said:

IMG_20210530_003046.jpg

Should $n=m$?

Robin Piedeleu (May 30 2021 at 09:06):

Guillaume Boisseau said:

or maybe even axiomatizing this new thing that's the union of the identity and the unit, since that requires only a single Frobenius algebra

Yes, that seems like a very interesting thing to try to pin down axiomatically!

Guillaume Boisseau (May 30 2021 at 11:10):

n and m can be different

Guillaume Boisseau (May 30 2021 at 11:13):

The thing that requires polyhedral relations is defining many-legged choice from one-legged choice, because it requires a 1 to n diagram such that plugging a unit gives n units and plugging a zero gives n zeros. Afaik that's impossible in GLA

Cole Comfort (May 30 2021 at 11:13):

It is interesting that this generator is the union of the state preparation in both complementary observables.

Cole Comfort (May 30 2021 at 11:17):

Guillaume Boisseau said:

The thing that requires polyhedral relations is defining many-legged choice from one-legged choice, because it requires a 1 to n diagram such that plugging a unit gives n units and plugging a zero gives n zeros. Afaik that's impossible in GLA

This is not possible in GLA because of a variation of the no cloning theorem

Guillaume Boisseau (May 30 2021 at 11:21):

Oh interesting!

Guillaume Boisseau (May 30 2021 at 11:23):

Do you know how to prove that?

Guillaume Boisseau (May 30 2021 at 11:26):

Guillaume Boisseau said:

IMG_20210530_003046.jpg

@Robin Piedeleu this definition of union uses many-legged choice, hence the issue I just mentioned

Guillaume Boisseau (May 30 2021 at 11:31):

Guillaume Boisseau said:

IMG_20210527_153341.jpg

This older definition of union subtly hides the number of legs. You can read it as using many-legged choice too, even though I had intended only one-legged. You can make it work with one-legged by merging all the legs into one with a black spider just before the choice, but that only works because all the Pi end with a comparison operator

Robin Piedeleu (May 30 2021 at 11:32):

Then I'm confused about the construction you give: the diagram you give for union seems to not be well typed if $n\neq m$ because $n$ copy nodes are connected to $m$ addition nodes.

And, if $n=m$, can't you define a $n \rightarrow n$ choice with $n$ copies of the basic choice generator, such that the union diagram you gave implements the union of two arbitrary $n\rightarrow 0$ diagrams $a$ and $b$ as in your picture?

Guillaume Boisseau (May 30 2021 at 11:33):

hm, which n and m are you talking about actually?

Robin Piedeleu (May 30 2021 at 11:34):

Guillaume Boisseau said:

IMG_20210530_003046.jpg

I mean in this picture (sorry discussions can get confusing on this platform, especially about diagrams).

Guillaume Boisseau (May 30 2021 at 11:36):

if I use many copies of the 1->1 choice, I won't end up with only the two options I want, I'll also get plenty of mixtures with some zeros and some black dots on each side

Cole Comfort (May 30 2021 at 11:36):

What are the options you want? the union of a bunch of things of the same colour?

Robin Piedeleu (May 30 2021 at 11:36):

Aaah ok, I get it!

Robin Piedeleu (May 30 2021 at 11:37):

But, for the union operator, you're still only using the $n=m$ case, right?

Guillaume Boisseau (May 30 2021 at 11:37):

@Cole Comfort I want the union of "all zeros on the left and all units on the right" and "same thing but flipped"

Guillaume Boisseau (May 30 2021 at 11:37):

Robin Piedeleu said:

But, for the union operator, you're still only using the $n=m$ case, right?

I am

Robin Piedeleu (May 30 2021 at 11:37):

ok, all clear for me, thanks!

Cole Comfort (May 30 2021 at 11:39):

I like this new generator more because it feels like it fits more naturally in the Lagrangian picture. Indeed you could just add it as a generator, and then add another type of undoubled wires

Cole Comfort (May 30 2021 at 11:40):

and it is almost like a form of measurement

Guillaume Boisseau (May 30 2021 at 11:40):

oh you mean using it to pass from doubled to single wire?

Guillaume Boisseau (May 30 2021 at 11:40):

such a weird operation, it's like measuring one of the wires but you don't know which

Cole Comfort (May 30 2021 at 11:41):

yes exactly

Cole Comfort (May 30 2021 at 11:42):

This diverges from the quantum picture where you can only measure X or Z, but doing so discards the other side.

Guillaume Boisseau (May 30 2021 at 11:43):

can you have an ordering on diagrams in the quantum picture?

Cole Comfort (May 30 2021 at 11:44):

Yes, but only for mixed states. In the pure case, everything has the same dimension so it is iso

Cole Comfort (May 30 2021 at 11:45):

(the pure things are precisely ${\sf AffLagRel}_{\mathbb{F}_p} \cong {\sf Stab}_p^\sim$ for $p$ an odd prime)

Cole Comfort (May 30 2021 at 11:46):

I am thinking of considering the multicoloured prop of affine lagrangian relations with these undoublings, and then proving completeness for it

Cole Comfort (May 30 2021 at 11:47):

so this generator would fit nicely into this picture

Cole Comfort (May 30 2021 at 11:51):

I wonder if it has an operational interpretation in terms of electrical circuits.

Guillaume Boisseau (May 30 2021 at 12:16):

I strongly doubt it x)

Cole Comfort (May 30 2021 at 22:47):

I don't know, it feels kind of nondeterministic. Like the computation branches on the result of a Z or X measurement.

Guillaume Boisseau (May 30 2021 at 23:21):

that's not what we get for electrical circuits: the whole point was to get diodes but they're not nondeterministic

Cole Comfort (May 30 2021 at 23:24):

I know, but even though diodes are deterministic, this isn't a diode, despite them being derived.

Guillaume Boisseau (May 30 2021 at 23:28):

sure, but it's not more nondeterministic than other relational things

Guillaume Boisseau (May 30 2021 at 23:30):

like, I just want to dispel the intuition that there's somehow a new layer of superposition happening here. It's just a normal relation that happens to be made of multiple linear pieces instead of a single one

Cole Comfort (May 30 2021 at 23:42):

I am not claiming that there is somehow a "new layer of superposition," but rather that it appears that such a circuit relates elements iff replacing this generator with Z or X measurements on the same wire results in a circuit which relates these elements. So it is not that something new is being introduced, but rather that the condition that the symplectic form vanishes is no longer constraining the system.

Cole Comfort (May 30 2021 at 23:50):

Not all relations have reasonable operational interpretations for eletrical circuits nor stabilizer circuits.

Guillaume Boisseau (May 31 2021 at 13:52):

what's a stabilizer circuit?

Cole Comfort (May 31 2021 at 13:58):

In short: stabilizer circuits (in the odd prime dimensional case) are the affine Lagrangian relations over $\mathbb{F}_p$, corresponding to a very important (but non universal) fragment of quantum circuits. Since changing the field between real rational functions and finite prime fields changes the semantics from electrical circuits to this fragment of quantum circuits, I am trying to use the intuition from both cases.

Cole Comfort (May 31 2021 at 13:59):

Because on the quantum side of things, these circuits have been studied lots, even from a diagrammatic perspective (stabilizer ZX calculi).

Guillaume Boisseau (May 31 2021 at 16:28):

oh cool

Guillaume Boisseau (Jun 03 2021 at 01:48):

@Robin Piedeleu hm you were right about hyperplanes being hard to find actually, my geometric intuition misled me.
If two polyhedra are intersecting I still think we can choose one face and extend it into a cutting hyperplane. But if they don't intersect we kinda want to find a hyperplane in between them and I don't know how to choose one

Guillaume Boisseau (Jun 03 2021 at 02:15):

And there might be none of course ><

Guillaume Boisseau (Jun 03 2021 at 02:16):

I guess the question is in which case is it clear that cutting there will make the procedure terminate. I don't want to be cutting intervals in half forever

Robin Piedeleu (Jun 03 2021 at 08:33):

I see. My immediate and naive reaction was that we could arbitrarily pick one face of either of them as the separating hyperplane, but that clearly does not work!

Could we instead proceed as in the proof of the separating hyperplane theorem? For $P$ and $Q$ two disjoint polyhedra, let $v$ be the shortest vector of $P - Q$. Then there exists $c$ such that $\langle x, v\rangle \geq c$ and $\langle y, v\rangle \leq c$ for all $x\in P$ and $y\in Q$. Here, the separating hyperplane is given by $\langle -, v\rangle = c$. I guess we need an effective way to find $v$ and $c$ diagrammatically?

Robin Piedeleu (Jun 03 2021 at 08:39):

Anyway, $v = x - y$ for $x$ the point in $P$ that's the closest to $Q$ and $y$ the point in $Q$ that's the closest to $P$. Then $c = \frac{1}{2}(|| x||^2 - ||y||^2)$ or something like that.

Guillaume Boisseau (Jun 03 2021 at 10:52):

Ohh that sounds very good

Guillaume Boisseau (Jun 03 2021 at 10:53):

I don't think we need to find anything diagrammatically, we can use the semantics to find what we need

Guillaume Boisseau (Jun 03 2021 at 10:54):

The issue is that we'll want to find a hyperplane between not just polyhedra but unions of them, and that's not convex

Guillaume Boisseau (Jun 03 2021 at 11:37):

For everyone else, here's the problem statement: we have X and Y diagrams for unions of polyhedra. We know $X \subset Y$ in the semantics (i.e. as subsets of R^n), and we want to prove that fact diagramatically. Wlog we can assume X to be a single polyhedron, because $A \cup B \subset Y \iff A \subset Y \& B \subset Y$

Guillaume Boisseau (Jun 03 2021 at 11:37):

The theory for single polyhedra is complete, so if Y is a single polyhedron we're done. The idea I had to make progress in the general case is to choose a hyperplane H in between A and B to reduce $X \subset A \cup B$ to $X \cap H^+ \subset A$ and $X \cap H^- \subset B$. Of course there will not always be such a hyperplane, but maybe we can still make progress this way

Guillaume Boisseau (Jun 03 2021 at 11:41):

hm, here's a different angle: we know that $X \subset Y \iff X \cap Y = X$. Since $X$ is a polyhedron, this means we only need to care about unions of polyhedra that equal a single polyhedron. So an alternative problem statement is to prove diagrammatically hat $X=Y$ knowing that this holds in the semantics. Hopefully that's simpler because $X$ is a single polyhedron

Guillaume Boisseau (Jun 03 2021 at 11:48):

The prototypical example is $[0,1] \cup [1,2]$. To prove that $[0,2] = [0,1] \cup [1,2]$, the way I did it was to cut along the hyperplane $x=1$, which reduces the proof to two cases of reflexivity

Robin Piedeleu (Jun 03 2021 at 12:11):

Guillaume Boisseau said:

The issue is that we'll want to find a hyperplane between not just polyhedra but unions of them, and that's not convex

Good point. But the non-convexity of these things is less wild than the arbitrary kind so we should be able to tame it. Is it enough, for a finite union of polyhedra $\bigcup_{i=0}^n P_i$ to find the hyperplane separating $P_0$ and the convex polyhedron enveloping $\bigcup_{i=1}^n P_i$, and then repeat for $P_1$, etc.?

Morgan Rogers (he/him) (Jun 03 2021 at 12:17):

why should the convex hull of the $P_i$ be disjoint from $P_0$, even if they're pairwise disjoint? (even in 1D, if we take $P_0$ between $P_1$ and $P_2$ on the line, there's a problem!)

Robin Piedeleu (Jun 03 2021 at 12:23):

You're right.

Robin Piedeleu (Jun 03 2021 at 12:31):

Then we need to consider all pairwise separating hyperplanes? Let $H_{i,j}$ be the separating hyperplane between $P_i$ and $P_j$. Define $C_{i} = \bigcap_{j\neq i} H^+_{i,j}$, the polyhedron defined by all separating hyperplanes between $P_i$ and all other $P_j$. Then, for $X\subseteq \bigcup_i P_i$ do we have $X\cap C_i\subseteq P_i$?

Guillaume Boisseau (Jun 03 2021 at 12:33):

That assumes that the polyhedra are pairwise disjoint, in which case can't we just pick $C_i = P_i$?

Guillaume Boisseau (Jun 03 2021 at 12:34):

Ah that would be missing the point

Guillaume Boisseau (Jun 03 2021 at 12:35):

Hm that's really cool, you're partitioning R^n into cells that contain a unique polyhedron. I think that works yeah, again assuming the polyhedra are disjoint

Robin Piedeleu (Jun 03 2021 at 12:35):

I thought the problem was for non-intersecting polyhedra

Guillaume Boisseau (Jun 03 2021 at 12:36):

There's an edge case where the polyhedra touch on their faces

Robin Piedeleu (Jun 03 2021 at 12:37):

(there's a pun somewhere here)

Guillaume Boisseau (Jun 03 2021 at 12:37):

My hunch is that your thing still works for that edge case, but not confident

Robin Piedeleu (Jun 03 2021 at 12:41):

That's my hunch too, because the separating hyperplane can include a face of both polyhedra (this is the case where the minimal distance between both is zero).

Robin Piedeleu (Jun 03 2021 at 12:42):

(But my intuition has been consistently rubbish about all this so I wouldn't trust myself.)

Guillaume Boisseau (Jun 03 2021 at 12:43):

Can we recover the whole space as a union of the $C_i$?

Robin Piedeleu (Jun 03 2021 at 12:53):

Not necessarily

Robin Piedeleu (Jun 03 2021 at 12:55):

Hmm... actually I don't know, maybe

Robin Piedeleu (Jun 03 2021 at 13:14):

Maybe not after all. I think if the intersection of all the $H^+_{i,j}$ is nonempty you leave out some chunk of the whole space. To see this, you can draw a picture with three convex shapes in the plane and the three separating hyperplanes that leave a whole in the middle.

Reid Barton (Jun 03 2021 at 13:20):

Guillaume Boisseau said:

The theory for single polyhedra is complete, so if Y is a single polyhedron we're done. The idea I had to make progress in the general case is to choose a hyperplane H in between A and B to reduce $X \subset A \cup B$ to $X \cap H^+ \subset A$ and $X \cap H^- \subset B$. Of course there will not always be such a hyperplane, but maybe we can still make progress this way

Is it allowed more generally to choose any hyperplane $H$ and reduce $X \subset Y$ to $X \cap H^+ \subset Y \cap H^+$ and $X \cap H^- \subset Y \cap H^-$?

Guillaume Boisseau (Jun 03 2021 at 16:21):

@Reid Barton yes absolutely, that's the general idea

Guillaume Boisseau (Jun 03 2021 at 16:29):

@Robin Piedeleu Ah yeah that's unfortunate. There should still be a way to recover the whole space from the $C_i$ and a bunch of other polyhedra defined from the $H_i$. Presumably these other polyhedra will contain none of the ones in Y

Guillaume Boisseau (Jun 03 2021 at 16:31):

The reason I want this is that if we have $R^n = \bigcup_i D_i$ such that $D_i \cap Y$ is always a single polyhedron and the $D_i$ only overlap on their boundaries, then we can reduce $X = Y$ to $\forall i. X \cap D_i = Y \cap D_i$ which are single polyhedra. So then the proof reduces to showing $R^n = \bigcup_i D_i$ diagrammatically. Hopefully for a clever choice of $D_i$ that's easier than the initial problem

Reid Barton (Jun 03 2021 at 16:38):

Hmm, so I thought you could just split along all the hyperplanes that make up the faces of polyhedra whose union is $Y$, but now I realize it doesn't always work. For instance if you have two segments in the plane that meet at a common endpoint, then you also need to include a line that separates the two other endpoints.

Guillaume Boisseau (Jun 03 2021 at 16:41):

yeah, polyhedra of dimension lower than the space have faces that aren't hyperplanes, so we kinda want to extend those into hyperplanes but that's not easy

Guillaume Boisseau (Jun 03 2021 at 17:27):

Here's a different angle: we have kind of a notion of complement. If H is a hyperplane, $H^+$ and $H^-$ are kind of complements. So if we write $Y = \bigcup_i \bigcap_j H_{ij}^+$, we have a "complement" $Y^c = \bigcap_i \bigcup_j H_{ij}^-$. Then $Y \cap Y^c$ isn't empty but should be the boundary of $Y$, which is of lower dimension.
Now, since $Y \cup Y^c = R^n$, I can show $X \subset Y \iff X \cap Y^c \subset Y \cap Y^c$. I think this is good, because $Y \cap Y^c$ should be lower dimension than $Y$. So we reduced the problem to one of lower dimension, and we can iterate until Y is a union of polyhedra of dimension 0 i.e. the empty set. And we know we can prove $X \subset \emptyset$ diagrammatically

Guillaume Boisseau (Jun 03 2021 at 17:54):

Hm, the complement is not well-defined actually: by this definition, $([0,1]\cup [1,2])^c = [-\infty,0] \cup \{1\} \cup [2, +\infty]$ which is not the same as $[0,2]^c$ :(

Guillaume Boisseau (Jun 03 2021 at 17:57):

Well, it can still be a valid procedure to find a $Z$ such that $Y \cup Z = R^n$ and $dim(Y \cap Z) < dim(Y)$, which is all we really need

Guillaume Boisseau (Jun 03 2021 at 21:16):

hm that doesn't work as well as I'd like. If we're in R^n and X is a polyhedron of dimension n, then yeah $dim(X \cap X^c) < n$. But if $dim(X) < n$ then $X^c$ is the full space $R^n$. We could try to save things by going to the smallest subspace that contains each $Y_i$ and complementing there, but then we lose the fundamental property that $Y \cup Z = R^n$. So we can't take the complement of a union in a way that always reduces dimension :(

Guillaume Boisseau (Jun 03 2021 at 22:16):

Back to @Robin Piedeleu's hyperspace idea. Write $Y = \bigcup_i Y_i$ such that the $Y_i$ have pairwise separating hyperspaces $H_{ij}$. This means $Y_i \subset H_{ij}^+$ and $Y_i \cap H_{ij}^- \subset H_{ij}$. Also $H_{ij} = -H_{ji}$.
We make a cell $c$ by choosing a direction $c(i,j) \in \{+,-\}$ for each hyperspace and intersecting all the $H_{ij}^{c(ij)}$. We should get: the union of all cells is $R^n$; for any cell c, $c \cap Y$ is a single polyhedron. If that's true then we're done

Guillaume Boisseau (Jun 03 2021 at 22:21):

grmbl that doesn't work. Take a small square $a$ that touches a bigger square on one side $b$. Take $H$ the line where they touch. It's not the case that $(a \cup b) \cap H^-$ is a single polyhedron: it's $a$ union a side of $b$

Guillaume Boisseau (Jun 03 2021 at 22:24):

I said earlier we could assume wlog that Y equals a single polyhedron in the semantics. In other words, it's convex. This should rule out annoying cases like the above, but I'm not sure how.

Guillaume Boisseau (Jun 03 2021 at 22:39):

Grmbl that might be enough but it's far from trivial: we could have all sorts of weird intersections with other things filling the gaps to make the whole convex.

Guillaume Boisseau (Jun 04 2021 at 00:02):

Reid Barton said:

Hmm, so I thought you could just split along all the hyperplanes that make up the faces of polyhedra whose union is $Y$, but now I realize it doesn't always work. For instance if you have two segments in the plane that meet at a common endpoint, then you also need to include a line that separates the two other endpoints.

Actually maybe that works too. The normal form makes sure we get all those hyperplanes I think. For example the normal form for a line segment in 2D will be something like $y \geq 0 \land y \leq 0 \land x \geq 1 \land x \leq 2$

Guillaume Boisseau (Jun 04 2021 at 01:19):

So instead of picking a set of separating hyperplanes, let's try to take the set of all hyperplanes in Y. If we're careful to include each hyperplane twice (once for each orientation), then the intersection of two cells is always another cell (unless empty). Now each $Y_i$ can be written as the union of some of those cells. In fact this is a new normal form for Y: we write Y as a union of polyhedra that are all defined using the same set of hyperplanes. I think that's pretty cool.
If $c$ is one of the cells in Y, then $Y \cap c = c$ which makes it easy to show $X \cap c \subset Y \cap c$. We're left with the case where $c$ is not in $Y$. I'm hoping convexity of Y means $Y \cap c$ is always a cell but I'm not sure.

Guillaume Boisseau (Jun 04 2021 at 01:22):

My intuition is that since $Y \cap c$ is semantically a polyhedron and also is described a union of polyhedra made using a known set of hyperplanes, then it should be the case that $Y \cap c$ can be described as a single polyhedron using those same hyperplanes. And hopefully that derivation can be done diagrammatically. If so, then we have a pretty neat proof of completeness, cause this whole thing about cells is quite elegant diagrammatically

Guillaume Boisseau (Jun 04 2021 at 01:32):

Or, maybe this normal form is a good enough? Then we'd add the hyperplanes of X to our set, write both $X$ and $Y$ in terms of the same hyperplanes, and maybe to prove $X = Y$ it suffices to check that $X$ and $Y$ use the same set of cells? We can read off which cells directly from the normal forms

Robin Piedeleu (Jun 04 2021 at 09:35):

Guillaume Boisseau said:

We're left with the case where $c$ is not in $Y$. I'm hoping convexity of Y means $Y \cap c$ is always a cell but I'm not sure.

Wait, I'm confused about notation here: $Y$ is not necessarily convex but we can assume wlog that $X$ is, right?

Guillaume Boisseau (Jun 04 2021 at 11:22):

We can assume wlog that both X and Y are convex, surprisingly enough

Guillaume Boisseau (Jun 04 2021 at 11:23):

I mean that their semantics are convex sets. Also wlog X is described as a single polyhedron. Y is still described as a union of course, otherwise we'd be done

Guillaume Boisseau (Jun 04 2021 at 11:24):

I might have been a bit imprecise in distinguishing between Y as a term and the semantics of Y as a subset of R^n

Morgan Rogers (he/him) (Jun 04 2021 at 11:44):

Guillaume Boisseau said:

We're asking what happens if we add a gadget to GAA that allows us to model diodes. So far it appears this is equivalent to extending the theory of polyhedra (https://arxiv.org/abs/2105.10946) with a gadget that gives the union of x=0 and y=0

Okay, I've only been vaguely following this topic, because I didn't know what GAA was and I was too lazy to find out, but now that I've had a look at the paper you referenced, can I get some clarification on basics here? For example, we've been talking about polyhedra as if they're the usual "shapes in n-dimensional Euclidean geometry", but that's not how they're defined in that paper, which is as sets of the form $P = \{ x \in k^n \mid Ax+b \geq0 \}$. How exactly are we identifying these with ordinary polyhedra?

Guillaume Boisseau (Jun 04 2021 at 11:47):

Those sets are exactly the convex polyhedra, and that's what I've been meaning by "polyhedra" so far in this chat

Guillaume Boisseau (Jun 04 2021 at 11:48):

But it's good timing, I was about to make a big summary

Morgan Rogers (he/him) (Jun 04 2021 at 11:54):

Guillaume Boisseau said:

Those sets are exactly the convex polyhedra, and that's what I've been meaning by "polyhedra" so far in this chat

In one dimension, these are sets of the form $\{x \mid ax + b \geq 0\}$, which is a ray starting at $-b/a$ or a point or the empty set if $a = 0$. I can see how you might argue this is somehow a polygon (or whatever the name for 1D polyhedra is), but there are clearly plenty of polyhedra (e.g. closed intervals) missing.

Guillaume Boisseau (Jun 04 2021 at 11:58):

A doesn't need to be square. In other words, the number of equations can be larger than the dimension of the space. You can easily get all closed intervals with two equations

Morgan Rogers (he/him) (Jun 04 2021 at 12:00):

Aha! That clarifies a lot. Still, I'm not sure one would normally assume that polyhedra could include infinite subsets of Euclidean space, so I'm glad I clarified that too.

Guillaume Boisseau (Jun 04 2021 at 12:01):

Ah fair, I forgot about those cases but yeah we also want them

Morgan Rogers (he/him) (Jun 04 2021 at 12:11):

I would have to understand a lot more about the diagrammatic stuff to engage with the question regarding whether one can prove that one polyhedron is a union of others diagrammatically; maybe I'll come back to that :wink:

Guillaume Boisseau (Jun 04 2021 at 12:16):

I'll try to explain that somewhat in my summary. Coming soon after my lunch ^^

Guillaume Boisseau (Jun 04 2021 at 13:40):

Le big summary of things so far

Background

We have a sound and complete diagrammatic theory of convex polyhedra (that I will call simply "polyhedra") here: https://arxiv.org/abs/2105.10946 . Polyhedron here also includes polyhedral-like shapes that go to infinity, for example the top-right quadrant $x,y \geq 0$. Terms in this theory are diagrams made from some basic generators, see there. An $n \to m$ diagram in this language is interpreted as a polyhedron in $\mathbb{R}^{n+m}$.

The theory

What we're trying to do is extend this to arbitrary unions of polyhedra. To do that, we add to our language a union operator on diagrams of the same type, and some axioms. So far I think we want:

• union distributes over composition and tensor

• union and the intersection already present in the language form a distributive
  lattice

• $x \geq 0 \cup x \leq 0 = \top$ (aka totality)

The semantics functor (call it $S$) now maps a term in this language to a union of polyhedra in $\mathbb{R}^{n+m}$. I believe the axioms mentioned above are enough to get completeness, namely that when $S(X) \subset S(Y)$ then $X \subset Y$ is provable in the theory.

Normal form

Single polyhedra (i.e. terms that don't feature the union operator) have a normal form, described in the paper above. The normal form expresses a polyhedron as the intersection of a bunch of half-spaces, where a half-space is $H^+ := \{ x | H(x) \geq 0 \}$ for some nonzero affine function $H$. I sometimes write $H$ or $H^0$ for the hyperplane $\{ x | H(x) = 0 \}$, and tend to call $H$ itself a hyperplane too.

Given a general term $X$, we can move all the unions to the top-level to get an explicit union of diagrams without unions aka polyhedra. We then normalize all those subpolyhedra. We end up with a form where $X$ is the union of intersections of half-spaces. Moreover, $A = (A \cap H^+) \cup (A \cap H^-)$ is provable, so we can add some half-spaces to a given subpolyhedron, so that in the end $X$ is a union of intersections of half-spaces, and each term in the union mentions the same set of hyperplanes.

Trying to prove completeness

Take $X$ and $Y$ such that $S(X) \subset S(Y)$. First normalize both X and Y. From the lattice axioms $A \cup B \subset Y \iff A \subset Y \land B \subset Y$, so wlog we can assume that $X$ doesn't use the union operator, i.e. is a single polyhedron.

Now $X \subset Y \iff X = X \cap Y$. So for completeness it suffices to be able to prove $X = Y$ when $X$ is a single polyhedron and $S(Y) = S(X)$ is convex. The direction $Y \subset X$ reduces to inclusions between single polyhedra, which we can prove by completeness of the theory of single polyhedra. So remains only the case $X \subset Y$ where $X$ is a single polyhedron and $S(Y)$ is convex.

The final reduction, which might not be the right approach, is as follows. Take all the hyperplanes in the normal form of $Y$ and consider all the possible intersections of the corresponding half-spaces. Call each of those a cell. From our axioms we can show that the union of all cells is the whole space. From this and lattice axioms we get $X \subset Y \iff \forall c. X \cap c \subset Y \cap c$ where $c$ ranges over the cells. Remember that $Y$ is written as a union of some of those cells. I'm hoping this makes it easy to express $Y \cap c$ as a single polyhedron, which would entail completeness.

Guillaume Boisseau (Jun 04 2021 at 14:07):

Ah, there's also a simpler approach that doesn't involve all the reductions: take all the hyperplanes in X and Y, and write X and Y in normal form using all of those hyperplanes. Then they are both unions of some of the cells defined from those hyperplanes. I suspect that when $S(X) = S(Y)$ then they use essentially the same set of cells. We just have to figure out what "essentially" means here ^^

Jacques Carette (Jun 04 2021 at 14:52):

This all feels incredibly like the linear case of Cylindrical Algebra Decomposition (CAD). For which there is a huge amount of theory, (implemented) algorithms, normal forms, etc. Also, the convex optimization people have done lots of work on representing polyhedra. Lastly, the Abstract Interpretation people have delved into polyhedral domains too.

Jules Hedges (Jun 04 2021 at 15:01):

First example of an entire extended abstract written on zulip!

Guillaume Boisseau (Jun 04 2021 at 15:18):

Jacques Carette said:

This all feels incredibly like the linear case of Cylindrical Algebra Decomposition (CAD). For which there is a huge amount of theory, (implemented) algorithms, normal forms, etc. Also, the convex optimization people have done lots of work on representing polyhedra. Lastly, the Abstract Interpretation people have delved into polyhedral domains too.

Hahaha, I'm sure I'm reinventing the wheel. Do you have references for those things by any chance?

Guillaume Boisseau (Jun 04 2021 at 15:24):

ok wow, this indeed looks very similar to https://en.wikipedia.org/wiki/Cylindrical_algebraic_decomposition . I see an important difference: most of the pain we have is that we can't find a nice decomposition into cells that are mutually disjoint, becaues we can only represent (topologically) closed cells. In other words we don't have negation.

Reid Barton (Jun 04 2021 at 17:17):

Suppose you could find a collection of hyperplanes such that, when we form all the cells they define as described in your last paragraph, the following two properties hold:
(a) $Y$ is (provably/by definition) a union of some of those cells.
(b) The intersection of $S(Y)$ with one of those cells is again one of those cells (or empty).
Is that enough?

Jacques Carette (Jun 04 2021 at 17:20):

CAD doesn't quite have negation either, but because it has inequalities, it has trichotomy. So that gives you a positive description of everything. So you get a complete 'cellular' decomposition of space. All 3 of the domains that I mentioned have enormous literature, and I'm not an expert in any of them (so I don't really know the modern introductions).

Reid Barton (Jun 04 2021 at 17:23):

I think then the equations of part (b) must be provable. Because say $Y = \bigcup_i c_i$ and we know that $S(Y) \cap a = b$ for some cells $a$ and $b$. The equation $c_i \cap a = c_i \cap b$ is provable because both sides are polyhedra. So we just need to prove that $(\bigcup_i c_i) \cap b = b$, that is, $b \subset \bigcup_i c_i$. I want to try to arrange this by making $b$ one of the $c_i$.

Reid Barton (Jun 04 2021 at 17:25):

Or at least, $b$ should be a subset (a face) of one of the $c_i$, and I think that's automatic from the way the "cells" were defined.

Reid Barton (Jun 04 2021 at 17:28):

Now if $X$ is a polyhedron then to prove that $X \subset Y$ we can prove that $X \cap a \subset Y \cap a$ for all $a$. And we know we can provably rewrite $Y \cap a$ to a polyhedron (another cell), so now we are left with a true inclusion between polyhedra and it is provable. Does that seem right so far? So the key is to arrange for (b) above to be satisfied.

Jacques Carette (Jun 04 2021 at 17:28):

But here is nevertheless an attempt:

• for linear programming and polyhedra https://sites.math.washington.edu/~raymonda/linprog.pdf
• for abstract interpretation and polyhedra http://elina.ethz.ch/papers/POPL17-Polyhedra.pdf (that's a really good paper!)
• for CAD, a nice entry point is Manuel Kauers's practical guide followed by James Davenport's slides.
• related to CAD is Regular Chains that have quite a bit of software support.

Guillaume Boisseau (Jun 04 2021 at 17:35):

Reid Barton said:

Suppose you could find a collection of hyperplanes such that, when we form all the cells they define as described in your last paragraph, the following two properties hold:
(a) $Y$ is (provably/by definition) a union of some of those cells.
(b) The intersection of $S(Y)$ with one of those cells is again one of those cells (or empty).
Is that enough?

We already have a way to do this, but I don't think this is enough. I think it's enough if we add the following extra assumption: for three cells a, b and c, $a \subset b \cup c \implies a \subset b \lor a \subset c$

Guillaume Boisseau (Jun 04 2021 at 17:37):

Reid Barton said:

Now if $X$ is a polyhedron then to prove that $X \subset Y$ we can prove that $X \cap a \subset Y \cap a$ for all $a$. And we know we can provably rewrite $Y \cap a$ to a polyhedron (another cell), so now we are left with a true inclusion between polyhedra and it is provable. Does that seem right so far? So the key is to arrange for (b) above to be satisfied.

yeah absolutely! That's where I'm stuck too

Reid Barton (Jun 04 2021 at 17:39):

Guillaume Boisseau said:

Reid Barton said:

Suppose you could find a collection of hyperplanes such that, when we form all the cells they define as described in your last paragraph, the following two properties hold:
(a) $Y$ is (provably/by definition) a union of some of those cells.
(b) The intersection of $S(Y)$ with one of those cells is again one of those cells (or empty).
Is that enough?

We already have a way to do this, but I don't think this is enough. I think it's enough if we add the following extra assumption: for three cells a, b and c, $a \subset b \cup c \implies a \subset b \lor a \subset c$

If "cell" means any subset formed by, for each of the chosen hyperplanes $H$, selecting one of $\{H \ge 0\}$, $\{H = 0\}$, $\{H \le 0\}$, and intersecting all of these, I think this is automatic. Or at least I can't think of a counterexample.

Reid Barton (Jun 04 2021 at 17:40):

The problem I know about is that the intersection of $Y$ with a cell might not be a single cell.

John Baez (Jun 04 2021 at 17:41):

Which kinds of people use CAD?

I assume it has nothing to do with CAD/CAM, though it could. :upside_down:

Reid Barton (Jun 04 2021 at 17:42):

So I wanted to suggest a partial solution to (b). Suppose $Y$ is bounded. Enclose it in a big box, and write the box as a simplicial complex in such a way that $Y$ form a subcomplex. If we take all the hyperplanes that make up the faces of the simplices of this complex, it's not good enough to achieve (b), as the example with two segments joined at an endpoint shows. Instead, form the barycentric subdivision of this complex--I claim that that one works.

Reid Barton (Jun 04 2021 at 17:43):

The point is that if $K$ is a simplicial complex, then a subcomplex $Y$ of $K$ could meet a simplex of $K$ in some arbitrary union of faces. But the subdivision of $Y$ can only meet a simplex of the subdivision of $K$ in very specific ways; in particular, in a single face or not at all.

Guillaume Boisseau (Jun 04 2021 at 17:43):

Reid Barton said:

The problem I know about is that the intersection of $Y$ with a cell might not be a single cell.

That's kind of the same question I think: since $Y$ is a union of cells, so is $Y \cap c$. Then I'm hoping that to prove $d \subset Y \cap c$ I can always find that one of the cells of $Y \cap c$ contains $d$

Reid Barton (Jun 04 2021 at 17:46):

Oh I see. Maybe this is easier. Isn't this true (provided we fix a single choice of hyperplanes, and thus a notion of "cell", for both $X$ and $Y$)?

Guillaume Boisseau (Jun 04 2021 at 17:46):

Reid Barton said:

The point is that if $K$ is a simplicial complex, then a subcomplex $Y$ of $K$ could meet a simplex of $K$ in some arbitrary union of faces. But the subdivision of $Y$ can only meet a simplex of the subdivision of $K$ in very specific ways; in particular, in a single face or not at all.

I think we already have a property like that for our subdivision into cells, since an intersection of cells is always a cell. Does the simplicial stuff help more?

Guillaume Boisseau (Jun 04 2021 at 17:47):

Reid Barton said:

Oh I see. Maybe this is easier. Isn't this true (provided we fix a single choice of hyperplanes, and thus a notion of "cell", for both $X$ and $Y$)?

Yeah, I'm pretty sure this is true. Just unclear how to prove it, and I'm losing track of what needs to be proven diagrammatically and what normally ><

Reid Barton (Jun 04 2021 at 17:48):

I was trying to arrange that the intersection $Y \cap c$ was not merely a union of cells, but actually a single cell.

Reid Barton (Jun 04 2021 at 17:49):

If $Y$ is the union of the nonnegative x and y axes, for example, then you can see from a picture that we need to include a hyperplane that cuts through the origin that isn't either of the axes.

Guillaume Boisseau (Jun 04 2021 at 17:49):

ah, well that's not the case in general, though I suspect it might be true in the convex case. Counter-example: choose $Y$ to be the union of the top-left and bottom-right quadrants of the plane. The two relevant hyperplanes are the two axes. Take $c$ to be the top-right quadrant, then $Y \cap c$ isn't a single cell

Guillaume Boisseau (Jun 04 2021 at 17:49):

hah, we had the same example in mind ^^

Reid Barton (Jun 04 2021 at 17:50):

But this is fixable by adding more hyperplanes, which is what the subdivision is for.

Guillaume Boisseau (Jun 04 2021 at 17:50):

ohh, now I understand a message of yours from a while ago

Guillaume Boisseau (Jun 04 2021 at 17:52):

hm, how would we do that? Is it enough to add separating hyperplanes between any two of the initial Y_i?

Guillaume Boisseau (Jun 04 2021 at 17:53):

no the $Y_i$ might have non-trivial intersection. So we start by doing the subdivision using all the hyperplanes of Y, and _then_ we add pairwise separating hyperplanes? Is that enough?

Robin Piedeleu (Jun 04 2021 at 17:55):

Pairwise, meaning for each pair of cells?

Guillaume Boisseau (Jun 04 2021 at 17:55):

yeah

Guillaume Boisseau (Jun 04 2021 at 17:55):

but I'm really hoping we don't need to go this way and that the initial subdivision is enough

Reid Barton (Jun 04 2021 at 17:57):

I think my whole scheme depended on the same hypothesis that the simpler approach you suggested does. Namely, if we fix some hyperplanes and use them to divide space into cells, then if one cell is contained in the union of some others, then it is already contained in one of the cells.

Guillaume Boisseau (Jun 04 2021 at 18:02):

nice

Guillaume Boisseau (Jun 04 2021 at 18:04):

well, I think all the pieces are here and we just need to put them together. I'm exhausted rn though, will try later

Guillaume Boisseau (Jun 04 2021 at 18:06):

ah, "a polyhedron is called a polytope if it is bounded". It sounds like our terminology is standard

Robin Piedeleu (Jun 04 2021 at 18:07):

Reid Barton said:

Namely, if we fix some hyperplanes and use them to divide space into cells, then if one cell is contained in the union of some others, then it is already contained in one of the cells.

Do you mean that for cells $a,b,c$ (built from the same set of hyperplanes), if $a\subseteq b \cup c$ then $a \subseteq b$ or $a\subseteq c$? I'm not convinced that's true. What I find more convincing is that there exists another cell built from the same collection of hyperplanes (not necessarily $b$ or $c$) that contains $a$. Is this what you meant? That would be enough for us, right?

Robin Piedeleu (Jun 04 2021 at 18:08):

Guillaume Boisseau said:

ah, "a polyhedron is called a polytope if it is bounded". It sounds like our terminology is standard

Yeah, I thought so too!

Reid Barton (Jun 04 2021 at 18:08):

I also haven't worked out all the details, but currently I believe some argument along the following lines should work:

• pick enough hyperplanes so that you can provably express each of $X$ and $Y$ as a union of cells with respect to those hyperplanes; this should just be "pick all the defining hyperplanes involved"
• since $X \subset Y$ is true, each cell of $X$ must be contained in a single cell of $Y$, which you can prove by your completeness result for polyhedra

Reid Barton (Jun 04 2021 at 18:12):

Robin Piedeleu said:

Reid Barton said:

Namely, if we fix some hyperplanes and use them to divide space into cells, then if one cell is contained in the union of some others, then it is already contained in one of the cells.

Do you mean that for cells $a,b,c$ (built from the same set of hyperplanes), if $a\subseteq b \cup c$ then $a \subseteq b$ or $a\subseteq c$? I'm not convinced that's true.

Yes, this is what I mean and I'm not 100% convinced it is true either.

What I find more convincing is that there exists another cell built from the same collection of hyperplanes (not necessarily $b$ or $c$) that contains $a$. Is this what you meant? That would be enough for us, right?

Only if it is contained in $Y$ as well.

Reid Barton (Jun 04 2021 at 18:13):

I think this works, though. The intersection of any two cells is a cell. If $a \subset b \cup c$ then also $a \subset (a \cap b) \cup (a \cap c)$, so we can assume that $b$ and $c$ are contained in $a$. Then if neither one equals $a$ then they both have lower dimension than $a$, and so their union cannot cover $a$.

Robin Piedeleu (Jun 04 2021 at 18:19):

Picture $a$ as a triangle (defined by three halfspaces) within a larger triangle (say three other halfspaces given by parallel hyperplanes to the first three). Cut the larger triangle in half with another hyperplane such that it also cuts $a$ into two, and call the two sides of the larger triangle $b$ and $c$ (a picture would be better here). Isn't this a counterexample to the first statement?

Reid Barton (Jun 04 2021 at 18:20):

If $a$ is cut in half then it isn't a cell.

Reid Barton (Jun 04 2021 at 18:20):

For me a cell means we have to specify $\ge 0$, $= 0$ or $\le 0$ for every chosen hyperplane.

Robin Piedeleu (Jun 04 2021 at 18:20):

Right

Robin Piedeleu (Jun 04 2021 at 18:21):

yes, that's true

Guillaume Boisseau (Jun 04 2021 at 18:22):

Robin Piedeleu said:

Reid Barton said:

Namely, if we fix some hyperplanes and use them to divide space into cells, then if one cell is contained in the union of some others, then it is already contained in one of the cells.

Do you mean that for cells $a,b,c$ (built from the same set of hyperplanes), if $a\subseteq b \cup c$ then $a \subseteq b$ or $a\subseteq c$? I'm not convinced that's true. What I find more convincing is that there exists another cell built from the same collection of hyperplanes (not necessarily $b$ or $c$) that contains $a$. Is this what you meant? That would be enough for us, right?

it would be enough, but I still believe the statement to be true

Guillaume Boisseau (Jun 04 2021 at 18:23):

@Reid Barton I'd be surprised that a dimension argument would work here. We can have nontrivial inclusions between polyhedra of the same dimension

Robin Piedeleu (Jun 04 2021 at 18:28):

Reid Barton said:

I think this works, though. The intersection of any two cells is a cell. If $a \subset b \cup c$ then also $a \subset (a \cap b) \cup (a \cap c)$, so we can assume that $b$ and $c$ are contained in $a$. Then if neither one equals $a$ then they both have lower dimension than $a$, and so their union cannot cover $a$.

To me, this seems to work.

Robin Piedeleu (Jun 04 2021 at 18:29):

You're not convinced @Guillaume Boisseau?

Guillaume Boisseau (Jun 04 2021 at 18:29):

No: cut a square along the diagonal, call the two triangles b and c.

Guillaume Boisseau (Jun 04 2021 at 18:30):

then $a \subset b \cup c$, yet $a$ is equal to neither

Robin Piedeleu (Jun 04 2021 at 18:30):

But $a$ is not a cell

Guillaume Boisseau (Jun 04 2021 at 18:30):

yeah but how do you use this fact in the proof?

Robin Piedeleu (Jun 04 2021 at 18:31):

I think this is where I was also confused earlier.

Guillaume Boisseau (Jun 04 2021 at 18:32):

Here's the proof I had in mind: define cells from a set of hyperplanes. Take Y a union of cells and c a cell such that $S(c) \subset S(Y)$. Wlog we can assume $Y \subset c$, as mentioned above. This means that if any hyperplanes are set to 0 in $c$, they are also set to 0 in all the cell of $Y$. So wlog we can ignore those. Now all hyperplanes in $c$ are set to $-$ or $+$. Wlog (up to negating some hyperplanes) we can assume they're all set to $+$. Now take a point $x$ in the interior of $c$. So $\forall i. H_i(x) > 0$. Now $x \in S(c) \subset S(Y) = \bigcup_j S(c_j)$. So there is a cell $c_j$ in $Y$ that contains $x$. Since $\forall i. H_i(x) > 0$, $c_j$ must have assigned $+$ to all hyperspaces, i.e. $c_j = c$, which is what we wanted.