feat(order/filter/*,topology/noetherian_space): add lemmas about cofinite (#16498)

* A filter is disjoint with `cofinite` iff there exists a finite set that belongs to this filter.
* An ultrafilter is either less than or equal to `cofinite`, or is equal to `pure a` for some `a`.
* Any type with cofinite topology is a Noetherian (hence, is a compact) space.

Author: urkud

src/order/filter/cofinite.lean

@@ -23,7 +23,7 @@ Define filters for other cardinalities of the complement.
 open set function
 open_locale classical
 
-variables {ι α β : Type*}
+variables {ι α β : Type*} {l : filter α}
 
 namespace filter
 
@@ -69,16 +69,14 @@ frequently_cofinite_iff_infinite.symm
 lemma eventually_cofinite_ne (x : α) : ∀ᶠ a in cofinite, a ≠ x :=
 (set.finite_singleton x).eventually_cofinite_nmem
 
-lemma le_cofinite_iff_compl_singleton_mem {l : filter α} :
-  l ≤ cofinite ↔ ∀ x, {x}ᶜ ∈ l :=
+lemma le_cofinite_iff_compl_singleton_mem : l ≤ cofinite ↔ ∀ x, {x}ᶜ ∈ l :=
 begin
   refine ⟨λ h x, h (finite_singleton x).compl_mem_cofinite, λ h s (hs : sᶜ.finite), _⟩,
   rw [← compl_compl s, ← bUnion_of_singleton sᶜ, compl_Union₂,filter.bInter_mem hs],
   exact λ x _, h x
 end
 
-lemma le_cofinite_iff_eventually_ne {l : filter α} :
-  l ≤ cofinite ↔ ∀ x, ∀ᶠ y in l, y ≠ x :=
+lemma le_cofinite_iff_eventually_ne : l ≤ cofinite ↔ ∀ x, ∀ᶠ y in l, y ≠ x :=
 le_cofinite_iff_compl_singleton_mem
 
 /-- If `α` is a preorder with no maximal element, then `at_top ≤ cofinite`. -/
@@ -100,6 +98,15 @@ lemma Coprod_cofinite {α : ι → Type*} [finite ι] :
 filter.coext $ λ s, by simp only [compl_mem_Coprod, mem_cofinite, compl_compl,
   forall_finite_image_eval_iff]
 
+@[simp] lemma disjoint_cofinite_left : disjoint cofinite l ↔ ∃ s ∈ l, set.finite s :=
+begin
+  simp only [has_basis_cofinite.disjoint_iff l.basis_sets, id, disjoint_compl_left_iff_subset],
+  exact ⟨λ ⟨s, hs, t, ht, hts⟩, ⟨t, ht, hs.subset hts⟩, λ ⟨s, hs, hsf⟩, ⟨s, hsf, s, hs, subset.rfl⟩⟩
+end
+
+@[simp] lemma disjoint_cofinite_right : disjoint l cofinite ↔ ∃ s ∈ l, set.finite s :=
+disjoint.comm.trans disjoint_cofinite_left
+
 end filter
 
 open filter

src/order/filter/ultrafilter.lean

@@ -67,6 +67,12 @@ le_of_inf_eq (f.unique inf_le_left hg)
 lemma le_of_inf_ne_bot' (f : ultrafilter α) {g : filter α} (hg : ne_bot (g ⊓ f)) : ↑f ≤ g :=
 f.le_of_inf_ne_bot $ by rwa inf_comm
 
+lemma inf_ne_bot_iff {f : ultrafilter α} {g : filter α} : ne_bot (↑f ⊓ g) ↔ ↑f ≤ g :=
+⟨le_of_inf_ne_bot f, λ h, (inf_of_le_left h).symm ▸ f.ne_bot⟩
+
+lemma disjoint_iff_not_le {f : ultrafilter α} {g : filter α} : disjoint ↑f g ↔ ¬↑f ≤ g :=
+by rw [← inf_ne_bot_iff, ne_bot_iff, ne.def, not_not, disjoint_iff]
+
 @[simp] lemma compl_not_mem_iff : sᶜ ∉ f ↔ s ∈ f :=
 ⟨λ hsc, le_principal_iff.1 $ f.le_of_inf_ne_bot
   ⟨λ h, hsc $ mem_of_eq_bot$ by rwa compl_compl⟩, compl_not_mem⟩
@@ -92,6 +98,12 @@ 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
 
+@[simp] lemma le_sup_iff {u : ultrafilter α} {f g : filter α} : ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g :=
+not_iff_not.1 $ by simp only [← disjoint_iff_not_le, not_or_distrib, disjoint_sup_right]
+
+@[simp] lemma union_mem_iff : s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f :=
+by simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]
+
 lemma mem_or_compl_mem (f : ultrafilter α) (s : set α) : s ∈ f ∨ sᶜ ∈ f :=
 or_iff_not_imp_left.2 compl_mem_iff_not_mem.2
 
@@ -100,10 +112,7 @@ protected lemma em (f : ultrafilter α) (p : α → Prop) :
 f.mem_or_compl_mem {x | p x}
 
 lemma eventually_or : (∀ᶠ x in f, p x ∨ q x) ↔ (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, q x :=
-⟨λ H, (f.em p).imp_right $ λ hp, (H.and hp).mono $ λ x ⟨hx, hnx⟩, hx.resolve_left hnx,
-  λ H, H.elim (λ hp, hp.mono $ λ x, or.inl) (λ hp, hp.mono $ λ x, or.inr)⟩
-
-lemma union_mem_iff : s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f := eventually_or
+union_mem_iff
 
 lemma eventually_not : (∀ᶠ x in f, ¬p x) ↔ ¬∀ᶠ x in f, p x := compl_mem_iff_not_mem
 
@@ -182,20 +191,22 @@ lemma pure_injective : injective (pure : α → ultrafilter α) :=
 instance [inhabited α] : inhabited (ultrafilter α) := ⟨pure default⟩
 instance [nonempty α] : nonempty (ultrafilter α) := nonempty.map pure infer_instance
 
-lemma eq_pure_of_finite_mem (h : s.finite) (h' : s ∈ f) : ∃ x ∈ s, (f : filter α) = pure x :=
+lemma eq_pure_of_finite_mem (h : s.finite) (h' : s ∈ f) : ∃ x ∈ s, f = pure x :=
 begin
   rw ← bUnion_of_singleton s at h',
   rcases (ultrafilter.finite_bUnion_mem_iff h).mp h' with ⟨a, has, haf⟩,
-  use [a, has],
-  change (f : filter α) = (pure a : ultrafilter α),
-  rw [ultrafilter.coe_inj, ← ultrafilter.coe_le_coe],
-  change (f : filter α) ≤ pure a,
-  rwa [← principal_singleton, le_principal_iff]
+  exact ⟨a, has, eq_of_le (filter.le_pure_iff.2 haf)⟩
 end
 
-lemma eq_pure_of_finite [finite α] (f : ultrafilter α) : ∃ a, (f : filter α) = pure a :=
+lemma eq_pure_of_finite [finite α] (f : ultrafilter α) : ∃ a, f = pure a :=
 (eq_pure_of_finite_mem finite_univ univ_mem).imp $ λ a ⟨_, ha⟩, ha
 
+lemma le_cofinite_or_eq_pure (f : ultrafilter α) : (f : filter α) ≤ cofinite ∨ ∃ a, f = pure a :=
+or_iff_not_imp_left.2 $ λ h,
+  let ⟨s, hs, hfin⟩ := filter.disjoint_cofinite_right.1 (disjoint_iff_not_le.2 h),
+      ⟨a, has, hf⟩ := eq_pure_of_finite_mem hfin hs
+  in ⟨a, hf⟩
+
 /-- Monadic bind for ultrafilters, coming from the one on filters
 defined in terms of map and join.-/
 def bind (f : ultrafilter α) (m : α → ultrafilter β) : ultrafilter β :=

src/topology/noetherian_space.lean

@@ -101,6 +101,17 @@ end
 
 variables {α β}
 
+instance {α} : noetherian_space (cofinite_topology α) :=
+begin
+  simp only [noetherian_space_iff_opens, is_compact_iff_ultrafilter_le_nhds,
+    cofinite_topology.nhds_eq, ultrafilter.le_sup_iff],
+  intros s f hs,
+  rcases f.le_cofinite_or_eq_pure with hf|⟨a, rfl⟩,
+  { rcases filter.nonempty_of_mem (filter.le_principal_iff.1 hs) with ⟨a, ha⟩,
+    exact ⟨a, ha, or.inr hf⟩ },
+  { exact ⟨a, filter.le_principal_iff.mp hs, or.inl le_rfl⟩ }
+end
+
 lemma noetherian_space.is_compact [h : noetherian_space α] (s : set α) : is_compact s :=
 let H := (noetherian_space_tfae α).out 0 2 in H.mp h s