Prove that the set of fixed points $Fix(f)$ of an order-preserving operator $f$ on a complete lattice $(L, \sqsubseteq)$ is a complete lattice itself. Moreover, show that $\mathrm{Fix}(f)$ is a complete sublattice of $L$.
The first part of this statement is known as Knaster-Tarski theorem. Can you please give some hints on how to prove it in a straight-forward way? I think it is sufficient to prove the existence of a least upper bound and a greatest lower bound of any subset of $Fix(f)$.
Moreover, I haven't found anything online about proving that $Fix(f)$ is a complete sublattice of $L$. How would you prove it? Thank you in advance. I'm a CS graduate trying to wrap my head around abstract semantics of programming languages.
Here are some useful definitions (feel free to correct them in case of errors):
Upper Bound Given a subset $X \subseteq L$, $l \in X$ is an upper bound if $\forall\ l' \in X : l' \sqsubseteq l$. A least upper bound (also called supremum) $l \in X$ is an upper bound of $X$ that satisfies $l \sqsubseteq l_0$ whenever $l_0$ is another upper bound of $X$.
Lower Bound Given a subset $X \subseteq L$, $l \in X$ is a lower bound if $\forall\ l' \in X : l' \sqsupseteq l$. A greatest lower bound (also called infimum) $l \in X$ is a lower bound of $X$ that satisfies $l_0 \sqsubseteq l$ whenever $l_0$ is another lower bound of $X$.
Complete Lattice: A complete lattice $L = (L, \sqsubseteq) = (L, \sqsubseteq, \sqcup, \sqcap, \top, \bot)$ is a partially ordered set $(L, \sqsubseteq)$ such that all subsets of $L$ have least upper bounds and greatest lower bounds.
Sublattice: Let $L = (L, \sqsubseteq)$ be a lattice. $S \subseteq L$ is a sublattice of $L$ if and only if
\begin{equation*} \forall x, y \in S\ :\ x \sqcup y \in S\ \wedge\ x \sqcap y \in S \end{equation*}
Order-preserving Operator: An operator $f : L \rightarrow L$ on a partially ordered set $(L, \sqsubseteq)$ is order-preserving if
\begin{equation} \forall\ l, l' \in L : l \sqsubseteq l' \Rightarrow f(l) \sqsubseteq f(l') \end{equation}
Fixed point: Given an order-preserving operator $f : L \rightarrow L$ defined on a complete lattice $(L, \sqsubseteq)$, a fixed point of $f$ is an element $l \in L$ such that $f(l) = l$. The set of all fixed points is
\begin{equation} \mathrm{Fix}(f) = \{ l\ |\ f(l) = l \} \end{equation}
I don't think $Fix(f)$ is a complete sublattice of $L$.
Maybe you're missing some additional condition, or maybe I'm thinking wrong.
Check the following and let me know!
Let $L = \wp_{fin}(\mathbb N) \cup \{\mathbb N, \mathbb Q\}$, where $\wp_{fin}(X)$ denotes the family of finite subsets of $X$, and $L$ is ordered by set inclusion.
This is a complete lattice.
Define $f:L\to L$ by making $$ x \mapsto \begin{cases} x, &\text{ if } x \in \wp_{fin}(\mathbb N),\\ \mathbb{Q}, &\text{ otherwise.} \end{cases} $$ Then $f$ is order-preserving, but $Fix(f) = \wp_{fin}(\mathbb N) \cup \{\mathbb Q\} = L\setminus\{\mathbb N\}$ is not a complete sublattice of $L$.