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

• [M. H. Stone, Topological representations of distributive lattices and Brouwerian logics (1938)][Sto1938]

theorem DistribLattice.mem_ideal_sup_principal {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a : α) (b : α) (J : Order.Ideal α) : b ∈ J ⊔ Order.Ideal.principal a ↔ ∃ j ∈ J, b ≤ j ⊔ a

theorem DistribLattice.prime_ideal_of_disjoint_filter_ideal {α : Type u_1} [DistribLattice α] [BoundedOrder α] {F : Order.PFilter α} {I : Order.Ideal α} (hFI : Disjoint ↑F ↑I) : ∃ (J : Order.Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J