ne_bot of ultrafilter

Stream: general

[Bernd Losert]

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]

import tactic
import order.filter.ultrafilter

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

[Adam Topaz]

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

[Bernd Losert]

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

[Yaël Dillies]

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

[Bernd Losert]

Aren't those supposed to mean the same thing?

[Yaël Dillies]

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

[Bernd Losert]

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

[Yaël Dillies]

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

[Kevin Buzzard]

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]

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]

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]

docs#filter.ne_bot ?

[Yaël Dillies]

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

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]

Oops. You're right. Scratch that.

[Bernd Losert]

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]

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

[Bernd Losert]

Yes. I will start doing that.

[Kyle Miller]

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 $\operatorname{Pro}(\mathcal{P}(X))$, the category of pro-subsets of $X$. The category of subsets of $X$ 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 $\varnothing\subseteq X$) and a greatest element (the image of $X\subseteq X$).

The correspondence is that a pro-subset $S$ is determined by the set $\{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]

That's some higher justification right there :joy_cat:

[Kyle Miller]

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

[Kevin Buzzard]

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]

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]

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]

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

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

If $f$ is a morphism, then this says "for all $j\in J$ there is an $i\in I$ such that $f$ restricts to a map $U_i\to V_j$."

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

[Bernd Losert]

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

[Kyle Miller]

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

[Adam Topaz]

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 : I \to FinSet$ then the limit (of sets, say) embeds in $\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 $\lim X$ is defined so that a map $Y \to lim X$ is continuous if and only if the induced map $Y \to X_i$ is continuous for all $i$.

Now suppose that $lim Y$ is another profinite set. As Kyle mentioned, the morphisms in the pro category are given by $lim_j colim_i (Y_i,X_j)$ and the above observation reduces the issue to considering $colim_i Hom(Y_i,X_j)$ for some fixed $j$.
To conclude, first note that a map $lim 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 $lim Y$ to some set factors through one of the $Y_j$.

[Adam Topaz]

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]

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