free filters and ultrafilters

Stream: maths

[Bernd Losert]

Does mathlib have stuff on free filters? The only thing I see is this about filter.hyperfilter.

[Junyan Xu]

I can't find it but on an infinite type, a filter F is free iff docs#filter.cofinite (the Frechet filter) is contained in it (in mathlib notation, F ≤ filter.cofinite). It seems to me that docs#filter.principalpure is a Galois insertion from set X to filter X with adjoint given by taking intersection of all sets in a filter, which is apparently also missing in mathlib.

[Kyle Miller]

@Junyan Xu Do you mean docs#filter.has_pure? That one is for X -> filter X, but I think docs#filter.principal is what corresponds to the adjunction between set X and filter X. The adjoint is known as the kernel of a filter, and I haven't seen it in mathlib.

[Kyle Miller]

Incidentally, I sometimes wish that docs#nhds were defined to be a function set X -> filter X such that 𝓝 s is the infimum of all the principal filters for open sets containing s. That way we'd have parallelism between 𝓟 s for plain filters and 𝓝 s for open filters.

One application is that you can consider germs of continuous functions at arbitrary subsets s of a topological space, with the understanding that you're using (the open sets in) 𝓝 s for the directed system.

[Junyan Xu]

Thanks! Corrected my post.

[Bernd Losert]

So, should I takee this as an opportunity to open some PRs?

[Junyan Xu]

You're welcome to!

[Anatole Dedecker]

Kyle Miller said:

Incidentally, I sometimes wish that docs#nhds were defined to be a function set X -> filter X such that 𝓝 s is the infimum of all the principal filters for open sets containing s.

We have this as docs#nhds_set

[Bernd Losert]

I will rename hyperfilter to free_ultrafilter since this terminology is standard.

[Bernd Losert]

So I'm trying to prove the following:

lemma free_ultrafilter_is_free : ⋂₀ (free_ultrafilter α).sets = ∅ :=
begin
  by_contra hcontra,
  rw [← ne.def, ne_empty_iff_nonempty] at hcontra,
  obtain ⟨x, hmem⟩ := hcontra,
  have hle : ↑(free_ultrafilter α) ≤ pure x, sorry,
  have heq : ↑(free_ultrafilter α) = pure x,
    from (free_ultrafilter α).ne_bot.le_pure_iff.mp hle,
  haveI hcofinite : ({x} : set α)ᶜ.finite, from
  begin
    have : x ∈ ({x} : set α), by tauto,
    simp [← filter.mem_pure, ← heq, free_ultrafilter, cofinite, has_mem.mem] at this,
    -- STUCK HERE
  end,
  haveI oops : ({x} : set α)ᶜ.infinite := sorry,
  exact not_finite ({x} : set α)ᶜ,
end

In the STUCK HERE part, I see this: {x} x in the tactic goal window. I don't know what to make of this. Any tips?

[Ruben Van de Velde]

Try dropping the has_mem.mem from the simp call

[Ruben Van de Velde]

But maybe the bigger issue is the at this?

[Bernd Losert]

Yes, I can drop the has_mem.mem, but how do I make it simp to ({x} : set α)ᶜ.finite ?

[Bernd Losert]

What's the problem with at this?

[Kevin Buzzard]

this : {x} x might well mean the useless x \in {x} because a set is implemented as a function.

[Bernd Losert]

Ah, I see.

[Ruben Van de Velde]

Oh, I was trying to take a look now that I'm at lean, but there seems to be a lot of code missing

[Patrick Massot]

Bernd Losert said:

I will rename hyperfilter to free_ultrafilter since this terminology is standard.

I don't understand that claim. Do you have any reference. I don't like the name hyperfilter, but for me free ultrafilter does not refer to this specific filter.

[Ruben Van de Velde]

#mwe:

import order.filter.ultrafilter

open filter set

variables {α : Type*} [infinite α]

lemma hyperfilter_is_free : ⋂₀ (hyperfilter α).sets = ∅ :=
begin
  by_contra hcontra,
  rw [← ne.def, ne_empty_iff_nonempty] at hcontra,
  obtain ⟨x, hmem⟩ := hcontra,
  have hle : ↑(hyperfilter α) ≤ pure x, sorry,
  have heq : ↑(hyperfilter α) = pure x,
    from (hyperfilter α).ne_bot.le_pure_iff.mp hle,
  have hcofinite : ({x} : set α)ᶜ.finite, from
  begin
    have mem_singleton : x ∈ ({x} : set α) := mem_singleton x,
    simp only [←filter.mem_pure, ←heq, ultrafilter.mem_coe] at mem_singleton,
    -- ⊢ {x} ∈ hyperfilter α → {x}ᶜ.finite
    sorry,
  end,
  have oops : ({x} : set α)ᶜ.infinite := sorry,
  exact oops hcofinite,
end

And this is where my (nonexistent) knowledge of filters runs out - it seems like the definition of a hyperfilter is basically the other direction

[Junyan Xu]

free ultrafilter does not refer to this specific filter.

I think docs#hyperfilter is just an arbitrarily chosen free ultrafilter?

[Junyan Xu]

Here's an easy proof:

import order.filter.ultrafilter --import order.filter.cofinite suffices for the theorem

namespace filter

theorem sInter_sets_eq_empty_iff_le_cofinite {α} (F : filter α) : ⋂₀ F.sets = ∅ ↔ F ≤ cofinite :=
begin -- doesn't require infiniteness
  rw [set.sInter_eq_empty_iff, le_cofinite_iff_compl_singleton_mem],
  refine ⟨λ h a, _, λ h a, ⟨_, h a, λ h, h rfl⟩⟩,
  obtain ⟨s, hs, ha⟩ := h a,
  exact mem_of_superset hs (λ b hb, ne_of_mem_of_not_mem hb ha),
end

lemma hyperfilter_is_free {α} [infinite α] : ⋂₀ (hyperfilter α).sets = ∅ :=
by { rw sInter_sets_eq_empty_iff_le_cofinite, exact hyperfilter_le_cofinite }

end filter

[Junyan Xu]

So now I'm not sure that free should be a separate definition, since it's always equivalent to F ≤ cofinite.

[Kyle Miller]

I was wondering where the name came from, and the hyperfilter was introduced back in mathlib#801 for the hyperreals.

[Patrick Massot]

Junyan Xu said:

free ultrafilter does not refer to this specific filter.

I think docs#hyperfilter is just an arbitrarily chosen free ultrafilter?

Yes it is. So it's not a specific ultrafilter at all.

[Patrick Massot]

Junyan Xu said:

Here's an easy proof:

import order.filter.ultrafilter --import order.filter.cofinite suffices for the theorem

namespace filter

theorem sInter_sets_eq_empty_iff_le_cofinite {α} (F : filter α) : ⋂₀ F.sets = ∅ ↔ F ≤ cofinite :=
begin -- doesn't require infiniteness
  rw [set.sInter_eq_empty_iff, le_cofinite_iff_compl_singleton_mem],
  refine ⟨λ h a, _, λ h a, ⟨_, h a, λ h, h rfl⟩⟩,
  obtain ⟨s, hs, ha⟩ := h a,
  exact mem_of_superset hs (λ b hb, ne_of_mem_of_not_mem hb ha),
end

lemma hyperfilter_is_free {α} [infinite α] : ⋂₀ (hyperfilter α).sets = ∅ :=
by { rw sInter_sets_eq_empty_iff_le_cofinite, exact hyperfilter_le_cofinite }

end filter

Please don't PR that statement since the wording ⋂₀ F.sets badly breaks the API barrier for filters.

[Junyan Xu]

Patrick Massot said:

Please don't PR that statement since the wording ⋂₀ F.sets badly breaks the API barrier for filters.

I don't understand why docs#filter.supr_sets_eq, docs#filter.sInter_comap_sets etc. are allowed but this isn't. Any other options for writing down the same thing?

[Yaël Dillies]

Use \in notation, I think.

[Junyan Xu]

You could state

example {α} (F : filter α) : (∀ a, ∃ s ∈ F, a ∉ s) ↔ F ≤ cofinite :=

and then in the proof you needn't rewrite by docs#set.sInter_eq_empty_iff, but it's not the same statement (not even defeq), only equivalent, in my opinion.

[Patrick Massot]

The easy fix is to state ⋂₀ {U | U ∈ F} = ∅ ↔ F ≤ cofinite which is defeq to your statement, so it has the same proof.

[Patrick Massot]

A statement that is much more in the spirit of mathlib, but not obviously equivalent to yours is:

theorem forall_finite_iff_le_cofinite {α} (F : filter α) : (∀ s : set α, s.finite → ∀ᶠ x in F, x ∉ s) ↔ F ≤ cofinite :=
⟨λ h, le_cofinite_iff_compl_singleton_mem.mpr (λ x, h _ ({x} : set α).to_finite),
 λ h s hs, hs.eventually_cofinite_nmem.filter_mono h⟩

[Yaël Dillies]

Also let me tell you that all this is secretly about docs#bornology

[Bernd Losert]

I never realized there was a connection with bornology. In any case, I need to talk about free filters, i.e. those satisfying ⋂₀ {U | U ∈ F} = ∅ and I need to be able to choose a free ultrafilter finer than a given filter. I'm not sure what the best API design for this is. Should I add something likefree_ultrafilter.of like we have with ultrafilter.of?

[Yaël Dillies]

bornology.of maybe? for consistency

[Anatole Dedecker]

Yaël Dillies said:

bornology.of maybe? for consistency

I don't like that, this doesn't tell you at all that this is about ultrafilters (and not just filters). Besides, we should really not use docs#bornology as a way of talking about filters smaller than docs#filter.cofinite. Describing a bornology as a filter is a nice implementation trick and we should absolutely abuse it when talking about bornologies, but not the other way around. Also, I still think we should remove the "smaller than docs#cofinite" condition for bornology, so please don't use it as a "filter smaller than cofinite" definition

[Bernd Losert]

Agree. I don't want to have to invoke the technology of bornologies just to get a free ultrafilter.