Given a Heyting Algebra $H$ we define a complete ideal (or c-ideal) $I$ to be a subset of $H$ satisfying.
- $\bot \in I$
- $b \in I$ and $a \leq b$ implies $a \in I$
- $X \subseteq I$ and $\bigvee X$ exists in $H$ implies $\bigvee X \in I$.
Note $H$ is not necessarily complete so arbitrary joins do not neccesarily exist in $H$. A complete ideal generalizes the notion of an ideal from binary joins to arbitrary joins if they exist.
We can use c-ideals to complete the Heyting Algebra $H$. Let $H'$ be the set of c-ideals of $H$. Let $I_{\alpha}$ be a family of c-ideals where $\alpha \in \mathcal{J}$ some index set.
We define the meet in $H'$ to be the intersections of $I_{\alpha}$ that is $\underset{\alpha \in \mathcal{J}}{\bigwedge} I_{\alpha} = \underset{\alpha \in \mathcal{J}}{\bigcap} I_{\alpha}$. It is easy enough to show that the intersection of c-ideals is a c-ideal and it is in fact the meet. Unfortunately, the union of c-ideals is not, in general, a c-ideal. So for the join things are a bit more complicated. We define the join below
$$ \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha} = \{ \bigvee X \ | \ X \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \ \text{and} \ \bigvee X \ \text{exists in H} \}. $$
I am struggling to show that this object is even a c-ideal, in particular on showing 2. and 3. hold.
Attempt:
- $\emptyset \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ and $\bigvee \emptyset = \bot$ exists in $H$ so $\bot \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$
- Let $b \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$ and $a \leq b$. There exists $X \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ such that $\bigvee X = b$. We need to show that there exists $Y \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ such that $\bigvee Y = a$. Some candidates for $Y$ are $\downarrow a$, $X \cap \downarrow a$ and $\underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \cap \downarrow a$. The upside of $\downarrow a$ is that $\bigvee \downarrow a = a$ but there is no way to show $\downarrow a \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$. The upside of the latter two is that they obviously satisfy the subset requirement but there is no obvious way to show that there join is $a$.
- Let $Y \subseteq \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$ and $\bigvee Y$ exist in $H$. To show $\bigvee Y \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$ it suffices to show $Y \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$. Let $x \in Y$ then by assumption $x \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$. Thus for some $X \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ we have $x = \bigvee X$. Again I am stuck because we cannot say $x \in X$ and conclude $x \in \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$.
Reference: [1] A.S. Troelstra, D. Van Dalen. Constructivism in Mathematics An Introduction vol. 2.
Best Answer
Here is some insight for you.
Consider a partially ordered set $S$ which has all meets. We will prove that $S$ has all joins.
Let us consider some indexed collection $\{s_i \in S\}_{i \in I}$. Let $J = \{x \in S \mid \forall i \in I (s_i \leq x)\}$. I claim that $\bigwedge J$ is the join of $s$.
Indeed, we first note that for all $i$, for all $x \in J$, $s_i \leq x$ (by the very definition of $J$). Therefore, $s_i \leq \bigwedge J$.
Now suppose that for all $i \in I$, $s_i \leq x$. Then $x \in J$, so $\bigwedge J \leq x$. This completes the proof. $\square$
Your definition also works. Let's work through it.
First, we must show that $Q := \{ \bigvee X \mid X \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$ and $\bigvee X$ exists$\}$ is in fact a $c$-ideal.
As you have shown, (1) is trivial.
For (2), suppose that $X \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$ and $\bigvee X$ exists, and that $a \leq \bigvee X$. Then $a = a \land \bigvee X = \bigvee \{a \land x \mid x \in X\}$ (using the fact that $a \land$ is the left adjoint to $a \implies$ and therefore preserves any colimits that do exist). Since each $I_\alpha$ is downward closed, if $x \in I_\alpha$ then $a \land x \in I_\alpha$. And thus, we see that $\{a \land x \mid x \in X\} \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$. Thus, $a \in Q$.
For (3), we need to get a big cleverer if we wish to avoid choice. Given $a \in Q$, let $f(a) = \{w \in \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha \mid w \leq a\}$; then clearly, $a = \bigvee f(a)$.
Now suppose we have some family $\{x_k \in Q\}_{k \in K}$, and that $\bigvee\limits_{k \in K} x_k$ exists. Then in particular, we have $\bigvee\limits_{k \in K} x_k = \bigvee\limits_{k \in K} \bigvee f(x_k) = \bigvee \bigcup \limits_{k \in K} f(x_k)$. Note that $f(x_k) \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$ by definition, so $\bigcup \limits_{k \in K} f(x_k) \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$. Therefore, $\bigvee\limits_{k \in K} x_k = \bigvee \bigcup \limits_{k \in K} f(x_k) \in Q$.
Now, let's go about proving that $Q$ is in fact the join of the $I_\alpha$.
Clearly, we see that if $x \in I_\alpha$, then $x = \bigvee \{x\} \in Q$. So $I_\alpha \subseteq Q$ for all $\alpha$.
Now suppose that we had some $y$ such that for all $\alpha$, $I_\alpha \subseteq y$. Then condition 3 ensures that $Q \subseteq y$.