Zulip Chat Archive

Stream: general

Topic: ne_bot of ultrafilter


Bernd Losert (Jul 26 2022 at 21:15):

I have the following:

import tactic
import order.filter.ultrafilter

example {α : Type*} (u : ultrafilter α) : u.ne_bot := sorry

but Lean complains:

type expected at
  u.ne_bot
term has type
  u.ne_bot

If I change it to ↑u.ne_bot, it still complains. What is the right way to do this?

Adam Topaz (Jul 26 2022 at 21:17):

import tactic
import order.filter.ultrafilter

example {α : Type*} (u : ultrafilter α) : (u : filter α).ne_bot := infer_instance

Adam Topaz (Jul 26 2022 at 21:17):

Note that infer_instance should mean that you never have to actually do this ;)

Bernd Losert (Jul 26 2022 at 21:18):

This is just an mwe. I'm doing something similar in a giant proof and it's causing weird problems.

Yaël Dillies (Jul 26 2022 at 21:20):

This is because u.ne_bot is the proof that ↑u ≠ ⊥. What you want is (u : filter α).ne_bot.

Bernd Losert (Jul 26 2022 at 21:21):

Aren't those supposed to mean the same thing?

Yaël Dillies (Jul 26 2022 at 21:22):

Just have a look at what docs#ultrafilter.ne_bot actually is and compare that to docs#filter.ne_bot.

Bernd Losert (Jul 26 2022 at 21:25):

Do you know what is the rational behind having a class for f ≠ ⊥?

Yaël Dillies (Jul 26 2022 at 21:40):

Not sure, no. Maybe it is needed as an assumption for some instance?

Kevin Buzzard (Jul 26 2022 at 21:41):

Being not bot for filters is a really common assumption in topology (so common that Bourbaki even went one step further and disallowed bot from being a filter). It's a Prop so it doesn't cause any trouble as an instance.

Bernd Losert (Jul 26 2022 at 22:07):

If it's so common though, why not just make a class for ne_bot filters instead of dealing with a ne_bot class for lattices? It does cause me trouble as you can see.

Bernd Losert (Jul 26 2022 at 22:08):

In the theory of convergence spaces that I am formalizing in lean, I have yet to see any real advantage to having a ne_bot class. I have to use haveI in proofs, which is kind of awkward.

Adam Topaz (Jul 26 2022 at 22:08):

docs#filter.ne_bot ?

Yaël Dillies (Jul 26 2022 at 22:09):

... except that all lemmas are/should duplicated with a version taking f.ne_bot as an instance argument and as an explicit one. Were you using the instances ones by accident?

Yaël Dillies (Jul 26 2022 at 22:10):

Also, I do not understand your previous message. We precisely have a ne_bot class for filters and no ne_bot class for lattices.

Bernd Losert (Jul 26 2022 at 22:22):

Oops. You're right. Scratch that.

Bernd Losert (Jul 26 2022 at 22:27):

Some lemmas take an explicit ne_bot argument and some don't and I've been designing my lemmas using instance arguments following the lemmas I have been using so far.

Yaël Dillies (Jul 26 2022 at 22:48):

So maybe this is the problem? Try making the arguments explicit instead and reassess pain.

Bernd Losert (Jul 27 2022 at 14:42):

Yes. I will start doing that.

Kyle Miller (Jul 27 2022 at 15:16):

Kevin Buzzard said:

Being not bot for filters is a really common assumption in topology (so common that Bourbaki even went one step further and disallowed bot from being a filter).

It turns out that the mathlib definition of a filter is, as a poset category, equivalent to the category Pro(P(X))\operatorname{Pro}(\mathcal{P}(X)), the category of pro-subsets of XX. The category of subsets of XX embeds in it, it naturally has arbitrary unions and finite (and cofiltered(*)) intersections from abstract Pro-nonsense, and it comes with a least element (the image of X\varnothing\subseteq X) and a greatest element (the image of XXX\subseteq X).

The correspondence is that a pro-subset SS is determined by the set {sXSs}\{s\subseteq X \mid S\subseteq s\}, which turns out to be a filter, and this map from pro-subsets to these sets is order-reversing. This is why people think mathlib's order for filters is backwards, but from the above perspective it's definitely the right one. Representing filters as sets saves us a universe bump, vs defining pro-subsets as left-exact copresheaves... (Plus, pro-subset isomorphism reduces to filter equality.)

(*) A cofiltered intersection is the intersection of a collection of pro-subsets that is closed under finite intersections. For example, intersections of chains.

Johan Commelin (Jul 27 2022 at 15:20):

That's some higher justification right there :joy_cat:

Kyle Miller (Jul 27 2022 at 15:25):

Why work with subsets for amateurs, when you can work with pro-subsets?

Kevin Buzzard (Jul 27 2022 at 15:56):

Profinite topological spaces (crucial in LTE and in many other places) are just Pro(finite sets), and spectral spaces (useful for nonarchimedean analysis/perfectoid etc) are just Pro(finite T_0 topological spaces). It would be interesting to see more about what this Pro construction does.

Kevin Buzzard (Jul 27 2022 at 15:58):

I think one thing worth stressing about this is that the category of finite sets has no mention of topology in its definition, and when you Pro it to get profinite sets, the morphisms are continuous even though the construction of the objects never mentions topology.

Bernd Losert (Jul 27 2022 at 18:17):

Interesting. I didn't realize the pro connection.

the morphisms are continuous even though the construction of the objects never mentions topology

In what sense are they continuous then?

Kyle Miller (Jul 27 2022 at 18:39):

If you have two pro-objects represented by U:ICU:I\to C and V:JCV:J\to C, where CC is the category and II and JJ are cofiltered categories, then the morphism set between them can be represented as

homPro(C)(U,V)limjJcolimiIhomC(Ui,Vj)\hom_{\operatorname{Pro}(C)}(U,V) \approx \operatorname*{lim}_{j\in J} \operatorname*{colim}_{i\in I} \hom_{C}(U_i,V_j)

If ff is a morphism, then this says "for all jJj\in J there is an iIi\in I such that ff restricts to a map UiVjU_i\to V_j."

That might not be the complete story, but at least it points toward morphisms somehow being continuous maps.

Bernd Losert (Jul 27 2022 at 19:52):

I see. Looks completely different from the notion of continuous that I'm familiar with.

Kyle Miller (Jul 27 2022 at 20:02):

This is the parallel I was thinking of: If f:XYf:X\to Y is a function between topological spaces, then continuity at xXx\in X is "for all open neighborhoods VYV\subseteq Y of f(x)f(x) there is an open neighborhood UXU\subseteq X of xx such that ff restricts to a map UVU\to V."

Adam Topaz (Jul 27 2022 at 20:17):

The way you get continuity in the profinite case has to do with how the topology is defined -- if you have a pro-object represented by X:IFinSetX : I \to FinSet then the limit (of sets, say) embeds in iXi\prod_i X_i which you endow with the Tychonoff topology. The transition maps give a closed condition defining this subset, and the product is a compact hausdoff totally disconnected space, so the same holds true for the limit.
In other words, the topology on limX\lim X is defined so that a map YlimXY \to lim X is continuous if and only if the induced map YXiY \to X_i is continuous for all ii.

Now suppose that limYlim Y is another profinite set. As Kyle mentioned, the morphisms in the pro category are given by limjcolimi(Yi,Xj)lim_j colim_i (Y_i,X_j) and the above observation reduces the issue to considering colimiHom(Yi,Xj)colim_i Hom(Y_i,X_j) for some fixed jj.
To conclude, first note that a map limYXjlim Y \to X_j is continuous if and only if it is locally constant, so the issue comes down to checking that any locally constant map from limYlim Y to some set factors through one of the YjY_j.

Adam Topaz (Jul 27 2022 at 20:21):

PS. This stuff was one of the first things we did in LTE (although we never got around to defining pro categories and/or identifying Profinite with Pro(FinType).

Bernd Losert (Jul 27 2022 at 20:51):

Aha. I think I am starting to get it. Interesting.


Last updated: Dec 20 2023 at 11:08 UTC