order on filter

Stream: new members

[Kenny Lau]

Why is the order on filter reverse inclusion instead of just inclusion?

[Mario Carneiro]

@Johannes Hölzl will know. I +1 this question, it throws me off every time

[Kevin Buzzard]

I just assumed it was because the set of subsets of X embeds into the set of filters on X via principal filters, and the smaller the subset the bigger the filter.

[Kenny Lau]

interesting

[Mario Carneiro]

Here is one way to look at it: the identity function is continuous on topologies when the topologies are dom <= cod. In other words, the poset of topologies is embedded in the category of topological spaces by the functor T -> (X,T)

[Mario Carneiro]

If you try to do the same thing with filters, the replacement for "continuous" is tendsto, and in order to keep the <= relation going the same way we have to reverse the order of filters

[Mario Carneiro]

That is, tendsto id L1 L2 iff L2 ⊆ L1

[Ming Li]

I am reading #mil and would like to understand the relation between filter bases and topological bases: are they one-to-one corresponding "in some sense"? Correct me please if I am worng. For a function on types/sets, given filter/topological bases, Tendsto of the function is defined, depending on bases. While a type is a topological space, by taking neighborhoods atTop from topological space, one gets the definition of continuity. Given a topological base, a filter can be formed (uniquly?) so that continuity is well defined..? How about the other around?

[Kevin Buzzard]

Filters and topologies on a type are not in one-one correspondence, so you shouldn't expect filter bases and topological bases to be in one-one correspondence in any meaningful way

[Ming Li]

Thanks. So, in Mathlib, the filter is induced from the topology so that it is dealing topological properties through filtters. Even without topologies, Tendsto is still defined via filters and is meaningful in 'computer' sense. Right?

[Kevin Buzzard]

Both continuity and tendsto are not properties of a topology/filter, they are properties of two topologies and a function. Continuity is really a property of two topologies, a function, and a point. You can see the definition of docs#Filter.Tendsto for yourself and see what inputs it needs to make it meaningful.

[Ming Li]

Continuity and tendsto rely on neighborhorhoods of a point and its image under the function, which are given from topologies. So continuity in Mathlib is induced from topologies and the function but is cannonical so that it is indepdent of filters. Right?

[Jireh Loreaux]

I'm not sure what you mean by "independent of filters". Here is what is true:

1. Given a topology on X, for every x you can build the neighborhood filter at x called nhds x. This filter consists of all sets which contain an open set containing x.
2. Then a function between topological spaces f : X -> Y is continuous at x if and only if tendsto f (nhds x) (nhds (f x)). So, while tendsto is a statement only about filters, continuity is a statement about tendsto involving neighborhood filters, so it invokes the topology.
3. If you forget the topology for a moment, you can go backwards. Suppose that for each x : X you have a filter F x : Filter X. From this, you can define a collection of sets by U : Set X is in this collection if, for every x in U, U lies in F x. Then this collection forms a topology on X, and with respect to this topology, nhds x = F x for all x : X.

The constructions in (1), i.e., the construction of neighborhood filters from a topology, and (3), i.e., the construction of a topology from a filter associated to every point, are inverses of each other.

[Anatole Dedecker]

This is almost true, but you need an extra axiom to be able to build out a topology from a set of filters. This axiom is docs#eventually_mem_nhds which says that a neighborhood of x has to also be a neighborhood of points close enough to x

[Ming Li]

Your (1) and (3) are the answer for my question about one to one correspondence in pointwise sense. Will the topology formed by a filter in (3) be exactly the one in (1)? What if given another filter? I learned topology in mathematics but not filter.

[Vincent Beffara]

Specifically, to make a topology out of an indexed family of filters you can use docs#TopologicalSpace.mkOfNhds, and then to check that the topology is what you wanted (i.e., your family coincides with the neighborhoods in the topology you obtain) you have to use something like docs#TopologicalSpace.nhds_mkOfNhds (you need to show that your family satisfies two conditions, which are always indeed satisfies by neighborhoods in a topology but of course not always satisfied by an arbitrary collections of filters).

[Anatole Dedecker]

Ah right, you can always define a topology from a family of filters, but then the neighborhood filters my not be equal to the filter you gave

[Anatole Dedecker]

And yes, when restricted to the families of filter which satisfy the extra "locality" axiom, you get a true bijection between topologies and families of filters

[Jireh Loreaux]

Ah yes, thanks. I forgot this condition was required to make the map bijective. I constructed the topology in my head and saw.that it worked, but didn't bother to check that the maps were inverses.

[Ming Li]

Ah great, thanks to all! Corresponding from a topology to a family of filters is exactly "independent of filters" in local sense. Usually, the convergence induced by the family of filters might be non-topological one so that it includes ones in measure sense. Right?

[Jireh Loreaux]

Sure, you can have non-topological ones. The simplest example would be convergence at infinity. For instance, given a sequence a : ℕ → ℝ and L : ℝ, Filter.Tendsto f Filter.atTop (𝓝 L) says exactly that the sequence converges to L as n goes to ∞. But here, Filter.atTop represents the "as n goes to ∞" bit, and this is not a topological filter†, it is a filter defined in terms of the order structure on ℕ.

† It is possible to view Filter.atTop as Filter.comap (↑) (𝓝 ∞) from the Alexandroff (i.e., docs#OnePoint) compactification of ℕ, but it is certainly not defined this way.

import Mathlib

open Filter OnePoint Topology

example : comap ((↑) : ℕ → OnePoint ℕ) (𝓝 ∞) = atTop := by
  rw [comap_coe_nhds_infty, coclosedCompact_eq_cocompact,
    cocompact_eq_cofinite, Nat.cofinite_eq_atTop]