Not Preceding implies Exists Completely Irreducible Element in Algebraic Lattice

From ProofWiki
Jump to navigation Jump to search


Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.

Let $x, y \in S$ such that

$y \npreceq x$


$\exists p \in S: p$ is completely irreducible $\land ~x \preceq p \land y \npreceq p$


By definition of algebraic:

$\forall z \in S: z^\ll$ is directed


$L$ satisfies axiom of approximation.

By Axiom of Approximation in Up-Complete Semilattice:

$\exists k \in S: k \ll y \land k \npreceq x$

By Algebraic iff Continuous and For Every Way Below Exists Compact Between:

$\exists z \in K\left({L}\right): k \preceq z \preceq y$

By definition of transitivity:

$z \npreceq x$

By definition of upper closure of element:

$x \notin z^\succeq$

By definition of difference:

$x \in S \setminus z^\succeq$

By definition of relative complement:

$x \in \complement_S\left({z^\succeq}\right)$

By definition of compact subset:

$z$ is a compact element.

By Upper Closure of Element is Way Below Open Filter iff Element is Compact:

$z^\succeq$ is a way below open filter on $L$.

By Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement:

$\exists p \in S: x \preceq p \land p = \max\complement_S\left({z^\succeq}\right)$

Thus by Maximal implies Completely Irreducible:

$p$ is completely irreducible.

Thus $x \preceq p$

Aiming for a contradiction suppose that

$y \preceq p$

By definition of transitivity:

$z \preceq p$

By definition of maximum element:

$p \in \complement_S\left({z^\succeq}\right)$

By definition of relative complement:

$p \notin z^\succeq$

Thus this contradicts $z \preceq p$ by definition of upper closure of element.