<p>I’m going to use normal notation, as the square symbols are a pain to typeset.</p>
<blockquote>
<p><strong>Proposition:</strong> Let <span class="math-container">$L$</span> be a complete lattice, and <span class="math-container">$B$</span> its set of completely join-irreducible elements. If every element of <span class="math-container">$L$</span> is a join of a subset of <span class="math-container">$B$</span>, then the following are equivalent:</p>
<ol>
<li><p><span class="math-container">$\bigvee X\le\bigvee Y\implies \forall x\in X\,\exists y\in Y\,x\le y$</span> for all <span class="math-container">$X,Y\subseteq B$</span>.</p>
</li>
<li><p>All <span class="math-container">$x\in B$</span> are completely join-prime, i.e., <span class="math-container">$x\le\bigvee Y\implies\exists y\in Y\,x\le y$</span> for all <span class="math-container">$Y\subseteq L$</span>.</p>
</li>
<li><p><span class="math-container">$L$</span> satisfies the infinitary distributive law <span class="math-container">$x\land\bigvee_{i\in I}y_i=\bigvee_{i\in I}(x\land y_i)$</span>.</p>
</li>
</ol>
</blockquote>
<p>Note that condition 3 is not equivalent to its dual, and it is weaker than full complete distributivity.</p>
<p><strong>Proof:</strong></p>
<p>1 → 2: By the assumption on <span class="math-container">$L$</span>, <span class="math-container">$\bigvee Y=\bigvee\{u\in B:\exists y\in Y\,u\le y\}$</span>. Thus, if <span class="math-container">$x\le\bigvee Y$</span>, then <span class="math-container">$\bigvee\{x\}\le\bigvee\{u\in B:\exists y\in Y\,u\le y\}$</span>, hence by 1, there exists <span class="math-container">$u\in B$</span> and <span class="math-container">$y\in Y$</span> such that <span class="math-container">$x\le u\le y$</span>.</p>
<p>2 → 1: For any <span class="math-container">$x\in X$</span>, <span class="math-container">$x\le\bigvee X\le\bigvee Y$</span>, hence <span class="math-container">$x\le y$</span> for some <span class="math-container">$y\in Y$</span> as <span class="math-container">$x$</span> is completely join-prime.</p>
<p>3 → 2: If <span class="math-container">$x$</span> is completely join-irreducible and <span class="math-container">$x\le\bigvee Y$</span>, then <span class="math-container">$x=\bigvee\{x\land y:y\in Y\}$</span> by 3, hence <span class="math-container">$x=x\land y$</span> (i.e., <span class="math-container">$x\le y$</span>) for some <span class="math-container">$y\in Y$</span> by complete irreducibility.</p>
<p>2 → 3: <span class="math-container">$x\land\bigvee_{i\in I}y_i\ge\bigvee_{i\in I}(x\land y_i)$</span> always holds. For the other inequality, since the left-hand side is a join of a subset of <span class="math-container">$B$</span> by assumption, it suffices to show that
<span class="math-container">$$u\le x\land\bigvee_{i\in I}y_i\implies u\le\bigvee_{i\in I}(x\land y_i)$$</span>
for all <span class="math-container">$u\in B$</span>. The premise implies <span class="math-container">$u\le x$</span>, and since <span class="math-container">$u$</span> is completely join-prime by 2, there exists <span class="math-container">$i\in I$</span> such that <span class="math-container">$u\le y_i$</span>. Then <span class="math-container">$u\le x\land y_i\le\bigvee_{i\in I}(x\land y_i)$</span>.</p>

CC BY-SA 4.0
2020-05-18T19:06:41.117Z
Thanks! You've completely answered my point
Denis Mazzucato
CC BY-SA 4.0
2020-05-18T15:00:08.340Z
2020-05-18T15:00:08.340Z
2020-06-17T09:38:08.363Z
Emil Jeřábek
<p>Given a complete lattice <span class="math-container">$(L, \sqsubseteq)$</span> and a basis of completely <span class="math-container">$\sqcup$</span>-irreducibles <span class="math-container">$B_L \subseteq L$</span>, such that <span class="math-container">$\forall l \in L$</span>, <span class="math-container">$l=\sqcup\{b \in B_L\ |\ b \sqsubseteq l\}$</span>.</p>

<p>I mean:</p>

<ul>
<li><p><strong>Hoare preorder</strong> <span class="math-container">$(2^{B_L}, \sqsubseteq_H)$</span>, where for <span class="math-container">$X, Y \in 2^{B_L}$</span>, </p>

<p><span class="math-container">$X \sqsubseteq_H Y \iff \forall x \in X$</span>, <span class="math-container">$\exists y \in Y$</span> such that <span class="math-container">$x \sqsubseteq y$</span></p></li>
<li><p><strong>Supremum preorder</strong> <span class="math-container">$(2^{B_L}, \sqsubseteq_{\sqcup})$</span>, where for <span class="math-container">$X, Y \in 2^{B_L}$</span>, </p>

<p><span class="math-container">$X \sqsubseteq_{\sqcup} Y \iff \sqcup X \sqsubseteq \sqcup Y$</span></p></li>
</ul>

<p>Where <span class="math-container">$l \in L$</span> is completely <span class="math-container">$\sqcup$</span>-irreducibles <span class="math-container">$\iff \forall X' \subseteq L$</span> such that <span class="math-container">$l = \sqcup X' \implies l \in X'$</span> (note that <span class="math-container">$\bot$</span> isn't completely <span class="math-container">$\sqcup$</span>-irreducible since <span class="math-container">$\bot = \sqcup \emptyset$</span> but <span class="math-container">$\bot \not\in \emptyset$</span>).</p>

<p>I'm pretty sure that "Hoare" is the right name for the intended preorder, a little less about "Supremum" (maybe "Smyth" could be better).</p>

<p>My question is, given a distributive lattice <span class="math-container">$L$</span>, how to prove that Hoare preorder and Supremum preorder coincide?
It is easy to see that in general (without distributivity) <span class="math-container">$X \sqsubseteq_H Y \implies X \sqsubseteq_{\sqcup} Y$</span>. But I'm stuck in the converse implication <span class="math-container">$X \sqsubseteq_{\sqcup} Y \implies X \sqsubseteq_H Y$</span>, that probably uses distributivity of <span class="math-container">$L$</span>.</p>

<p>Where <span class="math-container">$L$</span> is distributive <span class="math-container">$\iff \forall a, b, c \in L$</span> it holds that <span class="math-container">$a \sqcap (b \sqcup c) = (a \sqcap b) \sqcup (a \sqcap c)$</span>. By the way, I'm still not sure if I need to require <span class="math-container">$L$</span> to be only distributive or completely distributive.</p>

<p>Thanks in advance for any hint.</p>

CC BY-SA 4.0
2020-05-17T10:03:44.423Z
I may be missing something, but the way you defined it, it’s just false: if $c=a\sqcup b$ where $a,b\in L$ are incomparable, then $\{c\}\sqsubseteq_{\sqcup}\{a,b\}$, but $\{c\}\not\sqsubseteq_H\{a,b\}$. Also, is $S=L$?
Emil Jeřábek
CC BY-SA 4.0
2020-05-17T12:13:05.370Z
An instance that fails in *every* complete lattice is $\{\bot\}\sqsubseteq_\sqcup\varnothing$, $\{\bot\}\not\sqsubseteq_H\varnothing$, where $\bot=\bigsqcup\varnothing$ is the least element of $L$.
Emil Jeřábek
CC BY-SA 4.0
2020-05-17T12:50:28.353Z
Thanks, you're right. I miss some hypothesis in the preamble of my statement. I'm going to edit my question, the point is that the two cases are both avoided using the powerset of a basis of irreducibles instead of $2^S$. Thus, $\{c\}$ nor $\{\bot\}$ could not be chosen since $c$ and $\bot$ aren't irreducibles (hence $c \not\in B_L$ and $\bot \not\in B_L$). @EmilJeřábek
Denis Mazzucato
CC BY-SA 4.0
2020-05-18T10:18:41.540Z
You apply $\bigsqcup X$ liberally to arbitrary sets $X$. Does it mean that you assume $L$ to be a *complete* lattice? Likewise, your definition of irreducible elements are actually *completely irreducible*, unless you restrict $X'$ to be finite. Is this intended?
Emil Jeřábek
CC BY-SA 4.0
2020-05-18T10:24:35.140Z
Also, what do you mean by a *basis*?
Emil Jeřábek
CC BY-SA 4.0
2020-05-18T10:37:45.357Z
Yep, I intended to be in a complete lattice L and to use completely join irreducible elements, I edited the question because I need to work also with transfinite height lattices.
Denis Mazzucato
CC BY-SA 4.0
2020-05-18T10:39:46.247Z
I've also added the basis definition. By the way, I'm pretty sure that I don't need to require $L$ to be completely distributive but only distributive. I'm going to add also this definition to the question
Denis Mazzucato
<fl.formal-languages><partial-order><order-theory><lattice>
How to prove that Supremum preorder coincides with Hoare preorder?
Denis Mazzucato
# How to prove that Supremum preorder coincides with Hoare preorder?

(Asked by: username_0 on 2020-05-17)

Given a complete lattice $(L, \sqsubseteq)$ and a basis of completely $\sqcup$-irreducibles $B\_L \subseteq L$, such that $\forall l \in L$, $l=\sqcup\{b \in B\_L\ |\ b \sqsubseteq l\}$.

I mean:

* **Hoare preorder** $(2^{B\_L}, \sqsubseteq\_H)$, where for $X, Y \in 2^{B\_L}$,

  $X \sqsubseteq\_H Y \iff \forall x \in X$, $\exists y \in Y$ such that $x \sqsubseteq y$
* **Supremum preorder** $(2^{B\_L}, \sqsubseteq\_{\sqcup})$, where for $X, Y \in 2^{B\_L}$,

  $X \sqsubseteq\_{\sqcup} Y \iff \sqcup X \sqsubseteq \sqcup Y$

Where $l \in L$ is completely $\sqcup$-irreducibles $\iff \forall X' \subseteq L$ such that $l = \sqcup X' \implies l \in X'$ (note that $\bot$ isn't completely $\sqcup$-irreducible since $\bot = \sqcup \emptyset$ but $\bot \not\in \emptyset$).

I'm pretty sure that "Hoare" is the right name for the intended preorder, a little less about "Supremum" (maybe "Smyth" could be better).

My question is, given a distributive lattice $L$, how to prove that Hoare preorder and Supremum preorder coincide?
It is easy to see that in general (without distributivity) $X \sqsubseteq\_H Y \implies X \sqsubseteq\_{\sqcup} Y$. But I'm stuck in the converse implication $X \sqsubseteq\_{\sqcup} Y \implies X \sqsubseteq\_H Y$, that probably uses distributivity of $L$.

Where $L$ is distributive $\iff \forall a, b, c \in L$ it holds that $a \sqcap (b \sqcup c) = (a \sqcap b) \sqcup (a \sqcap c)$. By the way, I'm still not sure if I need to require $L$ to be only distributive or completely distributive.

Thanks in advance for any hint.

**Tags:** fl.formal-languages, partial-order, order-theory, lattice
> **Comments:**
> **username_1**: I may be missing something, but the way you defined it, it’s just false: if $c=a\sqcup b$ where $a,b\in L$ are incomparable, then $\{c\}\sqsubseteq_{\sqcup}\{a,b\}$, but $\{c\}\not\sqsubseteq_H\{a,b\}$. Also, is $S=L$?  
> **username_1**: An instance that fails in *every* complete lattice is $\{\bot\}\sqsubseteq_\sqcup\varnothing$, $\{\bot\}\not\sqsubseteq_H\varnothing$, where $\bot=\bigsqcup\varnothing$ is the least element of $L$.  
> **username_0**: Thanks, you're right. I miss some hypothesis in the preamble of my statement. I'm going to edit my question, the point is that the two cases are both avoided using the powerset of a basis of irreducibles instead of $2^S$. Thus, $\{c\}$ nor $\{\bot\}$ could not be chosen since $c$ and $\bot$ aren't irreducibles (hence $c \not\in B_L$ and $\bot \not\in B_L$). @EmilJeřábek  
> **username_1**: You apply $\bigsqcup X$ liberally to arbitrary sets $X$. Does it mean that you assume $L$ to be a *complete* lattice? Likewise, your definition of irreducible elements are actually *completely irreducible*, unless you restrict $X'$ to be finite. Is this intended?  
> **username_1**: Also, what do you mean by a *basis*?  
> **username_0**: Yep, I intended to be in a complete lattice L and to use completely join irreducible elements, I edited the question because I need to work also with transfinite height lattices.  
> **username_0**: I've also added the basis definition. By the way, I'm pretty sure that I don't need to require $L$ to be completely distributive but only distributive. I'm going to add also this definition to the question  

---

## 1 answers

### Answer by username_1 on 2020-05-18. Score: 0 | Accepted answer

I’m going to use normal notation, as the square symbols are a pain to typeset.

> **Proposition:** Let $L$ be a complete lattice, and $B$ its set of completely join-irreducible elements. If every element of $L$ is a join of a subset of $B$, then the following are equivalent:
>
> 1. $\bigvee X\le\bigvee Y\implies \forall x\in X\,\exists y\in Y\,x\le y$ for all $X,Y\subseteq B$.
> 2. All $x\in B$ are completely join-prime, i.e., $x\le\bigvee Y\implies\exists y\in Y\,x\le y$ for all $Y\subseteq L$.
> 3. $L$ satisfies the infinitary distributive law $x\land\bigvee\_{i\in I}y\_i=\bigvee\_{i\in I}(x\land y\_i)$.

Note that condition 3 is not equivalent to its dual, and it is weaker than full complete distributivity.

**Proof:**

1 → 2: By the assumption on $L$, $\bigvee Y=\bigvee\{u\in B:\exists y\in Y\,u\le y\}$. Thus, if $x\le\bigvee Y$, then $\bigvee\{x\}\le\bigvee\{u\in B:\exists y\in Y\,u\le y\}$, hence by 1, there exists $u\in B$ and $y\in Y$ such that $x\le u\le y$.

2 → 1: For any $x\in X$, $x\le\bigvee X\le\bigvee Y$, hence $x\le y$ for some $y\in Y$ as $x$ is completely join-prime.

3 → 2: If $x$ is completely join-irreducible and $x\le\bigvee Y$, then $x=\bigvee\{x\land y:y\in Y\}$ by 3, hence $x=x\land y$ (i.e., $x\le y$) for some $y\in Y$ by complete irreducibility.

2 → 3: $x\land\bigvee\_{i\in I}y\_i\ge\bigvee\_{i\in I}(x\land y\_i)$ always holds. For the other inequality, since the left-hand side is a join of a subset of $B$ by assumption, it suffices to show that
$$u\le x\land\bigvee\_{i\in I}y\_i\implies u\le\bigvee\_{i\in I}(x\land y\_i)$$
for all $u\in B$. The premise implies $u\le x$, and since $u$ is completely join-prime by 2, there exists $i\in I$ such that $u\le y\_i$. Then $u\le x\land y\_i\le\bigvee\_{i\in I}(x\land y\_i)$.

> **Comments:**
> **username_0**: Thanks! You've completely answered my point  

---

