filter bases

Stream: maths

[Patrick Massot]

@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?

[Patrick Massot]

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

[Johannes Hölzl]

I usually reduce it to the infimum.

[Johannes Hölzl]

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

[Patrick Massot]

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?

[Patrick Massot]

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

[Johannes Hölzl]

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

[Patrick Massot]

You need to take intersections of finite subsets

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Patrick Massot]

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?

[Patrick Massot]

This is a directed something assumption

[Johannes Hölzl]

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.

[Patrick Massot]

principal doesn't commute nicely

[Johannes Hölzl]

What you proved is essentially mem_infi

[Johannes Hölzl]

tendsto and principal and infi work very nicely together!

[Patrick Massot]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

Look ma no directed proof necessary :-)

[Johannes Hölzl]

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

[Patrick Massot]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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.

[Johannes Hölzl]

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

[Johannes Hölzl]

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)

[Johannes Hölzl]

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.

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Patrick Massot]

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

[Patrick Massot]

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?

[Sebastien Gouezel]

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.

[Patrick Massot]

Yes, this is obviously the good solution.

[Gabriel Ebner]

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

[Patrick Massot]

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.

[Patrick Massot]

@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.

[Patrick Massot]

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

[Yury G. Kudryashov]

@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.

[Gabriel Ebner]

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.

[Patrick Massot]

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

[Patrick Massot]

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