Ultrafilters

An ultrafilter is a minimal (maximal in the set order) proper filter. In this file we define

is_ultrafilter: a predicate stating that a given filter is an ultrafiler;
ultrafilter_of: an ultrafilter that is less than or equal to a given filter;
ultrafilter: subtype of ultrafilters;
ultrafilter.pure: pure x as an ultrafiler;
ultrafilter.map, ultrafilter.bind : operations on ultrafilters;
hyperfilter: the ultra-filter extending the cofinite filter.

source

def filter.is_ultrafilter {α : Type u} :

filter α → Prop

An ultrafilter is a minimal (maximal in the set order) proper filter.

Equations

f.is_ultrafilter = (f.ne_bot ∧ ∀ (g : filter α), g.ne_bot → g ≤ f → f ≤ g)

source

theorem filter.is_ultrafilter.unique {α : Type u} {f g : filter α} :

g.is_ultrafilter → f.ne_bot → f ≤ g → f = g

source

theorem filter.le_of_ultrafilter {α : Type u} {f g : filter α} :

f.is_ultrafilter → (g ⊓ f).ne_bot → f ≤ g

source

theorem filter.ultrafilter_iff_compl_mem_iff_not_mem {α : Type u} {f : filter α} :

f.is_ultrafilter ↔ ∀ (s : set α), sᶜ ∈ f ↔ s ∉ f

Equivalent characterization of ultrafilters: A filter f is an ultrafilter if and only if for each set s, -s belongs to f if and only if s does not belong to f.

source

theorem filter.mem_or_compl_mem_of_ultrafilter {α : Type u} {f : filter α} (hf : f.is_ultrafilter) (s : set α) :

s ∈ f ∨ sᶜ ∈ f

source

theorem filter.mem_or_mem_of_ultrafilter {α : Type u} {f : filter α} {s t : set α} :

f.is_ultrafilter → s ∪ t ∈ f → s ∈ f ∨ t ∈ f

source

theorem filter.is_ultrafilter.em {α : Type u} {f : filter α} (hf : f.is_ultrafilter) (p : α → Prop) :

(∀ᶠ (x : α) in f, p x) ∨ ∀ᶠ (x : α) in f, ¬p x

source

theorem filter.is_ultrafilter.eventually_or {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p q : α → Prop} :

(∀ᶠ (x : α) in f, p x ∨ q x) ↔ (∀ᶠ (x : α) in f, p x) ∨ ∀ᶠ (x : α) in f, q x

source

theorem filter.is_ultrafilter.eventually_not {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p : α → Prop} :

(∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, p x

source

theorem filter.is_ultrafilter.eventually_imp {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p q : α → Prop} :

(∀ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, q x)

source

theorem filter.mem_of_finite_sUnion_ultrafilter {α : Type u} {f : filter α} {s : set (set α)} :

f.is_ultrafilter → s.finite → ⋃₀s ∈ f → (∃ (t : set α) (H : t ∈ s), t ∈ f)

source

theorem filter.mem_of_finite_Union_ultrafilter {α : Type u} {β : Type v} {f : filter α} {is : set β} {s : β → set α} :

f.is_ultrafilter → is.finite → (⋃ (i : β) (H : i ∈ is), s i) ∈ f → (∃ (i : β) (H : i ∈ is), s i ∈ f)

source

theorem filter.ultrafilter_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :

f.is_ultrafilter → (filter.map m f).is_ultrafilter

source

theorem filter.ultrafilter_pure {α : Type u} {a : α} :

(has_pure.pure a).is_ultrafilter

source

theorem filter.ultrafilter_bind {α : Type u} {β : Type v} {f : filter α} (hf : f.is_ultrafilter) {m : α → filter β} :

(∀ (a : α), (m a).is_ultrafilter) → (f.bind m).is_ultrafilter

source

theorem filter.exists_ultrafilter {α : Type u} (f : filter α) [h : f.ne_bot] :

∃ (u : filter α), u ≤ f ∧ u.is_ultrafilter

The ultrafilter lemma: Any proper filter is contained in an ultrafilter.

source

def filter.ultrafilter_of {α : Type u} :

filter α → filter α

Construct an ultrafilter extending a given filter. The ultrafilter lemma is the assertion that such a filter exists; we use the axiom of choice to pick one.

Equations