Constructing complete lattices from total functions to posets

Question

So I ran into this statement that says that the lowest upper bound of a set Y in L, a function space built like L = {f : S → L1 | f is a total function} is somehow related to the joins of the f(s)'s within the original L1 poset, but I don't get the λs. business. What does this say?

Let $L_1 = (L_1, \sqsubseteq) $ be a poset and $S$ be a set.

Define $ L = (L, \sqsubseteq)$ by $ L = \{f: S \rightarrow L_1 | f $ is a total function$ \} $ and $ f \sqsubseteq f' $ iff $\forall s \in S: f(s) \sqsubseteq_1 f'(s)$.

Then, L is a poset. Also, if $L_1$ is a complete lattice, then $L$ is also one. Furthermore:

$$ \bigsqcup Y = \lambda s. \bigsqcup \{f(s) | f \in Y \} $$

and $ \perp = \lambda s.\perp $ and similarly for $ \sqcap Y$ and $\top $

image from original text

Answer 1

Ok, so I'll use a different notation and prove just the join part of the complete lattice.
I won't use the $L_1$ notation as it keeps confusing me...

We have a poset $\mathbf P = (P,\leq)$ and a set $S$ and define the poset $\mathbf L = (L,\leq)$ where $L = P^S$ (the set of maps from $S$ to $P$), with the order defined by $$f \leq f' \iff f(s) \leq f'(s), \,\text{ for all } s \in S.$$

I'll leave it to you to show that $\mathbf L$ is a poset (it seems you have no problem with that).

If $\mathbf P$ is a complete lattice, then you seem to have the task of proving that $\mathbf L$ is a complete lattice where

1. For $Y \subseteq L$, the join of $Y$ is given by $$\left(\bigvee Y\right)(s) = \bigvee\{f(s):f \in Y\}.$$
2. For $Y \subseteq L$, the meet of $Y$ is given by $$\left(\bigwedge Y\right)(s) = \bigwedge\{f(s):f \in Y\}.$$
3. $\bot(s) = \bot$.
4. $\top(s) = \top$.

Let us prove 1.
Define $f_Y(s) = \bigvee\{f(s):f \in Y\}$. We want to prove that $\bigvee Y = f_Y$.

If $g \in Y$ then $g(s) \leq \bigvee\{f(s):f \in Y\} = f_Y(s)$, whence $g \leq f_Y$, and so $f_Y$ is an upper bound of $Y$.

Let $h$ be an upper bound of $Y$. If we prove that $f_Y \leq h$, then we conclude that $f_Y$ is the least upper bound of $Y$, that is, $f_Y = \bigvee Y$.
As $h$ is an upper bound of $Y$, we have $g \leq h$, for any $g \in Y$, or yet, $g(s) \leq h(s)$ for any $g \in Y$ and any $s \in S$.
Thus, $$f_Y(s) = \bigvee\{f(s) : f \in Y\} \leq h(s),$$ and thus $f_Y \leq h$, as we wanted to prove.