Zulip Chat Archive

Stream: maths

Topic: free filters and ultrafilters


Bernd Losert (Oct 15 2022 at 10:15):

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

Junyan Xu (Oct 15 2022 at 16:42):

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 (Oct 15 2022 at 17:00):

@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 (Oct 15 2022 at 17:08):

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 (Oct 15 2022 at 17:17):

Thanks! Corrected my post.

Bernd Losert (Oct 15 2022 at 17:38):

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

Junyan Xu (Oct 15 2022 at 17:40):

You're welcome to!

Anatole Dedecker (Oct 15 2022 at 20:00):

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 (Oct 15 2022 at 22:11):

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

Bernd Losert (Oct 16 2022 at 14:44):

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 (Oct 16 2022 at 14:52):

Try dropping the has_mem.mem from the simp call

Ruben Van de Velde (Oct 16 2022 at 14:53):

But maybe the bigger issue is the at this?

Bernd Losert (Oct 16 2022 at 14:57):

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

Bernd Losert (Oct 16 2022 at 14:58):

What's the problem with at this?

Kevin Buzzard (Oct 16 2022 at 15:10):

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

Bernd Losert (Oct 16 2022 at 15:10):

Ah, I see.

Ruben Van de Velde (Oct 16 2022 at 19:49):

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 (Oct 16 2022 at 19:54):

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 (Oct 16 2022 at 20:09):

#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 (Oct 16 2022 at 22:34):

free ultrafilter does not refer to this specific filter.

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

Junyan Xu (Oct 16 2022 at 23:07):

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 (Oct 16 2022 at 23:10):

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

Kyle Miller (Oct 17 2022 at 01:07):

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

Patrick Massot (Oct 17 2022 at 07:05):

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 (Oct 17 2022 at 07:07):

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 (Oct 17 2022 at 15:34):

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 (Oct 17 2022 at 17:34):

Use \in notation, I think.

Junyan Xu (Oct 17 2022 at 17:49):

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 (Oct 17 2022 at 18:14):

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 (Oct 17 2022 at 18:15):

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 (Oct 17 2022 at 23:18):

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

Bernd Losert (Oct 22 2022 at 13:29):

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 (Oct 22 2022 at 13:51):

bornology.of maybe? for consistency

Anatole Dedecker (Oct 22 2022 at 14:32):

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 (Oct 22 2022 at 17:10):

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


Last updated: Dec 20 2023 at 11:08 UTC