Zulip Chat Archive

Stream: maths

Topic: filter base


view this post on Zulip Yury G. Kudryashov (Jan 14 2020 at 18:25):

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?

view this post on Zulip Yury G. Kudryashov (Jan 14 2020 at 18:35):

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 helper lemmas.

view this post on Zulip Patrick Massot (Jan 14 2020 at 20:56):

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.

view this post on Zulip Yury G. Kudryashov (Jan 14 2020 at 22:04):

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.

view this post on Zulip Patrick Massot (Jan 14 2020 at 22:08):

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

view this post on Zulip Patrick Massot (Jan 14 2020 at 22:09):

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

view this post on Zulip Patrick Massot (Jan 14 2020 at 22:09):

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

view this post on Zulip Mario Carneiro (Jan 14 2020 at 22:59):

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

view this post on Zulip Mario Carneiro (Jan 14 2020 at 22:59):

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


Last updated: May 18 2021 at 06:15 UTC