@John wrote:

> Suppose we have a poset \\(\mathcal{V}\\) with all joins, and a doubly indexed family of elements in \\(\mathcal{V}\\), say \\( \lbrace v_{a b} \rbrace_{a \in A, b \in B} \\) where \\(A\\) and \\(B\\) are arbitrary sets. Then

> \[ \bigvee_{a \in A} \bigvee_{b \in B} v_{ab} = \bigvee_{a \in A, b \in B} v_{ab} = \bigvee_{b \in B} \bigvee_{a \in A} v_{ab} \]

> It takes a bit of work to show this, but it seems so obvious I don't have the energy right now. All three are just different ways of thinking about the least upper bound of all the elements \\(v_{a b}\\).

Thinking about this further has led me to the conclusion that I'm overthinking it! I take your point that even if we were to index or structure our sets \\(A\\), \\(B\\), the _join_ would ignore that structure (since joins do not care about order or repetition).

Regarding proving the "obvious" identity, here's one reasonably slick way of doing it.

We write \\((\downarrow v)\\) for the subset \\(\\{ x \in \mathcal{V} : x \leq v\\}\\).

We can then write the definition of join as

\[ \bigvee S \leq v \iff S \subseteq (\downarrow v) \]

But this just states that \\(\bigvee\\) is left adjoint to \\(\downarrow\\) (treating them as monotone maps between \\(\mathcal{V}\\) and the poset of subsets of \\(\mathcal{V}\\)).

So \\(\bigvee\\) preserves joins, ie \\(\bigvee \bigcup \\{ S_i : i \in I \\} = \bigvee \\{ \bigvee S_i : i \in I \\}\\).

which is what we need to show that the join of all \\(v_{a b}\\) = the join of the joins of its rows = the join of the joins of its columns.

> Suppose we have a poset \\(\mathcal{V}\\) with all joins, and a doubly indexed family of elements in \\(\mathcal{V}\\), say \\( \lbrace v_{a b} \rbrace_{a \in A, b \in B} \\) where \\(A\\) and \\(B\\) are arbitrary sets. Then

> \[ \bigvee_{a \in A} \bigvee_{b \in B} v_{ab} = \bigvee_{a \in A, b \in B} v_{ab} = \bigvee_{b \in B} \bigvee_{a \in A} v_{ab} \]

> It takes a bit of work to show this, but it seems so obvious I don't have the energy right now. All three are just different ways of thinking about the least upper bound of all the elements \\(v_{a b}\\).

Thinking about this further has led me to the conclusion that I'm overthinking it! I take your point that even if we were to index or structure our sets \\(A\\), \\(B\\), the _join_ would ignore that structure (since joins do not care about order or repetition).

Regarding proving the "obvious" identity, here's one reasonably slick way of doing it.

We write \\((\downarrow v)\\) for the subset \\(\\{ x \in \mathcal{V} : x \leq v\\}\\).

We can then write the definition of join as

\[ \bigvee S \leq v \iff S \subseteq (\downarrow v) \]

But this just states that \\(\bigvee\\) is left adjoint to \\(\downarrow\\) (treating them as monotone maps between \\(\mathcal{V}\\) and the poset of subsets of \\(\mathcal{V}\\)).

So \\(\bigvee\\) preserves joins, ie \\(\bigvee \bigcup \\{ S_i : i \in I \\} = \bigvee \\{ \bigvee S_i : i \in I \\}\\).

which is what we need to show that the join of all \\(v_{a b}\\) = the join of the joins of its rows = the join of the joins of its columns.