feat(order/prime_ideal): prime ideals are maximal (#9004)

Proved that in boolean algebras:
1. An ideal is prime iff it always contains one of x, x^c
2. A prime ideal is maximal

src/order/ideal.lean

@@ -203,6 +203,9 @@ begin
   assumption,
 end
 
+lemma is_proper.top_not_mem {I : ideal P} (hI : is_proper I) : ⊤ ∉ I :=
+by { by_contra, exact hI.ne_top (top_of_mem_top h) }
+
 lemma _root_.is_coatom.is_proper {I : ideal P} (hI : is_coatom I) : is_proper I :=
 is_proper_of_ne_top hI.1
 
@@ -343,6 +346,23 @@ end
 
 end distrib_lattice
 
+section boolean_algebra
+
+variables [boolean_algebra P] {x : P} {I : ideal P}
+
+lemma is_proper.not_mem_of_compl_mem (hI : is_proper I) (hxc : xᶜ ∈ I) : x ∉ I :=
+begin
+  intro hx,
+  apply hI.top_not_mem,
+  have ht : x ⊔ xᶜ ∈ I := sup_mem _ _ ‹_› ‹_›,
+  rwa sup_compl_eq_top at ht,
+end
+
+lemma is_proper.not_mem_or_compl_not_mem (hI : is_proper I) : x ∉ I ∨ xᶜ ∉ I :=
+have h : xᶜ ∈ I → x ∉ I := hI.not_mem_of_compl_mem, by tauto
+
+end boolean_algebra
+
 end ideal
 
 /-- For a preorder `P`, `cofinal P` is the type of subsets of `P`

src/order/prime_ideal.lean

@@ -163,6 +163,30 @@ end
 lemma is_prime.mem_compl_of_not_mem (hI : is_prime I) (hxnI : x ∉ I) : xᶜ ∈ I :=
 hI.mem_or_compl_mem.resolve_left hxnI
 
+lemma is_prime_of_mem_or_compl_mem [is_proper I] (h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I) : is_prime I :=
+begin
+  simp only [is_prime_iff_mem_or_mem, or_iff_not_imp_left],
+  intros x y hxy hxI,
+  have hxcI : xᶜ ∈ I := h.resolve_left hxI,
+  have ass : (x ⊓ y) ⊔ (y ⊓ xᶜ) ∈ I := sup_mem _ _ hxy (mem_of_le I inf_le_right hxcI),
+  rwa [inf_comm, sup_inf_inf_compl] at ass
+end
+
+lemma is_prime_iff_mem_or_compl_mem [is_proper I] : is_prime I ↔ ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I :=
+⟨λ h _, h.mem_or_compl_mem, is_prime_of_mem_or_compl_mem⟩
+
+@[priority 100]
+instance is_prime.is_maximal [is_prime I] : is_maximal I :=
+begin
+  simp only [is_maximal_iff, set.eq_univ_iff_forall, is_prime.to_is_proper, true_and],
+  intros J hIJ x,
+  rcases set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩,
+  suffices ass : (x ⊓ y) ⊔ (x ⊓ yᶜ) ∈ J,
+  { rwa sup_inf_inf_compl at ass },
+  exact sup_mem _ _ (J.mem_of_le inf_le_right hyJ)
+    (hIJ.le (I.mem_of_le inf_le_right (is_prime.mem_compl_of_not_mem ‹_› hyI))),
+end
+
 end boolean_algebra
 
 end ideal