Universal property of inclusion of principal filters

Stream: maths

[Patrick Massot]

I have a question for people who love orders. It was initially a complicated question but then I realized I don’t even know how to answer a baby version. Let $X$ be a type and $φ : Filter(X) → Filter(X)$. Assume $φ$ is monotone and is the identity on principal filters. Is $φ$ the identity? The more complicated version is: assume $Q$ is complete lattice (or more generally a poset where directed sets have an infimum) and $f : Set(X) → Q$ is monotone. Does any monotone extension $φ : Filter(X) → Q$ of $f$ automatically preserve infimums of directed sets?

[Yaël Dillies]

I am pretty sure $φ$ doesn't need to be the identity

[Yaël Dillies]

Actually, here is a fully explicit counterexample: φ f := generate f.ker. This is the identity on filters with a basis and nowhere else

[Yaël Dillies]

The picture is that $φ$ somehow "completes" the filter to force it to be based

[Patrick Massot]

Nice, thanks. I couldn’t see any reason why $φ$ would miraculously behave nicely but I didn’t get the right idea to build a counter-example.

[Patrick Massot]

Where does your weird vocabulary comes from? Is it from the theory of pfilters on posets other than $Set(X)$?

[Yaël Dillies]

What part is the weird vocabulary? I was never officially taught about filters so I'm making the nomenclature up

[Patrick Massot]

Weird here means non-mathlib.

[Patrick Massot]

If I understand correctly, your generate is called principal in mathlib and what you call based filters are called principal filters.

[Patrick Massot]

But it may be that the mathlib vocabulary is weird. There are definitely people who seem to use the word principal only in the case of singletons.

[Yaël Dillies]

No, I mean docs#Filter.generate

[Patrick Massot]

Then your formula does not type-check.

[Patrick Massot]

And I am pretty sure I interpret your example in the way you intend it.

[Yaël Dillies]

Oh yes you are right, I mean principal f.ker

[Patrick Massot]

Do you know any property of the order on Filter X that is special and can be explained without referring to principal?

[Patrick Massot]

I’m sorry this is a vague question. What I try to understand better is whether the free completion going from Set X to Filter X by freely adding directed infimums makes Filter X intrinsically better than Set X.

[Patrick Massot]

The confusing thing compared to other free constructions is that other constructions usually start with a less structured object. For instance building a free group on a set starts with a set and builds a group, and same with free module etc. Here we already have a complete lattice but we are somehow dissatisfied with its (directed) infimums and add new ones.

[Yaël Dillies]

I want to say that the generalisation of principal filters to arbitrary orders is something like compact, prime or irreducible elements, but I haven't checked the details

[Yaël Dillies]

I mean, Kyle would say something something pro-objects, but I am not sure I have a good general intuition for why filters are better than sets.

[Patrick Massot]

The clear part is this story of directed infimums. Those suck in Set X. For instance the infimum of neighborhoods of x in a nice topological space is {x} and we want to change that. Going to Filter X changes this infimum to nhds x which is larger than {x}. And this is done in a way that any monotone function from Set X to a complete lattice (or even a poset with directed infimum) extends uniquely to a function that preserves directed infs. But I have a hard time seeing whether the infimums in Filter X have a nice property by themselves. A very nice one would be that any monotone function between filters automatically preserved directed infs, but this was fishy and indeed you provided a counter-example.

[Patrick Massot]

In relation with Set X this is clearer. There is the universal property I mentioned and also the related fact that a directed infimum is less than a principal filter if and only if one element of the set is less than this principal filter.

[Patrick Massot]

The later statement being Filter.mem_iInf_of_directed

[Antoine Chambert-Loir]

I interpret the theorem “A filter is the intersection of the ultrafilters it contains” as the fact that the set of filters on $X$ identifies with the set of subsets of $\beta X$, the Stone-Cech compactification of $X$. Since $\beta X$ is best viewed as a topological space, my intuition is that the set of filters should also be considered in regard with this topology, but I don't know whether this will help to answer your question.

[Patrick Massot]

I don’t think this helps me, but thanks anyway.

[Antoine Chambert-Loir]

I suspect that @Sam van G would have some idea about your question.

[Antoine Chambert-Loir]

Have you seen this? https://mathoverflow.net/questions/139608/a-characterization-of-the-poset-of-filters-on-a-set

[Sam van G]

Antoine Chambert-Loir said:

I suspect that Sam van G would have some idea about your question.

I’m not sure what the question is exactly. Section 2 of this article by Gehrke and Priestley 2008 studies the abstract properties of the filter completion of a poset (they focus on adding directed joins but mathematically it’s of course the same, modulo adding a few “op”s in the right places).

[Sam van G]

Patrick Massot said:

In relation with Set X this is clearer. There is the universal property I mentioned and also the related fact that a directed infimum is less than a principal filter if and only if one element of the set is less than this principal filter.

The second property is a special case of what is called “compact completion” in that section. It is indeed closely related to topological compactness.

[Sam van G]

Patrick Massot said:

Do you know any property of the order on Filter X that is special and can be explained without referring to principal?

The comparison with free groups is indeed a useful one to think about: As you know, the construction that sends Set(X) to Filter(X) is a special case of the construction that sends a poset P to a the poset F(P) of filters in (not “on”!) P. So when doing this construction, you actually first “forget” almost all the complete lattice (even complete atomic Boolean algebra) structure that you have on Set(X), except for the fact that it’s a poset.
Now one can ask the interesting question: If P is a “special” poset and I look at its filter poset F(P), how can the “specialness” of P be felt on F(P)? One such property is for example stated as Prop 2.3 of the cited paper (I just reverse the statement here wrt the paper to better fit your filter intuitions): If P had finite sups to begin with, then so does F(P). In Lemma 2.4, some extension properties for functions are given.

[Sam van G]

As is also shown there, the embedding e : P -> F(P) can be characterized abstractly as the unique completion of P which has directed meets, is generated by P under directed meets, and which satisfies the property that, whenever a meet of a directed set D is below an element e(p) where p in P, then at least one of the elements of D is below e(p).
To state this property, though, one must refer to the elements of the “generating” poset P. But this is analogous to the fact that when you say a set X freely generates the free group FG(X), you need to refer to X when you state that there are no relations between the generators.

[Adam Topaz]

Is there anything else to say beyond the pro objects point of view? For example the characterization of principal filters discussed above is analogous to the notion of a compact object as described here https://ncatlab.org/nlab/show/compact+object (or rather its dual since compact objects would be the analogue for ind-objects). And in terms of the universal property of the lattice of filters, it should correspond exactly to the universal property of the pro-category, which should translate to saying that any monotone map from Set X to T, where T has directed infs, extends uniquely to a monotone map from Filter X to T which preserves all directed infs.

[Patrick Massot]

Thanks Sam, this is all useful. I’ll read that paper. I like the confirmation of the characterization I was hoping for, but I still don’t have a good story about how F(P) is better than P when P was already a complete lattice. I think the best summary of what bothers me is: “if I start with something that is already complete then anything called a completion should not change it up to isomorphism”.

[Patrick Massot]

Since we are here, does anyone know whether F(P) can be seen as a category of sheaves on P (with e being the Yoneda embedding)?

[Adam Topaz]

Patrick you may want to look at https://ncatlab.org/nlab/show/ind-object#the_case_that__already_admits_filtered_colimits (again, this is in the categorical context and for ind-objects, but something analogous can be said in you context as well)

[Adam Topaz]

In other words, it’s not just about completeness in the sense that directed infs exist, but also that the lattice is generated under directed infs by “cocompact” objects. This generation condition will not hold true in general even if directed infs exist, and Set X is an example.

[Mai Gehrke]

I have a few comments to add to what Sam said. This does reiterate part of both what he and Adam Topaz have already said. Sorry about that.

When going from Powerset(X) to Filt(X), which from the point of view of ordered sets should really rather be called Filt(Powerset(X)), the first step is to FORGET — at least — the infinitary meets structure of Powerset(X) (you can keep just the order, the finite joins, the arbitrary joins structure, and/or the finite meets structure), THEN you freely add down-directed (=filtering) meets.

To follow the analogy with groups, if you take a group G, forget its structure and just keep the underlying set, then take the free group over that, there is not much you can say about the relation to the original group structure. Of course, this is not that bad because in the case of Powerset(X)\mapsto Filt(Powerset(X)), we do keep the order (so a weak part of the structure of Powerset(X)).

The good news is, for very general reasons, as Sam said:

• the poset Powerset(X) has finite meets, and therefore Filt(Powerset(X)) does also ! (and the embedding preserves these). In fact, as a consequence Filt(Powerset(X)) has all meets and is in fact a complete lattice.
• Powerset(X) has arbitrary joins and the embedding preserves these.

However, the embedding DESTROYS ALL non-trivial directed meets (that is, the embedding destroys meets of any filtering set, which doesn’t have a minimum)!
In fact, when one does the construction P\mapsto Filt(P) to a poset which already has filtering meets this is usually precisely what one is seeking: the existing filtering meets give faulty information about the limit behaviour of the finitary order/meet structure of the poset. Sorry that this last part is a bit vague, but I think it gets at what you, Patrick, are asking in your last post

good story about how F(P) is better than P when P was already a complete lattice

It is better precisely in that we have destroyed the nontrivial filtering meets!!!

If we take the free filtering meets completion in the category of posets enriched with "partially existing filtering meets" (this corresponds to taking filters closed under existing filtering meets), then from Powerset(X) we indeed just get Powerset(X), but I suspect, in whatever capacity you are using Powerset(X)\mapsto Filt(Powerset(X)), you probably want to encode "downward limit behaviour" of the finitary meet structure of Powerset(X). This is the point of (co-)compactness. This is also what Adam Topaz is talking about, I think.

Just to finish up the round of nice complete lattice properties possessed by Powerset(X):

• It is meet generated by its co-atoms and is a co-frame. This all remains true for Filt(Powerset(X));
• It is join generated by its atoms and is a frame. This is NOT true for Filt(Powerset(X)). It is atomic as every filter is an intersection of ultrafilters (assuming these exist), but it is not a frame as every atomic frame is isomorphic to the powerset of its atoms. This is not true for Filt(Powerset(X)), e.g. it isn't Boolean.
• It is completely distributive. This is not true for Filt(Powerset(X)) since it isn't even a frame.
  (Here "frame" means complete lattice in which arbitrary joins distribute over finite meets)