Defining arbitrary join on the set of complete ideals of a Heyting Algebra
Solution 1:
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$.