Ultrafilters #

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

Ultrafilter.of: an ultrafilter that is less than or equal to a given filter;
Ultrafilter: subtype of ultrafilters;
pure x : Ultrafilter α: pure x as an ultrafiler;
Ultrafilter.map, Ultrafilter.bind, Ultrafilter.comap : operations on ultrafilters;
hyperfilter: the ultrafilter extending the cofinite filter.

instance instIsAtomicFilterInstPartialOrderFilterToOrderBotToLEToPreorderToBoundedOrderInstCompleteLatticeFilter {α : Type u} :

IsAtomic (Filter α)

Filter α is an atomic type: for every filter there exists an ultrafilter that is less than or equal to this filter.

Equations

One or more equations did not get rendered due to their size.

source

ink

structure Ultrafilter (α : Type u_1) extends Filter :

Type u_1

An ultrafilter is nontrivial.
neBot' : Filter.NeBot toFilter
If g is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater than or equal to the ultrafilter.
le_of_le : ∀ (g : Filter α), Filter.NeBot g → g ≤ toFilter → toFilter ≤ g

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

Instances For

source

ink

instance Ultrafilter.instCoeTCUltrafilterFilter {α : Type u} :

CoeTC (Ultrafilter α) (Filter α)

Equations

Ultrafilter.instCoeTCUltrafilterFilter = { coe := Ultrafilter.toFilter }

source

ink

instance Ultrafilter.instMembershipSetUltrafilter {α : Type u} :

Membership (Set α) (Ultrafilter α)

Equations

Ultrafilter.instMembershipSetUltrafilter = { mem := fun s f => s ∈ ↑f }

source

ink

theorem Ultrafilter.unique {α : Type u} (f : Ultrafilter α) {g : Filter α} (h : g ≤ ↑f) (hne : autoParam (Filter.NeBot g) _auto✝) :

g = ↑f

source

ink

instance Ultrafilter.neBot {α : Type u} (f : Ultrafilter α) :

Filter.NeBot ↑f

Equations

@Ultrafilter.neBot = @Ultrafilter.neBot.proof_1

source

ink

theorem Ultrafilter.isAtom {α : Type u} (f : Ultrafilter α) :

IsAtom ↑f

source

ink

@[simp]

theorem Ultrafilter.mem_coe {α : Type u} {f : Ultrafilter α} {s : Set α} :

s ∈ ↑f ↔ s ∈ f

source

ink

theorem Ultrafilter.coe_injective {α : Type u} :

Function.Injective Ultrafilter.toFilter

source

ink

theorem Ultrafilter.eq_of_le {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} (h : ↑f ≤ ↑g) :

f = g

source

ink

@[simp]

theorem Ultrafilter.coe_le_coe {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} :

↑f ≤ ↑g ↔ f = g

source

ink

@[simp]

theorem Ultrafilter.coe_inj {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} :

↑f = ↑g ↔ f = g

source

ink

theorem Ultrafilter.ext {α : Type u} ⦃f : Ultrafilter α⦄ ⦃g : Ultrafilter α⦄ (h : ∀ (s : Set α), s ∈ f ↔ s ∈ g) :

f = g

source

ink

theorem Ultrafilter.le_of_inf_neBot {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : Filter.NeBot (↑f ⊓ g)) :

↑f ≤ g

source

ink

theorem Ultrafilter.le_of_inf_neBot' {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : Filter.NeBot (g ⊓ ↑f)) :

↑f ≤ g

source

ink

theorem Ultrafilter.inf_neBot_iff {α : Type u} {f : Ultrafilter α} {g : Filter α} :

Filter.NeBot (↑f ⊓ g) ↔ ↑f ≤ g

source

ink

theorem Ultrafilter.disjoint_iff_not_le {α : Type u} {f : Ultrafilter α} {g : Filter α} :

Disjoint (↑f) g ↔ ¬↑f ≤ g

source

ink

@[simp]

theorem Ultrafilter.compl_not_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set α} :

¬sᶜ ∈ f ↔ s ∈ f

source

ink

@[simp]

theorem Ultrafilter.frequently_iff_eventually {α : Type u} {f : Ultrafilter α} {p : α → Prop} :

Filter.Frequently (fun x => p x) ↑f ↔ Filter.Eventually (fun x => p x) ↑f

source

ink

theorem Filter.Frequently.eventually {α : Type u} {f : Ultrafilter α} {p : α → Prop} :

Filter.Frequently (fun x => p x) ↑f → Filter.Eventually (fun x => p x) ↑f

Alias of the forward direction of Ultrafilter.frequently_iff_eventually.

source

ink

theorem Ultrafilter.compl_mem_iff_not_mem {α : Type u} {f : Ultrafilter α} {s : Set α} :

sᶜ ∈ f ↔ ¬s ∈ f

source

ink

theorem Ultrafilter.diff_mem_iff {α : Type u} {s : Set α} {t : Set α} (f : Ultrafilter α) :

s \ t ∈ f ↔ s ∈ f ∧ ¬t ∈ f

source

ink

def Ultrafilter.ofComplNotMemIff {α : Type u} (f : Filter α) (h : ∀ (s : Set α), ¬sᶜ ∈ f ↔ s ∈ f) :

Ultrafilter α

If sᶜ ∉ f ↔ s ∈ f∉ f ↔ s ∈ f↔ s ∈ f∈ f, then f is an ultrafilter. The other implication is given by Ultrafilter.compl_not_mem_iff.

Equations

Ultrafilter.ofComplNotMemIff f h = { toFilter := f, neBot' := (_ : Filter.NeBot f), le_of_le := (_ : ∀ (g : Filter α), Filter.NeBot g → g ≤ f → ∀ (s : Set α), s ∈ g → s ∈ f) }

source

ink

def Ultrafilter.ofAtom {α : Type u} (f : Filter α) (hf : IsAtom f) :

Ultrafilter α

If f : Filter α is an atom, then it is an ultrafilter.

Equations

Ultrafilter.ofAtom f hf = { toFilter := f, neBot' := (_ : Filter.NeBot f), le_of_le := (_ : ∀ (g : Filter α), Filter.NeBot g → g ≤ f → f ≤ g) }

source

ink

theorem Ultrafilter.nonempty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s ∈ f) :

Set.Nonempty s

source

ink

theorem Ultrafilter.ne_empty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s ∈ f) :

s ≠ ∅

source

ink

@[simp]

theorem Ultrafilter.empty_not_mem {α : Type u} {f : Ultrafilter α} :

¬∅ ∈ f

source

ink

@[simp]

theorem Ultrafilter.le_sup_iff {α : Type u} {u : Ultrafilter α} {f : Filter α} {g : Filter α} :

↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g

source

ink

@[simp]

theorem Ultrafilter.union_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set α} {t : Set α} :

s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

source

ink

theorem Ultrafilter.mem_or_compl_mem {α : Type u} (f : Ultrafilter α) (s : Set α) :

s ∈ f ∨ sᶜ ∈ f

source

ink

theorem Ultrafilter.em {α : Type u} (f : Ultrafilter α) (p : α → Prop) :

Filter.Eventually (fun x => p x) ↑f ∨ Filter.Eventually (fun x => ¬p x) ↑f

source

ink

theorem Ultrafilter.eventually_or {α : Type u} {f : Ultrafilter α} {p : α → Prop} {q : α → Prop} :

Filter.Eventually (fun x => p x ∨ q x) ↑f ↔ Filter.Eventually (fun x => p x) ↑f ∨ Filter.Eventually (fun x => q x) ↑f

source

ink

theorem Ultrafilter.eventually_not {α : Type u} {f : Ultrafilter α} {p : α → Prop} :

Filter.Eventually (fun x => ¬p x) ↑f ↔ ¬Filter.Eventually (fun x => p x) ↑f

source

ink

theorem Ultrafilter.eventually_imp {α : Type u} {f : Ultrafilter α} {p : α → Prop} {q : α → Prop} :

Filter.Eventually (fun x => p x → q x) ↑f ↔ Filter.Eventually (fun x => p x) ↑f → Filter.Eventually (fun x => q x) ↑f

source

ink

theorem Ultrafilter.finite_unionₛ_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set (Set α)} (hs : Set.Finite s) :

⋃₀ s ∈ f ↔ ∃ t, t ∈ s ∧ t ∈ f

source

ink

theorem Ultrafilter.finite_bunionᵢ_mem_iff {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {s : β → Set α} (his : Set.Finite is) :

(Set.unionᵢ fun i => Set.unionᵢ fun h => s i) ∈ f ↔ ∃ i, i ∈ is ∧ s i ∈ f

source

ink

def Ultrafilter.map {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α) :

Ultrafilter β

Pushforward for ultrafilters.

Equations

Ultrafilter.map m f = Ultrafilter.ofComplNotMemIff (Filter.map m ↑f) (_ : ∀ (s : Set β), ¬(m ⁻¹' s)ᶜ ∈ f ↔ m ⁻¹' s ∈ f)

source

ink

@[simp]

theorem Ultrafilter.coe_map {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α) :

↑(Ultrafilter.map m f) = Filter.map m ↑f

source

ink

@[simp]

theorem Ultrafilter.mem_map {α : Type u} {β : Type v} {m : α → β} {f : Ultrafilter α} {s : Set β} :

s ∈ Ultrafilter.map m f ↔ m ⁻¹' s ∈ f

source

ink

@[simp]

theorem Ultrafilter.map_id {α : Type u} (f : Ultrafilter α) :

Ultrafilter.map id f = f

source

ink

@[simp]

theorem Ultrafilter.map_id' {α : Type u} (f : Ultrafilter α) :

Ultrafilter.map (fun x => x) f = f

source

ink

@[simp]

theorem Ultrafilter.map_map {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter α) (m : α → β) (n : β → γ) :

Ultrafilter.map n (Ultrafilter.map m f) = Ultrafilter.map (n ∘ m) f

source

ink

def Ultrafilter.comap {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) :

Ultrafilter α

The pullback of an ultrafilter along an injection whose range is large with respect to the given ultrafilter.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Ultrafilter.mem_comap {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) {s : Set α} :

s ∈ Ultrafilter.comap u inj large ↔ m '' s ∈ u

source

ink

@[simp]

theorem Ultrafilter.coe_comap {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) :

↑(Ultrafilter.comap u inj large) = Filter.comap m ↑u

source

ink

@[simp]

theorem Ultrafilter.comap_id {α : Type u} (f : Ultrafilter α) (h₀ : optParam (Function.Injective id) (_ : Function.Injective id)) (h₁ : optParam (Set.range id ∈ f) (_ : Set.range id ∈ f)) :

Ultrafilter.comap f h₀ h₁ = f

source

ink

@[simp]

theorem Ultrafilter.comap_comap {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter γ) {m : α → β} {n : β → γ} (inj₀ : Function.Injective n) (large₀ : Set.range n ∈ f) (inj₁ : Function.Injective m) (large₁ : Set.range m ∈ Ultrafilter.comap f inj₀ large₀) (inj₂ : optParam (Function.Injective (n ∘ m)) (_ : Function.Injective (n ∘ m))) (large₂ : optParam (Set.range (n ∘ m) ∈ f) (_ : Set.range (n ∘ m) ∈ f)) :

Ultrafilter.comap (Ultrafilter.comap f inj₀ large₀) inj₁ large₁ = Ultrafilter.comap f inj₂ large₂

source

ink

instance Ultrafilter.instPureUltrafilter :

Pure Ultrafilter

The principal ultrafilter associated to a point x.

Equations

Ultrafilter.instPureUltrafilter = { pure := fun {α} a => Ultrafilter.ofComplNotMemIff (pure a) (_ : ∀ (s : Set α), ¬sᶜ ∈ pure a ↔ s ∈ pure a) }

source

ink

@[simp]

theorem Ultrafilter.mem_pure {α : Type u} {a : α} {s : Set α} :

s ∈ pure a ↔ a ∈ s

source

ink

@[simp]

theorem Ultrafilter.coe_pure {α : Type u} (a : α) :

↑(pure a) = pure a

source

ink

@[simp]

theorem Ultrafilter.map_pure {α : Type u} {β : Type v} (m : α → β) (a : α) :

Ultrafilter.map m (pure a) = pure (m a)

source

ink

@[simp]

theorem Ultrafilter.comap_pure {α : Type u} {β : Type v} {m : α → β} (a : α) (inj : Function.Injective m) (large : Set.range m ∈ pure (m a)) :

Ultrafilter.comap (pure (m a)) inj large = pure a

source

ink

theorem Ultrafilter.pure_injective {α : Type u} :

Function.Injective pure

source

ink

instance Ultrafilter.instInhabitedUltrafilter {α : Type u} [inst : Inhabited α] :

Inhabited (Ultrafilter α)

Equations

Ultrafilter.instInhabitedUltrafilter = { default := pure default }

source

ink

instance Ultrafilter.instNonemptyUltrafilter {α : Type u} [inst : Nonempty α] :

Nonempty (Ultrafilter α)

Equations

@Ultrafilter.instNonemptyUltrafilter = @Ultrafilter.instNonemptyUltrafilter.proof_1

source

ink

theorem Ultrafilter.eq_pure_of_finite_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (h : Set.Finite s) (h' : s ∈ f) :

∃ x, x ∈ s ∧ f = pure x

source

ink

theorem Ultrafilter.eq_pure_of_finite {α : Type u} [inst : Finite α] (f : Ultrafilter α) :

∃ a, f = pure a

source

ink

theorem Ultrafilter.le_cofinite_or_eq_pure {α : Type u} (f : Ultrafilter α) :

↑f ≤ Filter.cofinite ∨ ∃ a, f = pure a

source

ink

def Ultrafilter.bind {α : Type u} {β : Type v} (f : Ultrafilter α) (m : α → Ultrafilter β) :

Ultrafilter β

Monadic bind for ultrafilters, coming from the one on filters defined in terms of map and join.

Equations

Ultrafilter.bind f m = Ultrafilter.ofComplNotMemIff (Filter.bind ↑f fun x => ↑(m x)) (_ : ∀ (s : Set β), (¬sᶜ ∈ Filter.bind ↑f fun x => ↑(m x)) ↔ s ∈ Filter.bind ↑f fun x => ↑(m x))

source

ink

instance Ultrafilter.instBind :

Bind Ultrafilter

Equations

Ultrafilter.instBind = { bind := @Ultrafilter.bind }

source

ink

instance Ultrafilter.functor :

Functor Ultrafilter

Equations

Ultrafilter.functor = { map := @Ultrafilter.map, mapConst := fun {α β} => Ultrafilter.map ∘ Function.const β }

source

ink

instance Ultrafilter.monad :

Monad Ultrafilter

Equations

Ultrafilter.monad = Monad.mk

source

ink

instance Ultrafilter.lawfulMonad :

LawfulMonad Ultrafilter

Equations

Ultrafilter.lawfulMonad = Ultrafilter.lawfulMonad.proof_1

source

ink

theorem Ultrafilter.exists_le {α : Type u} (f : Filter α) [h : Filter.NeBot f] :

∃ u, ↑u ≤ f

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

source

ink

theorem Filter.exists_ultrafilter_le {α : Type u} (f : Filter α) [h : Filter.NeBot f] :

∃ u, ↑u ≤ f

Alias of Ultrafilter.exists_le.

source

ink

noncomputable def Ultrafilter.of {α : Type u} (f : Filter α) [inst : Filter.NeBot f] :

Ultrafilter α

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