feat(order/ideal, order/pfilter, order/prime_ideal): added is_ideal…

…, `is_pfilter`, `is_prime`, `is_maximal`, `prime_pair` (#6656)

Proved basic lemmas about them. Also extended the is_proper API.

Made the `pfilter`arguments of some lemmas explicit:
- `pfilter.nonempty`
- `pfilter.directed`

src/order/boolean_algebra.lean

@@ -46,6 +46,9 @@ eq.trans sup_comm sup_compl_eq_top
 theorem is_compl_compl : is_compl x xᶜ :=
 is_compl.of_eq inf_compl_eq_bot sup_compl_eq_top
 
+theorem is_compl.eq_compl (h : is_compl x y) : x = yᶜ :=
+h.left_unique is_compl_compl.symm
+
 theorem is_compl.compl_eq (h : is_compl x y) : xᶜ = y :=
 (h.right_unique is_compl_compl).symm
 

src/order/ideal.lean

@@ -5,6 +5,7 @@ Authors: David Wärn
 -/
 import order.basic
 import data.equiv.encodable.basic
+import order.atoms
 
 /-!
 # Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma
@@ -14,12 +15,19 @@ import data.equiv.encodable.basic
 Throughout this file, `P` is at least a preorder, but some sections require more
 structure, such as a bottom element, a top element, or a join-semilattice structure.
 
-- `ideal P`: the type of upward directed, downward closed subsets of `P`.
-             Dual to the notion of a filter on a preorder.
-- `cofinal P`: the type of subsets of `P` containing arbitrarily large elements.
-               Dual to the notion of 'dense set' used in forcing.
-- `ideal_of_cofinals p 𝒟`, where `p : P`, and `𝒟` is a countable family of cofinal
-  subsets of P: an ideal in `P` which contains `p` and intersects every set in `𝒟`.
+- `order.ideal P`: the type of nonempty, upward directed, and downward closed subsets of `P`.
+  Dual to the notion of a filter on a preorder.
+- `order.is_ideal P`: a predicate for when a `set P` is an ideal.
+- `order.ideal.principal p`: the principal ideal generated by `p : P`.
+- `order.ideal.is_proper P`: a predicate for proper ideals.
+  Dual to the notion of a proper filter.
+- `order.ideal.is_maximal`: a predicate for maximal ideals.
+  Dual to the notion of an ultrafilter.
+- `order.cofinal P`: the type of subsets of `P` containing arbitrarily large elements.
+  Dual to the notion of 'dense set' used in forcing.
+- `order.ideal_of_cofinals p 𝒟`, where `p : P`, and `𝒟` is a countable family of cofinal
+  subsets of P: an ideal in `P` which contains `p` and intersects every set in `𝒟`. (This a form
+  of the Rasiowa–Sikorski lemma.)
 
 ## References
 
@@ -42,14 +50,28 @@ variables {P : Type*}
 
 /-- An ideal on a preorder `P` is a subset of `P` that is
   - nonempty
-  - upward directed
-  - downward closed. -/
+  - upward directed (any pair of elements in the ideal has an upper bound in the ideal)
+  - downward closed (any element less than an element of the ideal is in the ideal). -/
 structure ideal (P) [preorder P] :=
 (carrier   : set P)
 (nonempty  : carrier.nonempty)
 (directed  : directed_on (≤) carrier)
 (mem_of_le : ∀ {x y : P}, x ≤ y → y ∈ carrier → x ∈ carrier)
 
+/-- A subset of a preorder `P` is an ideal if it is
+  - nonempty
+  - upward directed (any pair of elements in the ideal has an upper bound in the ideal)
+  - downward closed (any element less than an element of the ideal is in the ideal). -/
+@[mk_iff] structure is_ideal {P} [preorder P] (I : set P) : Prop :=
+(nonempty : I.nonempty)
+(directed : directed_on (≤) I)
+(mem_of_le : ∀ {x y : P}, x ≤ y → y ∈ I → x ∈ I)
+
+/-- Create an element of type `order.ideal` from a set satisfying the predicate
+`order.is_ideal`. -/
+def is_ideal.to_ideal [preorder P] {I : set P} (h : is_ideal I) : ideal P :=
+⟨I, h.1, h.2, h.3⟩
+
 namespace ideal
 
 section preorder
@@ -75,6 +97,13 @@ instance : has_mem P (ideal P) := ⟨λ x I, x ∈ (I : set P)⟩
 @[ext] lemma ext : ∀ (I J : ideal P), (I : set P) = J → I = J
 | ⟨_, _, _, _⟩ ⟨_, _, _, _⟩ rfl := rfl
 
+@[simp, norm_cast] lemma ext_set_eq {I J : ideal P} : (I : set P) = J ↔ I = J :=
+⟨by ext, congr_arg _⟩
+
+lemma ext'_iff {I J : ideal P} : I = J ↔ (I : set P) = J := ext_set_eq.symm
+
+lemma is_ideal (I : ideal P) : is_ideal (I : set P) := ⟨I.2, I.3, I.4⟩
+
 /-- The partial ordering by subset inclusion, inherited from `set P`. -/
 instance : partial_order (ideal P) := partial_order.lift coe ext
 
@@ -87,15 +116,21 @@ instance : partial_order (ideal P) := partial_order.lift coe ext
 
 /-- A proper ideal is one that is not the whole set.
     Note that the whole set might not be an ideal. -/
-class proper (I : ideal P) : Prop := (nuniv : (I : set P) ≠ set.univ)
+@[mk_iff] class is_proper (I : ideal P) : Prop := (ne_univ : (I : set P) ≠ set.univ)
 
-lemma proper_of_not_mem {I : ideal P} {p : P} (nmem : p ∉ I) : proper I :=
+lemma is_proper_of_not_mem {I : ideal P} {p : P} (nmem : p ∉ I) : is_proper I :=
 ⟨λ hp, begin
   change p ∉ ↑I at nmem,
   rw hp at nmem,
   exact nmem (set.mem_univ p),
 end⟩
 
+/-- An ideal is maximal if it is maximal in the collection of proper ideals.
+  Note that we cannot use the `is_coatom` class because `P` might not have a `top` element.
+-/
+@[mk_iff] class is_maximal (I : ideal P) extends is_proper I : Prop :=
+(maximal_proper : ∀ J : ideal P, I < J → J.carrier = set.univ)
+
 end preorder
 
 section order_bot
@@ -126,17 +161,47 @@ instance : order_top (ideal P) :=
 @[simp] lemma top_carrier : (⊤ : ideal P).carrier = set.univ :=
 set.univ_subset_iff.1 (λ p _, le_top)
 
-lemma top_of_mem_top {I : ideal P} (topmem : ⊤ ∈ I) : I = ⊤ :=
+@[simp] lemma top_coe : ((⊤ : ideal P) : set P) = set.univ := top_carrier
+
+lemma top_of_mem_top {I : ideal P} (mem_top : ⊤ ∈ I) : I = ⊤ :=
 begin
   ext,
   change x ∈ I.carrier ↔ x ∈ (⊤ : ideal P).carrier,
   split,
   { simp [top_carrier] },
-  { exact λ _, I.mem_of_le le_top topmem }
+  { exact λ _, I.mem_of_le le_top mem_top }
 end
 
-lemma proper_of_ne_top {I : ideal P} (ntop : I ≠ ⊤) : proper I :=
-proper_of_not_mem (λ h, ntop (top_of_mem_top h))
+lemma is_proper_of_ne_top {I : ideal P} (ne_top : I ≠ ⊤) : is_proper I :=
+is_proper_of_not_mem (λ h, ne_top (top_of_mem_top h))
+
+lemma is_proper.ne_top {I : ideal P} (hI : is_proper I) : I ≠ ⊤ :=
+begin
+  intro h,
+  rw [ext'_iff, top_coe] at h,
+  apply hI.ne_univ,
+  assumption,
+end
+
+lemma _root_.is_coatom.is_proper {I : ideal P} (hI : is_coatom I) : is_proper I :=
+is_proper_of_ne_top hI.1
+
+lemma is_proper_iff_ne_top {I : ideal P} : is_proper I ↔ I ≠ ⊤ :=
+⟨λ h, h.ne_top, λ h, is_proper_of_ne_top h⟩
+
+lemma is_maximal.is_coatom {I : ideal P} (h : is_maximal I) : is_coatom I :=
+⟨is_maximal.to_is_proper.ne_top,
+ λ J _, by { rw [ext'_iff, top_coe], exact is_maximal.maximal_proper J ‹_› }⟩
+
+lemma is_maximal.is_coatom' {I : ideal P} [is_maximal I] : is_coatom I :=
+is_maximal.is_coatom ‹_›
+
+lemma _root_.is_coatom.is_maximal {I : ideal P} (hI : is_coatom I) : is_maximal I :=
+{ maximal_proper := λ _ _, by simp [hI.2 _ ‹_›],
+  ..is_coatom.is_proper ‹_› }
+
+lemma is_maximal_iff_is_coatom {I : ideal P} : is_maximal I ↔ is_coatom I :=
+⟨λ h, h.is_coatom, λ h, h.is_maximal⟩
 
 end order_top
 
@@ -215,7 +280,7 @@ namespace cofinal
 variables [preorder P]
 
 instance : inhabited (cofinal P) :=
-⟨{ carrier := set.univ, mem_gt := λ x, ⟨x, trivial, le_refl _⟩}⟩
+⟨{ carrier := set.univ, mem_gt := λ x, ⟨x, trivial, le_refl _⟩ }⟩
 
 instance : has_mem P (cofinal P) := ⟨λ x D, x ∈ D.carrier⟩
 

src/order/pfilter.lean

@@ -14,9 +14,11 @@ Throughout this file, `P` is at least a preorder, but some sections
 require more structure, such as a bottom element, a top element, or
 a join-semilattice structure.
 
-- `pfilter P`: The type of nonempty, downward directed, upward closed
+- `order.pfilter P`: The type of nonempty, downward directed, upward closed
                subsets of `P`. This is dual to `order.ideal`, so it
                simply wraps `order.ideal (order_dual P)`.
+- `order.is_pfilter P`: a predicate for when a `set P` is a filter.
+
 
 Note the relation between `order/filter` and `order/pfilter`: for any
 type `α`, `filter α` represents the same mathematical object as
@@ -32,34 +34,48 @@ pfilter, filter, ideal, dual
 
 -/
 
+namespace order
+
 variables {P : Type*}
 
 /-- A filter on a preorder `P` is a subset of `P` that is
   - nonempty
   - downward directed
   - upward closed. -/
 structure pfilter (P) [preorder P] :=
-(dual : order.ideal (order_dual P))
+(dual : ideal (order_dual P))
+
+/-- A predicate for when a subset of `P` is a filter. -/
+def is_pfilter [preorder P] (F : set P) : Prop :=
+@is_ideal (order_dual P) _ F
+
+/-- Create an element of type `order.pfilter` from a set satisfying the predicate
+`order.is_pfilter`. -/
+def is_pfilter.to_pfilter [preorder P] {F : set P} (h : is_pfilter F) : pfilter P :=
+⟨h.to_ideal⟩
 
 namespace pfilter
 
 section preorder
-variables [preorder P] {x y : P} {F G : pfilter P}
+variables [preorder P] {x y : P} (F : pfilter P)
 
 /-- A filter on `P` is a subset of `P`. -/
 instance : has_coe (pfilter P) (set P) := ⟨λ F, F.dual.carrier⟩
 
 /-- For the notation `x ∈ F`. -/
 instance : has_mem P (pfilter P) := ⟨λ x F, x ∈ (F : set P)⟩
 
+lemma is_pfilter : is_pfilter (F : set P) :=
+F.dual.is_ideal
+
 lemma nonempty : (F : set P).nonempty := F.dual.nonempty
 
 lemma directed : directed_on (≥) (F : set P) := F.dual.directed
 
-lemma mem_of_le : x ≤ y → x ∈ F → y ∈ F := λ h, F.dual.mem_of_le h
+lemma mem_of_le {F : pfilter P} : x ≤ y → x ∈ F → y ∈ F := λ h, F.dual.mem_of_le h
 
 /-- The smallest filter containing a given element. -/
-def principal (p : P) : pfilter P := ⟨order.ideal.principal p⟩
+def principal (p : P) : pfilter P := ⟨ideal.principal p⟩
 
 instance [inhabited P] : inhabited (pfilter P) := ⟨⟨default _⟩⟩
 
@@ -70,11 +86,11 @@ instance [inhabited P] : inhabited (pfilter P) := ⟨⟨default _⟩⟩
 /-- The partial ordering by subset inclusion, inherited from `set P`. -/
 instance : partial_order (pfilter P) := partial_order.lift coe ext
 
-@[trans] lemma mem_of_mem_of_le : x ∈ F → F ≤ G → x ∈ G :=
-order.ideal.mem_of_mem_of_le
+@[trans] lemma mem_of_mem_of_le {F G : pfilter P} : x ∈ F → F ≤ G → x ∈ G :=
+ideal.mem_of_mem_of_le
 
-@[simp] lemma principal_le_iff : principal x ≤ F ↔ x ∈ F :=
-order.ideal.principal_le_iff
+@[simp] lemma principal_le_iff {F : pfilter P} : principal x ≤ F ↔ x ∈ F :=
+ideal.principal_le_iff
 
 end preorder
 
@@ -83,7 +99,7 @@ variables [order_top P] {F : pfilter P}
 
 /-- A specific witness of `pfilter.nonempty` when `P` has a top element. -/
 @[simp] lemma top_mem : ⊤ ∈ F :=
-order.ideal.bot_mem
+ideal.bot_mem
 
 /-- There is a bottom filter when `P` has a top element. -/
 instance : order_bot (pfilter P) :=
@@ -104,11 +120,13 @@ variables [semilattice_inf P] {x y : P} {F : pfilter P}
 
 /-- A specific witness of `pfilter.directed` when `P` has meets. -/
 lemma inf_mem (x y ∈ F) : x ⊓ y ∈ F :=
-order.ideal.sup_mem x y ‹x ∈ F› ‹y ∈ F›
+ideal.sup_mem x y ‹x ∈ F› ‹y ∈ F›
 
 @[simp] lemma inf_mem_iff : x ⊓ y ∈ F ↔ x ∈ F ∧ y ∈ F :=
-order.ideal.sup_mem_iff
+ideal.sup_mem_iff
 
 end semilattice_inf
 
 end pfilter
+
+end order

src/order/prime_ideal.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2021 Noam Atar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Noam Atar
+-/
+import order.basic
+import order.ideal
+import order.pfilter
+
+/-!
+# Prime ideals
+
+## Main definitions
+
+Throughout this file, `P` is at least a preorder, but some sections require more
+structure, such as a bottom element, a top element, or a join-semilattice structure.
+
+- `order.ideal.prime_pair`: A pair of an `ideal` and a `pfilter` which form a partition of `P`.
+  This is useful as giving the data of a prime ideal is the same as giving the data of a prime
+  filter.
+- `order.ideal.is_prime`: a predicate for prime ideals. Dual to the notion of a prime filter.
+- `order.pfilter.is_prime`: a predicate for prime filters. Dual to the notion of a prime ideal.
+
+## References
+
+- <https://en.wikipedia.org/wiki/Ideal_(order_theory)>
+
+## Tags
+
+ideal, prime
+
+-/
+
+namespace order
+
+variables {P : Type*}
+
+section preorder
+
+variables [preorder P]
+
+namespace ideal
+
+/-- A pair of an `ideal` and a `pfilter` which form a partition of `P`.
+-/
+@[nolint has_inhabited_instance]
+structure prime_pair (P : Type*) [preorder P] :=
+(I            : ideal P)
+(F            : pfilter P)
+(is_compl_I_F : is_compl (I : set P) F)
+
+namespace prime_pair
+variable (IF : prime_pair P)
+
+lemma compl_I_eq_F : (IF.I : set P)ᶜ = IF.F := IF.is_compl_I_F.compl_eq
+lemma compl_F_eq_I : (IF.F : set P)ᶜ = IF.I := IF.is_compl_I_F.eq_compl.symm
+
+lemma I_is_proper : is_proper IF.I :=
+begin
+  cases IF.F.nonempty,
+  apply is_proper_of_not_mem (_ : w ∉ IF.I),
+  rwa ← IF.compl_I_eq_F at h,
+end
+
+lemma disjoint : disjoint (IF.I : set P) IF.F := IF.is_compl_I_F.disjoint
+
+lemma I_union_F : (IF.I : set P) ∪ IF.F = set.univ := IF.is_compl_I_F.sup_eq_top
+lemma F_union_I : (IF.F : set P) ∪ IF.I = set.univ := IF.is_compl_I_F.symm.sup_eq_top
+
+end prime_pair
+
+/-- An ideal `I` is prime if its complement is a filter.
+-/
+@[mk_iff] class is_prime (I : ideal P) extends is_proper I : Prop :=
+(compl_filter : is_pfilter (I : set P)ᶜ)
+
+/-- Create an element of type `order.ideal.prime_pair` from an ideal satisfying the predicate
+`order.ideal.is_prime`. -/
+def is_prime.to_prime_pair {I : ideal P} (h : is_prime I) : prime_pair P :=
+{ I            := I,
+  F            := h.compl_filter.to_pfilter,
+  is_compl_I_F := is_compl_compl }
+
+lemma prime_pair.I_is_prime (IF : prime_pair P) : is_prime IF.I :=
+{ compl_filter := by { rw IF.compl_I_eq_F, exact IF.F.is_pfilter },
+  ..IF.I_is_proper }
+
+end ideal
+
+namespace pfilter
+
+/-- A filter `F` is prime if its complement is an ideal.
+-/
+@[mk_iff] class is_prime (F : pfilter P) : Prop :=
+(compl_ideal : is_ideal (F : set P)ᶜ)
+
+/-- Create an element of type `order.ideal.prime_pair` from a filter satisfying the predicate
+`order.pfilter.is_prime`. -/
+def is_prime.to_prime_pair {F : pfilter P} (h : is_prime F) : ideal.prime_pair P :=
+{ I            := h.compl_ideal.to_ideal,
+  F            := F,
+  is_compl_I_F := is_compl_compl.symm }
+
+lemma _root_.order.ideal.prime_pair.F_is_prime (IF : ideal.prime_pair P) : is_prime IF.F :=
+{ compl_ideal := by { rw IF.compl_F_eq_I, exact IF.I.is_ideal } }
+
+end pfilter
+
+end preorder
+
+end order