Maximal Ideal WRT Filter Complement is Prime in Distributive Lattice
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
If you are fairly certain that there are none, please remove {{proofread}} from the code.
In particular: plenty throughout.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can remove this instance of {{MissingLinks}} from the code.
Theorem
Let $L$ be a distributive lattice.
Full notational specification needed
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this point in more detail, feel free to use the talk page.
If you are able to explain it, then when you have done so you can remove this instance of {{Explain}} from the code.
Let $F$ be a filter in $L$.
Let $M$ be an ideal in $L$ which is disjoint from $F$ such that no ideal in $L$ larger than $M$ is disjoint from $F$.
Then $M$ is a prime ideal.
Proof
Aiming for a contradiction, suppose $M$ is not a prime ideal.
Then by Prime Ideal in Lattice, there are elements $a$ and $b$ of $L$ such that
- $a \wedge b \in M$
- $a \notin M$
- $b \notin M$
Lemma
There do not exist $m$ and $n$ in $M$ such that $m \vee a \in F$ and $n \vee b \in F$.
Proof
Aiming for a contradiction, suppose such exist.
Since:
- $m \vee \paren {n \vee b} \ge n \vee b$
- $n \vee b \in F$
- $F$ is a filter
it follows that:
- $m \vee \paren {n \vee b} \in F$
Applying associativity yields:
- $\paren {m \vee n} \vee b \in F$
By the same argument:
- $\paren {m \vee n} \vee a \in F$
By the definition of a filter:
- $\paren {\paren {m \vee n} \vee b} \wedge \paren {\paren {n \vee m} \vee a} \in F$
Distributing:
- $\paren {m \vee n} \wedge \paren {b \vee a} \in F$
But by assumption:
- $b \vee a \in M$
and by the definition of an ideal:
- $m \vee n \in M$
so again by the definition of an ideal:
- $\paren {m \vee n} \wedge \paren {b \vee a} \in M$
contradicting the supposition that $M$ is disjoint from $F$.
$\Box$
Without loss of generality, we can thus suppose that:
- $m \vee a \notin F$ for all $m \in M$
Let $N = \set {x \in L: \exists m \in M: x \le m \vee a}$.
Lemma
$N$ is an ideal in $L$.
Proof
Let:
- $x \in N$
- $y \in L$
- $y \le x$
Then by the definition of $N$ there exists an $m \in M$ such that:
- $x \le m \vee a$
Since $y \le x$, it follows that:
- $y \le m \vee a$
so $y \in N$.
Let:
- $x \in N$
- $y \in N$
Then there exist $m_x$ and $m_y$ in $M$ such that:
- $x \le m_x \vee a$
- $y \le m_y \vee a$
Then:
- $x \vee y \le \paren {m_x \vee a} \vee \paren {m_y \vee a} = \paren {m_x \vee m_y} \vee a$
But $m_x \vee m_y \in M$, so:
- $x \vee y \in N$
$\Box$
Lemma
$M \subsetneq N$
Proof
Let $m \in M$.
Then:
- $m \le \paren {m \vee a}$
so $m \in N$.
Thus $M \subseteq N$.
We have:
- $a \le \paren {m \vee a}$
so:
- $a \in N$
but:
- $a \notin M$
Thus:
- $M \subsetneq N$
$\Box$
Lemma
$N \cap F = \O$
Proof
Aiming for a contradiction, suppose $x \in N \cap F$.
Then:
- $x \in N$
so for some $m \in M$:
- $x \le m \vee a$
Furthermore, $x \in F$.
So by the definition of a filter:
- $m \vee a \in F$
But this contradicts our assumption that $\forall m \in M: m \vee a \notin F$.
$\Box$
By assuming that $M$ is not a prime ideal, we have constructed an ideal $N$ properly containing $M$ that is disjoint from $F$, contradicting the maximality of $M$.
Thus $M$ is a prime ideal.
$\blacksquare$