feat(order/filter/ultrafilter): an ultrafilter is an atom in the latt…

…ice of filters (#17116)

* add `filter.nontrivial`, `filter.Inf_ne_bot_of_directed`, and `filter.Inf_ne_bot_of_directed'`;
* add `is_atom_iff` and `is_coatom_iff`;
* generalize `ultrafilter.exists_le` to any partial order;
* prove that a filter is an ultrafilter if and only if it is an atom in the lattice of filters.

src/order/atoms.lean

@@ -70,6 +70,10 @@ lemma is_atom.Iic (ha : is_atom a) (hax : a ≤ x) : is_atom (⟨a, hax⟩ : set
 lemma is_atom.of_is_atom_coe_Iic {a : set.Iic x} (ha : is_atom a) : is_atom (a : α) :=
 ⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩
 
+lemma is_atom_iff {a : α} : is_atom a ↔ a ≠ ⊥ ∧ ∀ b ≠ ⊥, b ≤ a → a ≤ b :=
+and_congr iff.rfl $ forall_congr $
+  λ b, by simp only [ne.def, @not_imp_comm (b = ⊥), not_imp, lt_iff_le_not_le]
+
 end preorder
 
 variables [partial_order α] [order_bot α] {a b x : α}
@@ -118,6 +122,8 @@ lemma is_coatom.of_is_coatom_coe_Ici {a : set.Ici x} (ha : is_coatom a) :
   is_coatom (a : α) :=
 @is_atom.of_is_atom_coe_Iic αᵒᵈ _ _ x a ha
 
+lemma is_coatom_iff {a : α} : is_coatom a ↔ a ≠ ⊤ ∧ ∀ b ≠ ⊤, a ≤ b → b ≤ a := @is_atom_iff αᵒᵈ _ _ _
+
 end preorder
 
 variables [partial_order α] [order_top α] {a b x : α}

src/order/filter/basic.lean

@@ -672,11 +672,14 @@ lemma forall_mem_nonempty_iff_ne_bot {f : filter α} :
   (∀ (s : set α), s ∈ f → s.nonempty) ↔ ne_bot f :=
 ⟨λ h, ⟨λ hf, empty_not_nonempty (h ∅ $ hf.symm ▸ mem_bot)⟩, @nonempty_of_mem _ _⟩
 
+instance [nonempty α] : nontrivial (filter α) :=
+⟨⟨⊤, ⊥, ne_bot.ne $ forall_mem_nonempty_iff_ne_bot.1 $ λ s hs,
+  by rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]⟩⟩
+
 lemma nontrivial_iff_nonempty : nontrivial (filter α) ↔ nonempty α :=
-⟨λ ⟨⟨f, g, hfg⟩⟩, by_contra $
-  λ h, hfg $ by haveI : is_empty α := not_nonempty_iff.1 h; exact subsingleton.elim _ _,
-  λ ⟨x⟩, ⟨⟨⊤, ⊥, ne_bot.ne $ forall_mem_nonempty_iff_ne_bot.1 $ λ s hs,
-    by rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]⟩⟩⟩
+⟨λ h, by_contra $ λ h',
+  by { haveI := not_nonempty_iff.1 h', exact not_subsingleton (filter α) infer_instance },
+  @filter.nontrivial α⟩
 
 lemma eq_Inf_of_mem_iff_exists_mem {S : set (filter α)} {l : filter α}
   (h : ∀ {s}, s ∈ l ↔ ∃ f ∈ S, s ∈ f) : l = Inf S :=
@@ -819,14 +822,21 @@ end⟩
 See also `infi_ne_bot_of_directed'` for a version assuming `nonempty ι` instead of `nonempty α`. -/
 lemma infi_ne_bot_of_directed {f : ι → filter α}
   [hn : nonempty α] (hd : directed (≥) f) (hb : ∀ i, ne_bot (f i)) : ne_bot (infi f) :=
-if hι : nonempty ι then @infi_ne_bot_of_directed' _ _ _ hι hd hb else
-⟨λ h : infi f = ⊥,
-  have univ ⊆ (∅ : set α),
-  begin
-    rw [←principal_mono, principal_univ, principal_empty, ←h],
-    exact (le_infi $ λ i, false.elim $ hι ⟨i⟩)
-  end,
-  let ⟨x⟩ := hn in this (mem_univ x)⟩
+begin
+  casesI is_empty_or_nonempty ι,
+  { constructor, simp [infi_of_empty f, top_ne_bot] },
+  { exact infi_ne_bot_of_directed' hd hb }
+end
+
+lemma Inf_ne_bot_of_directed' {s : set (filter α)} (hne : s.nonempty) (hd : directed_on (≥) s)
+  (hbot : ⊥ ∉ s) : ne_bot (Inf s) :=
+(Inf_eq_infi' s).symm ▸ @infi_ne_bot_of_directed' _ _ _
+  hne.to_subtype hd.directed_coe (λ ⟨f, hf⟩, ⟨ne_of_mem_of_not_mem hf hbot⟩)
+
+lemma Inf_ne_bot_of_directed [nonempty α] {s : set (filter α)} (hd : directed_on (≥) s)
+  (hbot : ⊥ ∉ s) : ne_bot (Inf s) :=
+(Inf_eq_infi' s).symm ▸ infi_ne_bot_of_directed hd.directed_coe
+  (λ ⟨f, hf⟩, ⟨ne_of_mem_of_not_mem hf hbot⟩)
 
 lemma infi_ne_bot_iff_of_directed' {f : ι → filter α} [nonempty ι] (hd : directed (≥) f) :
   ne_bot (infi f) ↔ ∀ i, ne_bot (f i) :=

src/order/filter/ultrafilter.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov
 -/
 import order.filter.cofinite
-import order.zorn
+import order.zorn_atoms
 
 /-!
 # Ultrafilters
@@ -25,6 +25,13 @@ variables {α : Type u} {β : Type v} {γ : Type*}
 open set filter function
 open_locale classical filter
 
+/-- `filter α` is an atomic type: for every filter there exists an ultrafilter that is less than or
+equal to this filter. -/
+instance : is_atomic (filter α) :=
+is_atomic.of_is_chain_bounded $ λ c hc hne hb,
+  ⟨Inf c, (Inf_ne_bot_of_directed' hne (show is_chain (≥) c, from hc.symm).directed_on hb).ne,
+    λ x hx, Inf_le hx⟩
+
 /-- An ultrafilter is a minimal (maximal in the set order) proper filter. -/
 @[protect_proj]
 structure ultrafilter (α : Type*) extends filter α :=
@@ -45,6 +52,9 @@ le_antisymm h $ f.le_of_le g hne h
 
 instance ne_bot (f : ultrafilter α) : ne_bot (f : filter α) := f.ne_bot'
 
+protected lemma is_atom (f : ultrafilter α) : is_atom (f : filter α) :=
+⟨f.ne_bot.ne, λ g hgf, by_contra $ λ hg, hgf.ne $ f.unique hgf.le ⟨hg⟩⟩
+
 @[simp, norm_cast] lemma mem_coe : s ∈ (f : filter α) ↔ s ∈ f := iff.rfl
 
 lemma coe_injective : injective (coe : ultrafilter α → filter α)
@@ -94,6 +104,12 @@ def of_compl_not_mem_iff (f : filter α) (h : ∀ s, sᶜ ∉ f ↔ s ∈ f) : u
   ne_bot' := ⟨λ hf, by simpa [hf] using h⟩,
   le_of_le := λ g hg hgf s hs, (h s).1 $ λ hsc, by exactI compl_not_mem hs (hgf hsc) }
 
+/-- If `f : filter α` is an atom, then it is an ultrafilter. -/
+def of_atom (f : filter α) (hf : is_atom f) : ultrafilter α :=
+{ to_filter := f,
+  ne_bot' := ⟨hf.1⟩,
+  le_of_le := λ g hg, (_root_.is_atom_iff.1 hf).2 g hg.ne }
+
 lemma nonempty_of_mem (hs : s ∈ f) : s.nonempty := nonempty_of_mem hs
 lemma ne_empty_of_mem (hs : s ∈ f) : s ≠ ∅ := (nonempty_of_mem hs).ne_empty
 @[simp] lemma empty_not_mem : ∅ ∉ f := empty_not_mem f
@@ -230,27 +246,8 @@ instance is_lawful_monad : is_lawful_monad ultrafilter :=
 end
 
 /-- The ultrafilter lemma: Any proper filter is contained in an ultrafilter. -/
-lemma exists_le (f : filter α) [h : ne_bot f] : ∃u : ultrafilter α, ↑u ≤ f :=
-begin
-  let τ                := {f' // ne_bot f' ∧ f' ≤ f},
-  let r : τ → τ → Prop := λt₁ t₂, t₂.val ≤ t₁.val,
-  haveI                := nonempty_of_ne_bot f,
-  let top : τ          := ⟨f, h, le_refl f⟩,
-  let sup : Π(c:set τ), is_chain r c → τ :=
-    λc hc, ⟨⨅a:{a:τ // a ∈ insert top c}, a.1,
-      infi_ne_bot_of_directed
-        (is_chain.directed $ hc.insert $ λ ⟨b, _, hb⟩ _ _, or.inl hb)
-        (assume ⟨⟨a, ha, _⟩, _⟩, ha),
-      infi_le_of_le ⟨top, mem_insert _ _⟩ le_rfl⟩,
-  have : ∀ c (hc : is_chain r c) a (ha : a ∈ c), r a (sup c hc),
-    from assume c hc a ha, infi_le_of_le ⟨a, mem_insert_of_mem _ ha⟩ le_rfl,
-  have : (∃ (u : τ), ∀ (a : τ), r u a → r a u),
-    from exists_maximal_of_chains_bounded (assume c hc, ⟨sup c hc, this c hc⟩)
-      (assume f₁ f₂ f₃ h₁ h₂, le_trans h₂ h₁),
-  cases this with uτ hmin,
-  exact ⟨⟨uτ.val, uτ.property.left, assume g hg₁ hg₂,
-    hmin ⟨g, hg₁, le_trans hg₂ uτ.property.right⟩ hg₂⟩, uτ.property.right⟩
-end
+lemma exists_le (f : filter α) [h : ne_bot f] : ∃ u : ultrafilter α, ↑u ≤ f :=
+let ⟨u, hu, huf⟩ := (eq_bot_or_exists_atom_le f).resolve_left h.ne in ⟨of_atom u hu, huf⟩
 
 alias exists_le ← _root_.filter.exists_ultrafilter_le
 
@@ -281,6 +278,8 @@ variables {f : filter α} {s : set α} {a : α}
 
 open ultrafilter
 
+lemma is_atom_pure : is_atom (pure a : filter α) := (pure a : ultrafilter α).is_atom
+
 protected lemma ne_bot.le_pure_iff (hf : f.ne_bot) : f ≤ pure a ↔ f = pure a :=
 ⟨ultrafilter.unique (pure a), le_of_eq⟩
 

src/order/zorn_atoms.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import order.zorn
+import order.atoms
+
+/-!
+# Zorn lemma for (co)atoms
+
+In this file we use Zorn's lemma to prove that a partial order is atomic if every nonempty chain
+`c`, `⊥ ∉ c`, has a lower bound not equal to `⊥`. We also prove the order dual version of this
+statement.
+-/
+
+open set
+
+/-- **Zorn's lemma**: A partial order is coatomic if every nonempty chain `c`, `⊤ ∉ c`, has an upper
+bound not equal to `⊤`. -/
+lemma is_coatomic.of_is_chain_bounded {α : Type*} [partial_order α] [order_top α]
+  (h : ∀ c : set α, is_chain (≤) c → c.nonempty → ⊤ ∉ c → ∃ x ≠ ⊤, x ∈ upper_bounds c) :
+  is_coatomic α :=
+begin
+  refine ⟨λ x, le_top.eq_or_lt.imp_right $ λ hx, _⟩,
+  rcases zorn_nonempty_partial_order₀ (Ico x ⊤) (λ c hxc hc y hy, _) x (left_mem_Ico.2 hx)
+    with ⟨y, ⟨hxy, hy⟩, -, hy'⟩,
+  { refine ⟨y, ⟨hy.ne, λ z hyz, le_top.eq_or_lt.resolve_right $ λ hz, _⟩, hxy⟩,
+    exact hyz.ne' (hy' z ⟨hxy.trans hyz.le, hz⟩ hyz.le) },
+  { rcases h c hc ⟨y, hy⟩ (λ h, (hxc h).2.ne rfl) with ⟨z, hz, hcz⟩,
+    exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩ }
+end
+
+/-- **Zorn's lemma**: A partial order is atomic if every nonempty chain `c`, `⊥ ∉ c`, has an lower
+bound not equal to `⊥`. -/
+lemma is_atomic.of_is_chain_bounded {α : Type*} [partial_order α] [order_bot α]
+  (h : ∀ c : set α, is_chain (≤) c → c.nonempty → ⊥ ∉ c → ∃ x ≠ ⊥, x ∈ lower_bounds c) :
+  is_atomic α :=
+is_coatomic_dual_iff_is_atomic.mp $ is_coatomic.of_is_chain_bounded $ λ c hc, h c hc.symm