Documentation

Mathlib.Order.PrimeSeparator

Separating prime filters and ideals #

In a bounded distributive lattice, if $F$ is a filter, $I$ is an ideal, and $F$ and $I$ are disjoint, then there exists a prime ideal $J$ containing $I$ with $J$ still disjoint from $F$. This theorem is a crucial ingredient to [Stone's][Sto1938] duality for bounded distributive lattices. The construction of the separator relies on Zorn's lemma.

Tags #

ideal, filter, prime, distributive lattice

References #