Zulip Chat Archive

Stream: maths

Topic: filter bases


view this post on Zulip Patrick Massot (Mar 12 2019 at 15:25):

@Johannes Hölzl Bourbaki is always using filter bases everywhere, and it's been puzzling me forever that this seems to be nowhere in mathlib. In particular I can't find:

import order.filter
open filter set

lemma generate_of_base {α : Type*} {ι : Type*} {s : ι  set α} [inhabited ι]
  (H :  i j,  k, s k  s i  s j) (U : set α): U  generate (range s)   i, s i  U :=
begin
  split ; intro h,
  { induction h with U U_in U V U_gen UV U_union U V U_gen V_gen U_union V_union,
    { rcases U_in with i, rfl,
      use i },
    { use default ι,
      exact (univ_mem_sets : univ  principal (s $ default ι))},
    { cases U_union with i Ui,
      use i,
      exact subset.trans Ui UV },
    { cases U_union with i Ui,
      cases V_union with j Vj,
      cases H i j with k k_sub,
      use k,
      cases subset_inter_iff.1 k_sub with ki kj,
      exact subset_inter_iff.2 subset.trans ki Ui, subset.trans kj Vj }},
  { cases h with i Ui,
    exact generate_sets.superset (generate_sets.basic $ mem_range_self i) Ui },
end

What is the story here? Do you have a better way?

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:27):

I know this is a fake tactic mode proof, but I don't dare writing the proof term...

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:27):

I usually reduce it to the infimum.

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:28):

So nhds is not defined using a generating set, but as a infimum of principal filters. The advantage is that for the infimum very generic rules exist

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:28):

I can also prove that, under the same assumption, generate (range s) = ⨅ i, principal (s i). But what do you gain from expressing it as the RHS?

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:29):

I think the problem is that ⨅ i, principal (s i) is not very nice in general

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:29):

often s is not only indexed by one value, but many values. this fits nicely with infi.

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:29):

You need to take intersections of finite subsets

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:30):

it is not nice if you directly work on sets, instead of on filters.

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:30):

Of course, it is often hard to use filters in their full generality but when we can they are very powerful.

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:31):

I still don't understand why the condition H : ∀ i j, ∃ k, s k ⊆ s i ∩ s j appears nowhere. Whatever the language, things will always be simpler under this assumption, right?

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:31):

This is a directed something assumption

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:32):

Everybody here wants to have more category theory, but nobody is using the complete lattices structure on the filters. But you can see the infi as a nice behaving limit of filters. And many operations commute _somehow_ with infi.

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:32):

principal doesn't commute nicely

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:33):

What you proved is essentially mem_infi

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:33):

tendsto and principal and infi work very nicely together!

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:34):

⨅ i, principal (s i) is not principal (⨅ i, s i), right?

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:34):

Look at these rules: https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean#L1205

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:34):

Look ma no directed proof necessary :-)

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:35):

Ah sorry, I didn't mean prinicpal and infi are commuting. But tendsto and infi are nice behaving

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:35):

But the story of filter bases and sub-bases is precisely the story of ⨅ i, principal (s i) vs generate (range s)

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:37):

Yes, but generate only allows me to construct a filter from sets. While allows me to constructa filter from other filters (hence including sets)

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:39):

Many statements are actually filter inclusion statements. Often they are not seen to be obvious filter inclusions, but when they are then we can use the powerful complete lattice structure.

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:40):

An example is: https://github.com/leanprover-community/mathlib/commit/a4afa904f2e902e34764ff69ec5baf31ad56525a#diff-2f853d294b8568321089942e42ccd7b1L1411
Here the directed proof is completely unnecessary

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:42):

Or this change:
https://github.com/leanprover-community/mathlib/commit/a4afa904f2e902e34764ff69ec5baf31ad56525a#diff-11d4223aa3461ef9e12d2f034e79d0f1R375
Here the same proof which was done before set-wise is now done on filters and their order structure (even when the final goal is to reduce a filer statement to a set statement)

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:42):

What I want to say: generate is much more limited than using infi. With infi we get nice compositional behaviour, and especially for the reduction of tendsto statements it can be very powerful.

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:44):

We can reduce generate to infi but not the other way round

view this post on Zulip Johannes Hölzl (Mar 12 2019 at 15:45):

We can define infi using generate, but then we lose the compositional behaviour

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:53):

Thanks, I'll try to keep all that in mind

view this post on Zulip Patrick Massot (Apr 05 2020 at 12:23):

In mathlib, we have Yury's filter bases which are predicate based, and used in some places, but notably not in topology.bases. In the perfectoid project, we had filter bases everywhere, but we used a much more bundled approach because:

  1. We needed to enforce many properties of our bases
  2. We needed to construct filters starting from a basis having a lot of properties (typically providing a basis for neighborhood of zero in a ring that will ensure there is a topological ring structure inducing that filter).

As a scaled down example, I'd like to discuss the following example:

structure decreasing_enumerated_basis {α : Type*} (f : filter α)  :=
(V :   set α)
(in_filter :  n, V n  f)
(decreasing :  {n m}, n  m  V m  V n)
(basis :  s, s  f   n, V n  s)

instance  {α : Type*} {f : filter α} : has_coe_to_fun (decreasing_enumerated_basis f) :=
⟨_, λ B n, B.V n

lemma decreasing_enumerated_basis.tendsto {α : Type*} {β : Type*} {f : filter α} {g : filter β}
(B : decreasing_enumerated_basis g) (φ : α  β) : tendsto φ f g   n,  x in f, φ x  B n :=
begin
  split ; intro h,
  { intro n,
    exact h (B.in_filter n) },
  { intros s s_in,
    cases (B.basis s).mp s_in with n hn,
    apply mem_sets_of_superset (h n),
    exact preimage_mono hn }
end

lemma decreasing_enumerated_basis.tendsto' {β : Type*} {g : filter β}
(B : decreasing_enumerated_basis g) {φ :   β} (h :  n, φ n  B n) : tendsto φ at_top g :=
begin
  rw B.tendsto,
  intro n,
  rw eventually_at_top,
  use n,
  intros m hm,
  exact B.decreasing hm (h m),
end

def decreasing_enumerated_basis.of_has_countable_basis {α : Type*} {f : filter α}
  (hf : has_countable_basis f) : decreasing_enumerated_basis f :=
...

This setup is very convenient to use because you can apply the function defined at the bottom of this snippet, and access all the lemmas using the dot notation. What do @Sebastien Gouezel and @Yury G. Kudryashov think about this?

view this post on Zulip Sebastien Gouezel (Apr 05 2020 at 13:18):

If this is useful in your specific setup, then go for it! Although I would formulate the third property in your structure using Yury's predicate and call it has_basis, to get all the existing lemmas for bases with B.has_basis.foo.

view this post on Zulip Patrick Massot (Apr 05 2020 at 13:36):

Yes, this is obviously the good solution.

view this post on Zulip Gabriel Ebner (Apr 05 2020 at 14:06):

In January, Yury said that he has already migrated has_countable_basis to the new API and that he's just splitting it up into multiple PRs. https://github.com/leanprover-community/mathlib/pull/1896#issuecomment-576681341

view this post on Zulip Patrick Massot (Apr 05 2020 at 14:19):

Actually maybe an even better solution would be to wrap filter.has_basis into a structure and have more specific basis extending it. That would save a couple of restatements.

view this post on Zulip Patrick Massot (Apr 05 2020 at 21:08):

@Yury G. Kudryashov and @Sebastien Gouezel I'd like comments on WIP at https://github.com/leanprover-community/mathlib/commit/94701f1a9f33abbeb17894929d567affd42e2267. There I did three things: first I removed the filter countable basis stuff from topology.bases and put it in order.filter.bases, next to filter.has_basis where I can be later refactord. Then I added my decreasing_enumerated_basis, in the same file. And then my end goal in this story is what I added in topology.sequences. There is general stuff about subsequences, the high scores stuff and the final lemma which was the end-goal:

variables {X : Type*} [topological_space X] [first_countable_topology X]

lemma compact.tendsto_subseq {s : set X} {u :   X}
  (hs : compact s) (hu :  n, u n  s) :
 (x  s) (φ :   ), strict_mono φ  tendsto (u  φ) at_top (𝓝 x) :=
hs.tendsto_subseq' (univ_mem_sets' hu)

I still need to clean a bit the last file, but I'd like to read at least comments about the reorganization stuff, and naming suggestions.

view this post on Zulip Patrick Massot (Apr 05 2020 at 21:12):

The next step will be to hook this to Sébastien's proper metric space thing to actually get Bolzano-Weirstrass.

view this post on Zulip Yury G. Kudryashov (Apr 05 2020 at 23:27):

@Gabriel Ebner I'm afraid that I've accidentally deleted this part (messed up with git stashes). So far @Patrick Massot 's approach looks very good. I think that has_countable_basis should become nonempty (decreasing_enumerated_basis f) if we want it in Prop. BTW, I'd turn it into a class because in many cases (at_top on nat, nhds in an emetric_space) it can be deduced automatically.

view this post on Zulip Gabriel Ebner (Apr 06 2020 at 11:42):

I don't think we make any use of the fact that has_countable_basis is in Prop. It is only used as a hypothesis for lemmas. So I'd say we can replace has_countable_basis by decreasing_enumerated_basis directly. Although the name is quite a mouthful.

view this post on Zulip Patrick Massot (Apr 06 2020 at 12:00):

has_countable_basis is still easier to check in principle, and also what is in the traditional sources.

view this post on Zulip Patrick Massot (Apr 06 2020 at 12:00):

Long names are hard to avoid, especially since we don't want cryptic abreviations.


Last updated: May 11 2021 at 16:22 UTC