Lecture 57 - Chapter 4: Feasibility Relations

John Baez · July 2018

Let's look at some examples of feasibility relations!

Feasibility relations work between preorders, but for simplicity suppose we have two posets $X$ and $Y$. We can draw them using Hasse diagrams:

Here an arrow means that one element is less than or equal to another: for example, the arrow $S \to W$ means that $S \le W$. But we don't bother to draw all possible inequalities as arrows, just the bare minimum. For example, obviously $S \le S$ by reflexivity, but we don't bother to draw arrows from each element to itself. Also $S \le N$ follows from $S \le E$ and $E \le N$ by transitivity, but we don't bother to draw arrows that follow from others using transitivity. This reduces clutter.

(Usually in a Hasse diagram we draw bigger elements near the top, but notice that $e \in Y$ is not bigger than the other elements of $Y$. In fact it's neither $\ge$ or $\le$ any other elements of $Y$ - it's just floating in space all by itself. That's perfectly allowed in a poset.)

Now, we saw that a feasibility relation from $X$ to $Y$ is a special sort of relation from $X$ to $Y$. We can think of a relation from $X$ to $Y$ as a function $\Phi$ for which $\Phi(x,y)$ is either $\text{true}$ or $\text{false}$ for each pair of elements $ x \in X, y \in Y$. Then a feasibility relation is a relation such that:

If $\Phi(x,y) = \text{true}$ and $x' \le x$ then $\Phi(x',y) = \text{true}$.
If $\Phi(x,y) = \text{true}$ and $y \le y'$ then $\Phi(x,y') = \text{true}$.

Fong and Spivak have a cute trick for drawing feasibility relations: when they draw a blue dashed arrow from $x \in X$ to $y \in Y$ it means $\Phi(x,y) = \text{true}$. But again, they leave out blue dashed arrows that would follow from rules 1 and 2, to reduce clutter!

Let's do an example:

So, we see $\Phi(E,b) = \text{true}$. But we can use the two rules to draw further conclusions from this:

Since $\Phi(E,b) = \text{true}$ and $S \le E$ then $\Phi(S,b) = \text{true}$, by rule 1.
Since $\Phi(S,b) = \text{true}$ and $b \le d$ then $\Phi(S,d) = \text{true}$, by rule 2.

and so on.

Puzzle 171. Is $\Phi(E,c) = \text{true}$ ?

Puzzle 172. Is $\Phi(E,e) = \text{true}$?

I hope you get the idea! We can think of the arrows in our Hasse diagrams as one-way streets going between cities in two countries, $X$ and $Y$. And we can think of the blue dashed arrows as one-way plane flights from cities in $X$ to cities in $Y$. Then $\Phi(x,y) = \text{true}$ if we can get from $x \in X$ to $y \in Y$ using any combination of streets and plane flights!

That's one reason $\Phi$ is called a feasibility relation.

What's cool is that rules 1 and 2 can also be expressed by saying

$$ \Phi : X^{\text{op}} \times Y \to \mathbf{Bool} $$ is a monotone function. And it's especially cool that we need the '$\text{op}$' over the $X$. Make sure you understand that: the $\text{op}$ over the $X$ but not the $Y$ is why we can drive to an airport in $X$, then take a plane, then drive from an airport in $Y$.

Here are some ways to lots of feasibility relations. Suppose $X$ and $Y$ are preorders.

Puzzle 173. Suppose $f : X \to Y $ is a monotone function from $X$ to $Y$. Prove that there is a feasibility relation $\Phi$ from $X$ to $Y$ given by

$$ \Phi(x,y) \text{ if and only if } f(x) \le y .$$ Puzzle 174. Suppose $g: Y \to X $ is a monotone function from $Y$ to $X$. Prove that there is a feasibility relation $\Psi$ from $X$ to $Y$ given by

$$ \Psi(x,y) \text{ if and only if } x \le g(y) .$$ Puzzle 175. Suppose $f : X \to Y$ and $g : Y \to X$ are monotone functions, and use them to build feasibility relations $\Phi$ and $\Psi$ as in the previous two puzzles. When is

$$ \Phi = \Psi ? $$ To read other lectures go here.

MatthewDoty · July 2018

Puzzle 171. Is $\Phi(E,c) = \text{true}$ ?

No (if I am reading the diagram correctly)

Puzzle 172. Is $\Phi(E,e) = \text{true}$?

Yes

We have $E \leq N$ so $\Phi(N,e) \leq \Phi(E,e)$. Since the diagram indicates $\Phi(N,e)=\text{true}$ then we know $\Phi(E,e) = \text{true}$.

Puzzle 175. Suppose $f : X \to Y$ and $g : Y \to X$ are monotone functions, and use them to build feasibility relations $\Phi$ and $\Psi$ as in the previous two puzzles. When is
$$ \Phi = \Psi ? $$

When $f$ and $g$ are adjoints, that is to say $f \dashv g$

Michael Hong · July 2018

Puzzle 173

If we let $y = f(x')$ then $f(x) \leq y$ sets up the following inequalities by definition of a monotone function :

$$x \leq x' \;\text{and}\; f(x) \leq f(x')$$ By definition of a feasibility relation the above inequality implies :

$$\Phi(x,f(x)) \;\text{implies}\; \Phi(x',f(x'))$$ So...

$$\text{If} \; \Phi(x,f(x)) = \text{true and} \; f(x) \leq y, \text{then} \; \Phi(x,y) = \text{true}$$ Puzzle 174

Similarly,

$$\text{If} \; \Psi(g(y),y) = \text{true and} \; x \leq g(y), \text{then} \; \Psi(x,y) = \text{true}$$

Christopher Upshaw · July 2018

Puzzle 174: Given $g : Y -> X$ and $\Psi(x,y) = x \le g(y)$, we must show that $\Psi$ is a feasibility relation. $ \Psi $ is a feasibility relation if and only if \[\forall x',x : X, y,y' : Y, x'\le x, y \le y', \Psi(x,y) \to \Psi(x',y')\] $\Psi(x,y)$ equals, by the definition of Psi: \[x \le g(y)\] By transitivity and $x\le x'$: \[x'\le g(y)\] By monotonicity we have \[y\le y' \to g(y)\le g(y')\] and so \[\to x'\le g(y')\] which by definition of $\Psi$, equals $\Psi(x',y')$ Therefor, \[\Psi(x,y) \to \Psi(x',y')\] QED.

Anindya Bhattacharyya · July 2018

@Matthew – I agree with your answers to 172 and 175 but surely we do have $\Phi(E,c) = \text{true}$ because we can "drive" from $E$ to $N$ and then "fly" from $N$ to $c$.

MatthewDoty · July 2018

Anindya wrote

surely we do have $\Phi(E,c) = \text{true}$ because we can "drive" from $E$ to $N$ and then "fly" from $N$ to $c$.

Yeah, you are right. I read the diagram incorrectly... thanks!

Keith E. Peterson · July 2018

Anindya Bhattacharyya wrote:

@Matthew – I agree with your answers to 172 and 175 but surely we do have $\Phi(E,c) = \text{true}$ because we can "drive" from $E$ to $N$ and then "fly" from $N$ to $c$.

Yeah, I was thinking the same thing.

Simon Willerton · July 2018

In some sense, in the pictures it would be more sensible to put $Y$ on top of $X$. One can think (sometimes usefully, sometimes less usefully) of a feasability relation (or profunctor) between preorders as giving rise to a new preorder, known as the collage. The underlying set of the collage is the disjoint union $X \sqcup Y$ and on both $X$ and $Y$ the new preorder restricts to the preorders you started with, but for all $x \in X$ and $y \in Y$ you have $y\not\le x$ whilst $x\le y\, \iff\ \Phi(x,y)$.

The pictures drawn with the blue arrows are the Hasse diagrams of these collages. Nothing in $Y$ ever comes before anything in $X$ in this preorder, so that's why it would make sense to draw $Y$ on top of $X$. I'll leave it for someone to produce such a version of the examples above :-).

John Baez · July 2018

Puzzle 171. Yes, $\Phi(E,c) = \text{true}$ because we can first walk from $E$ to $N$ and then fly from $N$ to $c$. I hadn't noticed this when creating this puzzle! Like Matthew, I thought the answer was $\text{false}$.

Puzzle 172. Yes, $\Phi(E,e) = \text{true}$ because we can first walk from $E$ to $N$ and then fly from $N$ to $e$.

I should have given an example that was a bit different, like $\Phi(S,d)$.

John Baez · July 2018

Michael wrote:

Puzzle 173. If we let $y = f(x')$ then $f(x) \leq y$ sets up the following inequalities by definition of a monotone function :
$$x \leq x' \;\text{and}\; f(x) \leq f(x')$$ By definition of a feasibility relation the above inequality implies : $$\Phi(x,f(x)) \;\text{implies}\; \Phi(x',f(x'))$$ So... $$\text{If} \; \Phi(x,f(x)) = \text{true and} \; f(x) \leq y, \text{then} \; \Phi(x,y) = \text{true}$$

I have trouble following what you're doing here. The question asks you to assume $\Phi$ is defined by

$$ \Phi(x,y) \text{ if and only if } f(x) \le y .$$ where $f$ is monotone, and prove that $\Phi$ is a feasibility relation.

So, it makes me very nervous when you say "by the definition of a feasibility relation the above inequality implies...." That sounds like you are assuming $\Phi$ is a feasibility relation and deducing things from this. But this is what you're trying to prove.

It's quite possible you have a good idea and I'm getting stumped by the way you're explaining it. Here's how a mathematician would start an answer to this puzzle:

Assume $f : X \to Y$ is monotone and define $\Phi$ by
$$ \Phi(x,y) \text{ if and only if } f(x) \le y .$$ We want to prove $\Phi$ is a feasibility relation. So, it suffices to show

If $\Phi(x,y) = \text{true}$ and $x' \le x$ then $\Phi(x',y) = \text{true}$.

If $\Phi(x,y) = \text{true}$ and $y \le y'$ then $\Phi(x,y') = \text{true}$.

In other words: state what you're assuming and what you're trying to show. Then use the assumptions to get what you're trying to show.

Another fine approach starts with the original definition of feasibility relation:

Assume $f : X \to Y$ is monotone and define $\Phi$ by
$$ \Phi(x,y) \text{ if and only if } f(x) \le y .$$ We want to prove $\Phi$ is a feasibility relation. So, it suffices to show that if $\Phi(x,y) = \text{true}$ and $x' \le x$ and $y \le y'$, then $\Phi(x',y') = \text{true}$.

John Baez · July 2018

Simon wrote:

One can think (sometimes usefully, sometimes less usefully) of a feasability relation (or profunctor) between preorders as giving rise to a new preorder, known as the collage. The underlying set of the collage is the disjoint union $X \sqcup Y$ and on both $X$ and $Y$ the new preorder restricts to the preorders you started with, but for all $x \in X$ and $y \in Y$ you have $y\not\le x$ whilst $x\le y\, \iff\ \Phi(x,y)$.

I think it's really great how one can glom together two preorders into a "collage" this way using a feasibility relation... or more generally, glom together two categories using profunctor. But the preorder case is so easy to visualize and like!

I got interested in collages when thinking about the 10-fold way in condensed matter physics. I noticed that it arose from taking the 2-element super-Brauer group of the complex numbers and the 8-element super-Brauer group of the real numbers and glomming them into a single structure. It's easy to check that a field homomorphism like $\mathbb{R} \hookrightarrow \mathbb{C}$ gives rise to a homomorphism between their super-Brauer groups (whatever those are). But how do you combine the Brauer groups into a single thing?

Well, if you have a group homomorphism $f : G \to H$ you can a make the disjoint union $G \sqcup H$ into a monoid in a pretty obvious way. This is not quite the collage of the underlying categories of these groups, since it has one object rather than two. But it's related.

Christopher Upshaw · July 2018

Then taking that behavior and extending it over the superposition* of graphs, should give a decent idea of supposition of one category (groupoid) over another. Which like a non disjoint union in type theory requires specifying the overlap.

Superposition in the general sense, that is metaphorically physically overlaying one thing on top of another thing.

Michael Hong · July 2018

John

Thanks for getting my head back on LOL. Indeed I have trouble knowing what to assume and where exactly I need to end up. Christopher has a nice answer for Puzzle 174 so I will write out Puzzle 173 to practice (hopefully correctly).

Assume $f : X \to Y$ is monotone and define $\Phi$ by
$$ \Phi(x,y) \text{ if and only if } f(x) \le y .$$ We want to prove $\Phi$ is a feasibility relation. So, it suffices to show

If $\Phi(x,y) = \text{true}$ and $x' \le x$ then $\Phi(x',y) = \text{true}$.

If $\Phi(x,y) = \text{true}$ and $y \le y'$ then $\Phi(x,y') = \text{true}$.

So we have at our dispense: $$\Phi(x,y) \text{ if and only if } f(x) \le y $$ $$x' \leq x \;\text{and}\; f(x') \leq f(x)$$ $$y \le y'$$ And we have to show $$\Phi(x',y') = \text{true}$$ Here we go: $$\Phi(x,y) = f(x) \le y $$ $$\rightarrow f(x) \le y' \text{ since } y \le y'$$ $$\rightarrow f(x') \le y' \text{ since } x' \leq x \;\text{and}\; f(x') \leq f(x)$$ $$\Phi(x',y') \text{ by definition of } \Phi $$

John Baez · July 2018

Michael - yes, that's good! Great!

You would need some feedback, and practice to learn how to write up proofs the way mathematicians do. This is math grad students spend so much time doing homeworks full of proofs, and I spend so much time grading these, writing comments in the margin, and showing all the students the 'best' proofs, so they can learn what good examples are like.

However, you didn't sign up for math grad school, and I'm not being paid to teach this course, so I won't correct the style of your proof. I will just say: you've got the idea right. :)>-

MatthewDoty · July 2018

Hey Michael,

To follow up on what John Baez said:

You would need some feedback, and practice to learn how to write up proofs the way mathematicians do. This is math grad students spend so much time doing homeworks full of proofs, and I spend so much time grading these, writing comments in the margin, and showing all the students the 'best' proofs, so they can learn what good examples are like.

I've seen some free MOOCs where students grade one another. In this forum, I know I make my fair share of mistakes. Other students kindly point them out, so I have had a lot of chance to improve.

John gave you a head start on the proof of the puzzle:

Assume $f : X \to Y$ is monotone and define $\Phi$ by
$$ \Phi(x,y) \text{ if and only if } f(x) \le y .$$ We want to prove $\Phi$ is a feasibility relation. So, it suffices to show

If $\Phi(x,y) = \text{true}$ and $x' \le x$ then $\Phi(x',y) = \text{true}$.

If $\Phi(x,y) = \text{true}$ and $y \le y'$ then $\Phi(x,y') = \text{true}$.

Sadly, you can't just show $$\Phi(x',y') = \text{true}$$ You have to show (1) and (2).

So let's prove (1).

Proof. Assume (a) $\Phi(x,y) = \text{true}$ and (b) $x' \le x$. We must show $\Phi(x',y) = \text{true}$.

From (a), we know since $\Phi(x,y) \text{ if and only if } f(x) \le y$ that:

$$ f(x) \leq y \tag{c}$$ By (b) and the assumption that $f$ is monotone, we have

$$f(x') \le f(x) \tag{d}$$ From (c) and (d) we have by the transitivity of the preorder relation $\leq$

$$f(x') \le y $$ This, along with $\Phi(x,y) \text{ if and only if } f(x) \le y$, suffices to show $\Phi(x',y) = \text{true}$ as desired.

There are many styles of proof.

TLA+ is a computer proof system. It has been used to analyze software systems at Amazon looking for bugs. The author of TLA+, Leslie Lamport, has some opinions about how proofs should be written. You can read them in How to Write a 21st Century Proof.

I have done a lot of computer proofs. They are in my opinion, mechanical and boring. But, you can get really good at writing technically correct proofs, since you have the computer to check you.

But I think proofs are like artwork. If you want to read beautiful proofs, I recommend Proofs from THE BOOK (2013) by Aigner, Ziegler and Hofmann.

I suspect John Baez feels the same, perhaps he will stop by and make some reading suggestions...

John Baez · July 2018

Matthew - I thought Michael was taking a different approach than the one I suggested: proving that $\Phi(x',y') = \text{true}$ if $\Phi(x,y) = \text{true}$, $x' \le x$ and $y \le y'$. This uses the 'original' definition of enriched profunctor, which I expanded to a lengthier definition in the theorem in Lecture 56.

Of course, if this is what Michael was doing, it counts as bad style not to mention it!

Basically, if a smart mathematician who knows the subject matter doesn't understand your proof, there's probably a way to improve the proof.

MatthewDoty · July 2018

I thought Michael was taking a different approach than the one I suggested: proving that $\Phi(x',y') = \text{true}$ if $\Phi(x,y) = \text{true}$, $x' \le x$ and $y \le y'$. This uses the 'original' definition of enriched profunctor, which I expanded to a lengthier definition in the theorem in Lecture 56.

Ah, sure I see that we can say $\Phi$ is a feasibility relation if it obeys the axiom:

$$ x' \le x \text{ and } y \le y' \text{ and } \Phi(x,y) \text{ implies } \Phi(x',y') $$ Michael's proof certainly works, I was just thrown off because I had assumed he was going to prove parts (1) and (2) like you outlined. My mistake!

John Baez · July 2018

... but also his mistake, because he make it sound like he was going to do X, and then he did Y.

Ideally, a proof is an attempt at extremely clear communication. Most proofs don't live up to that standard, though!

Michael Hong · July 2018

John and Matthew

Wow thanks for the correction and tips! I am truly grateful!

Clearly I wasn't being clear in my communication and I think John is giving me the benefit of the doubt in that I knew what I was doing LOL. I was trying to figure out what to assume and what to prove but once I did, I apparently ended up skipping steps and went in a different direction! In my mind after reading Christopher's answer, I realized that you can do that in one step like John said in the end of his comment 9 and pretty much rewrote what Christopher did in terms of this puzzle while making sure I was only using the assumptions I made. Being a newby, I shouldn't have skipped steps and should have done what Matthew did... or at least clearly stated which direction I was going to take as John pointed out...

Thanks for the references Matthew. I will definitely try to read through and hopefully one day I can become fluent speaker of this beautiful language!

Julio Song · December 2018

I have two small questions:

1 - In the appealing flight analogy:

We can think of the arrows in our Hasse diagrams as one-way streets in two cities, $X$ and $Y$. And we can think of the blue dashed arrows as one-way plane flights from cities in $X$ to cities in $Y$. Then $\Phi(x,y) = \text{true}$ if we can get from $x \in X$ to $y \in Y$ using any combination of streets and plane flights!

Should "from cities in $X$ to cities in $Y$" be "from streets in $X$ to streets in $Y$" instead (as $X,Y$ are already cities themselves)?

2 - In Puzzle 174:

Puzzle 174. Suppose $g: Y \to X $ is a monotone function from $X$ to $Y$...

Should this be a function from $Y$ to $X$ instead?

John Baez · January 2019

Julio - I meant for $X$ and $Y$ to be countries, $x \in X$ to be a city in the country $X$, and $y \in Y$ to be a city in the country $Y$.

So, just one word in my description was wrong, and I'll fix it now. Thanks for catching it!

And yes, you're right about Puzzle 174, too.

Julio Song · January 2019

@John Cool, thanks for the clarification! :-)

By the way, is there any way to efficiently "@" members in this forum? Sometimes I miss replies targeted at me because I don't receive notifications and forget to follow up on all my comments... XD

Azimuth Forum

Howdy, Stranger!

Categories

Lecture 57 - Chapter 4: Feasibility Relations

Comments