filter base

Stream: maths

[Yury G. Kudryashov]

Hi, many simplification lemmas about filters can be formulated in terms of

def filter.has_base {α : Type*} {ι : Sort*} (f : filter α) (s : ι → set α) : Prop :=
∀ {{t : set α}}, t ∈ f <-> ∃ i, s i ⊆ t

I use s : ι → set α instead of set (set α) because usually this base is a range of a function. This property is stronger than f = infi (principal ∘ s), and immediately implies statements like tendsto m f f' → f.has_base s → ∀ t ∈ f', ∃ i, s i ⊆ m ⁻¹' t, and similarly for f'.
What do you think about adding it to mathlib?

[Yury G. Kudryashov]

A possible application: we can prove that various families (open balls, closed balls, same with rational r, same with r=n⁻¹) form bases of nhds x in an emetric/metric space, then use these lemmas in rewrites without proving N² helper lemmas.

[Patrick Massot]

We already had this need in the perfectoid project, but it's among the many things that should be PRed but are not. We also tried several implementations and I'm super happy with the one we currently have. See https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/filter.lean#L82 and the rest of that file, as well as https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/topological_groups.lean, https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/topological_rings.lean etc. One difficulty is to make something that we can easily use in more specialized situation without rewriting all lemmas to make them really usable.

[Yury G. Kudryashov]

Why did you choose to have a separate type instead of a predicate? I think that usually we already have a filter and want to rewrite some tendsto in a more reasonable way.

[Patrick Massot]

That's not the case in the perfectoid project. The filter base comes first, then the filter and then the topology.

[Patrick Massot]

See https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/valuation/topology.lean

[Patrick Massot]

But I didn't find a nice way to cover all use cases.

[Mario Carneiro]

Isn't there already a filter.generate function for generating a filter from a filter (sub)base?

[Mario Carneiro]

I can certainly see the use in a has_base predicate for saying that a filter is generated by a base other than the one used in its definition though