## Stream: maths

### Topic: filter bases

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

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

#### Johannes Hölzl (Mar 12 2019 at 15:27):

I usually reduce it to the infimum.

#### 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

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

#### Patrick Massot (Mar 12 2019 at 15:29):

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

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

#### Patrick Massot (Mar 12 2019 at 15:29):

You need to take intersections of finite subsets

#### Johannes Hölzl (Mar 12 2019 at 15:30):

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

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

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

#### Patrick Massot (Mar 12 2019 at 15:31):

This is a directed something assumption

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

#### Patrick Massot (Mar 12 2019 at 15:32):

principal doesn't commute nicely

#### Johannes Hölzl (Mar 12 2019 at 15:33):

What you proved is essentially mem_infi

#### Johannes Hölzl (Mar 12 2019 at 15:33):

tendsto and principal and infi work very nicely together!

#### Patrick Massot (Mar 12 2019 at 15:34):

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

#### Johannes Hölzl (Mar 12 2019 at 15:34):

Look ma no directed proof necessary :-)

#### 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

#### 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)

#### 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)

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

#### Johannes Hölzl (Mar 12 2019 at 15:40):

Here the directed proof is completely unnecessary

#### Johannes Hölzl (Mar 12 2019 at 15:42):

Or this change:
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 (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.

#### Johannes Hölzl (Mar 12 2019 at 15:44):

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

#### Johannes Hölzl (Mar 12 2019 at 15:45):

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

#### Patrick Massot (Mar 12 2019 at 15:53):

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

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

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

#### Patrick Massot (Apr 05 2020 at 13:36):

Yes, this is obviously the good solution.

#### 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

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

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

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

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

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

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

#### 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