T2 quotient

Stream: maths

[Patrick Massot]

Looking at #12536 by @Matias Heikkilä convinced me it is time to fix our universe issues in the Stone-Cech universal property. Working on this I got side-tracked by the fact we don’t seem to have the reflection of topological spaces into T2 spaces (by reflection I mean a functor that is left-adjoint to the inclusion functor). We do have something called docs#separationQuotient whose name is not so great since we have at least half a dozen separation axioms in Mathlib and this name does not tell which separation is achieved. And it is not the one I want here (we could argue that T2 is the most common separation axiom and it should get the separationQuotient name, but being explicit is also nice).

So I built the T2 one here. So far everything is in one place, including twenty lines above that have nothing to do with separation. Before moving things to their proper home, I’d be interested in reading comments about this. People who may want to comment include @Yury G. Kudryashov, @Anatole Dedecker and @Reid Barton.

[Patrick Massot]

One weird lemma is

lemma Continuous.disjoint_nhds_of_different_image {X Y Z : Type*}
    [TopologicalSpace Y] [T2Space Y]
    [TopologicalSpace Z] {f : X → Y} {k : X → Z} {g : Z → Y}
    (hg : Continuous g) (h : g ∘ k = f) {x x' : X} (hxx' : f x ≠ f x') :
    Disjoint (𝓝 (k x)) (𝓝 (k x')) := by
  have := disjoint_nhds_nhds.mpr hxx'
  rw [← h] at *
  have d₁ : 𝓝 (k x) ≤ comap g (𝓝 (g (k x))) := by refine tendsto_iff_comap.mp hg.continuousAt
  have d₂ : 𝓝 (k x') ≤ comap g (𝓝 (g (k x'))) := by refine tendsto_iff_comap.mp hg.continuousAt
  exact (disjoint_comap this).mono d₁ d₂

that is simply the common part of two proofs that I had. Of course the formulation is silly, the map f could simply be replace by g ∘ k in the statement. But somehow it makes the lemma easier to apply. Also one could ask that g is continuous only at k x and k x', and weaken the T2 assumption on Y to talk only about f x and f x'. But again it would make the lemma harder to use for its two intended applications. But I still feel bad about this so don’t hesitate to find a nicer way to solve the proof duplication issue.

[Yury G. Kudryashov]

What do you suggest about migration?

• For R1 spaces, two setoids are equivalent, and I think that we should have it as a theorem.
• Which defeq do we use for uniform spaces, metric spaces etc?
• Who does the migration?

[Patrick Massot]

I’m not sure we need to migrate anything.

[Patrick Massot]

Maybe the other construction is useful too since in general they are different.

[Yury G. Kudryashov]

Currently, docs#SeparationQuotient (a.k.a. T0 quotient) is used for uniform spaces, metric spaces etc. Do you want to use the new construction for uniform spaces? If yes, then we need to migrate.

[Steven Clontz]

Definitely still a lean newbie, but as a general topology researcher, I can say that if I came across "separation quotient" in the literature I'd react with :shrug: and look up how it was defined, but "$T_0$ quotient" is quite natural.

[Yury G. Kudryashov]

As for your lemma, subst f gets you to docs#Filter.Tendsto.disjoint

[Patrick Massot]

Yes, I think we can have names t0Quotient and t2Quotient, but I understand that using t0Quotient with a uniform space would read weird.

[Yury G. Kudryashov]

What do you think about KolmogorovQuotient? https://en.wikipedia.org/wiki/Kolmogorov_space#The_Kolmogorov_quotient

[Yury G. Kudryashov]

Is there a useful description for the equivalence relation behind T2Quotient that doesn't use global structure? Something in terms of nhds filters?

[Patrick Massot]

Indeed

lemma Continuous.disjoint_nhds_of_different_image {X Y Z : Type*}
    [TopologicalSpace Y] [T2Space Y]
    [TopologicalSpace Z] {f : X → Y} {k : X → Z} {g : Z → Y}
    (hg : Continuous g) (h : g ∘ k = f) {x x' : X} (hxx' : f x ≠ f x') :
    Disjoint (𝓝 (k x)) (𝓝 (k x')) := by
  subst h
  exact Tendsto.disjoint  hg.continuousAt (disjoint_nhds_nhds.mpr hxx') hg.continuousAt

is much shorter, and probably sufficiently short to be inlined in my two use cases. So this issue is solved.

[Patrick Massot]

I don’t know any other description of this equivalence relation.

[Patrick Massot]

I googled a bit and only found more complicated descriptions (including taking a transfinite number of quotients instead of one…).

[Yury G. Kudryashov]

Is it the transitive closure of "nhds aren't disjoint"?

[Yury G. Kudryashov]

Or this is not enough?

[Patrick Massot]

I think it’s not enough. But I’m sure Steven will tell us.

[Patrick Massot]

By the way, Steven, you may also have something to contribute to the original goal which was to improve our construction of the Stone-Cech compactification. Do you know a direct construction that stay within general topology (so does not involve real numbers in particular) but has no size issue? By size issue I mean things like taking quotients by an equivalence relation involving all compact Hausdorff spaces like we currently do here. I have an idea to do that, but maybe there is something “well-known”.

[Patrick Massot]

I will read answers tomorrow because it is bed time now.

[Steven Clontz]

Yury G. Kudryashov said:

What do you think about KolmogorovQuotient? https://en.wikipedia.org/wiki/Kolmogorov_space#The_Kolmogorov_quotient

This is also standard, but if there's both a T0 and T2 quotient, having similar names might be better UX

[Steven Clontz]

Patrick Massot said:

By the way, Steven, you may also have something to contribute to the original goal which was to improve our construction of the Stone-Cech compactification. Do you know a direct construction that stay within general topology (so does not involve real numbers in particular) but has no size issue? By size issue I mean things like taking quotients by an equivalence relation involving all compact Hausdorff spaces like we currently do here. I have an idea to do that, but maybe there is something “well-known”.

I'll look into this and get back

[Kevin Buzzard]

What exactly is the problem with the current set-up? It seems that we still get def StoneCech : Type u :=... if (α : Type u) [TopologicalSpace α].

[Patrick Massot]

Thanks Steven. Kevin, the issue is with docs#stoneCechExtend. Note how α and γ live in the same universe.

[Patrick Massot]

So we have a universal property for the Stone-Cech compactification that is not universal across universes. Will I dare writing we need an inter-universal Stone-Cech compactification?

[Anatole Dedecker]

I feel like I'm about to say something silly, but doesn't any continuous map $f : X \to Y$ where $X$ and $Y$ are compact Hausdorff factor through some compact Hausdorff $Y'$ which lives in the same universe as $X$ ? E.g because docs#Setoid.quotientKerEquivRange would upgrade to an homeomorphism thanks to docs#Continuous.homeoOfEquivCompactToT2 ? Where does this fail ?

[Kevin Buzzard]

The theorem only applies if $Y$ is compact, and I guess you don't know that $Y'$ is compact?

[Anatole Dedecker]

Well if you take it as a quotient of a compact space it is compact for sure ?

[Kevin Buzzard]

Oh maybe I've not understood what you're doing. Let me go through it step by step. We have alpha (non-compact, universe u) and are trying to prove that any map from alpha to Y (compact, universe v) extends to a map from alpha-compactified to Y. What is your X?

[Anatole Dedecker]

X is alpa-compactified

[Anatole Dedecker]

Ah

[Anatole Dedecker]

Ok

[Anatole Dedecker]

But my argument still says that, in the definition of docs#stoneCechSetoid, one could choose any universe for the target spaces, right ?

[Kevin Buzzard]

I don't properly understand what's going on here. It seems to me that the relation might depend on the target universe. For example if v < u and you define the relationship to be that for all gamma of type v and for all maps from alpha to gamma etc etc, then there simply might not be enough maps to get the correct relation. As a toy example, imagine there's a universe whose type are just the finite types (this isn't quite a universe, but it's not far from one and it's a good toy model). Then you don't get too many interesting maps from alpha to gamma and so r might change?

[Yury G. Kudryashov]

We don't want the setoid to depend on an extra universe parameter.

[Anatole Dedecker]

In other words without changing any definition: takeX as Ultrafilter alpha and f' as Ultrafilter.extend f where f : alpha -> Y is our original map. Now the question is does f' factor through the map Ultrafilter alpha -> alpha-compactified, and my claim is yes because everything is compact T2 so I can assume f' lands in the same universe as Ultrafilter alpha (i.e the universe of alpha).

[Yury G. Kudryashov]

Can you formalize this?

[Anatole Dedecker]

I can do it tomorrow yes. There may well be a stupid mistake somewhere of course (and indeed the fact that it works even when making the universe smaller sounds a bit weird...)

[Patrick Massot]

I considered deducing the inter-universal version from the version we have. In principle it should be doable. But it would feel pretty ugly to me. It would feel nicer to have a construction that do not involving universes at all.

[Yury G. Kudryashov]

Most (all?) my knowledge on the subject comes from the Wikipedia page. All constructions there either involve the product of all compact T2 spaces or real numbers...

[Anatole Dedecker]

Patrick Massot said:

Do you know a direct construction that stay within general topology (so does not involve real numbers in particular) but has no size issue?

I would be tempted to say that C-star algebra theory is just noncommutative general topology, so the spectrum construction is indeed staying inside topology :upside_down:

[Kevin Buzzard]

Is Ultrafilter alpha compact T2? Does it even have a topology?

[Anatole Dedecker]

Yes it is

[Patrick Massot]

I should try to finish my idea. I have some preliminary work at https://github.com/leanprover-community/mathlib4/blob/599d37eb6b393fae6564e634a9ac7d715aa255ca/Mathlib/Topology/StoneCech.lean#L248-L249. At first I thought that would be the right definition. I proved the universal property but then I realized that I didn’t know how to prove that it is T2. That’s why my new plan became to build t2Quotient. I’m not super happy about this since it would be a three steps construction, but I thought that t2Quotient was worth having anyway.

[Anatole Dedecker]

Kevin Buzzard said:

Is Ultrafilter alpha compact T2? Does it even have a topology?

It’s the Stone Cech compactification of alpha with the discrete topology.

[Patrick Massot]

That being said, maybe that thinking about t2Quotient made be better at proving things are T2 and I’ll be able to finish the proof now.

[Patrick Massot]

No, I had something stupid in mind. I’m back to my previous strategy.

[Kevin Buzzard]

I think Anatole's approach works without changing the definition of the compactification? If v is too small then you probably can't make the definition of the compactification using v but it still seems to satisfy the universal property

[Steven Clontz]

I have to admit that in my "day job" I mostly think about ultrafilters when X is discrete (and most counterexamples I need are subspaces thereof). When I do deal with other compactifications I like to use maps into $[0,1]$ (or just the universal property). So I'm derusting a bit on the other characterizations, and may have a more clever idea next week when I'm back in the office and can get to my copy of Walker.

But, another characterization one might consider (if it makes formalization easier) is the product described at https://math.stackexchange.com/a/2958720: each factor corresponds to each possible continuous map from the space into a compact Hausdorff space. To make this a set and not a class, observe that the cardinality of compact Hausdorff spaces that have a particular space mapped into a dense subset is bounded above (by $2^{2^{|X|}}$ I think?) so we need only index over maps into those spaces.

[Patrick Massot]

This kind of cardinality bound is part of what I’m trying to avoid.

[Patrick Massot]

I finished the 3 steps approach I had in mind and it indeed builds a model with the really universal universal property, as can be seen here.

[Patrick Massot]

In that version of the file there are three variations: StoneCech is the original one, with its problematic construction (I mean problematic only because we like to be crazy with universe polymorphism). Then StoneCech' is my optimistic version from before I thought about proving it was T2. And StoneCech'' is the T2 quotient of the previous one. It satisfies the universal property with any target space in any universe and its definition does not involve any universe juggling. Of course I could cleanup all this, but I’ll wait a bit to see whether anyone comes up with a smarter way.

[Steven Clontz]

Patrick Massot said:

I think it’s not enough. But I’m sure Steven will tell us.

Unlike the T0 quotient, the "non-disjoint neighborhoods relation" corresponding to T2 is not transitive. But it's true that if you take the equivalence relation generated by it (the intersection of all equivalence relations containing it, equivalently, its transitive closure) then that quotient will be T2. Whether that's the same or not as your definition is not clear to me yet.

[Yury G. Kudryashov]

How do I show that the quotient by the transitive closure of this relation is T2?

[Adam Topaz]

If you take the "universal algebra" point of view that compact Hausdorff spaces are algebras for the ultrafilter monad, then you know exactly what you have to do: If X is any compact Hausdorff space and r is a relation on X, you need to "close up" r to get the analogue of a congruence relation for the ultrafilter monad. The "operations" interpreted topologically are just the map Ultrafilter X -> X sending F to the (unique) limit of F on X. To "close it up" I think it suffices to take the inductive relation generated by r and limits of F and G whenever F and G are ultrafilters which have the same pushforward in X/(closure of r). Now you can apply this to X = Ultrafilter alpha and r the relation saying that two ultrafilters are identified if they have a common limit on alpha (this is Patrick's StoneCech').

Note that since quotients of compact spaces are compact, the quotient of X/r which agrees with the quotient by the "closed up" r is the same as the t2 quotient of X/r.

[Adam Topaz]

Now, in the case of Ultrafilter alpha, the "limit" map Ultrafilter (Ultrafilter alpha) -> Ultrafilter alpha is the monadic join. So it's possible to write down the closed up relation directly as an inductive relation without referring to limits.

[Adam Topaz]

Well, now that I wrote that out, I realized that it won't be possible to write down the inductive relation as above since one has to consider the quotient by the inductive relation in a hypothesis of one of the constructors. But it's possible there's another way to write down the condition without referring to the quotient.

[Adam Topaz]

Another approach is to take the infimum over all equivalence relations satisfying that condition and implied by r.

[Adam Topaz]

So, if I got it right, the following setoid should work:

def stoneCechSetoid : Setoid (Ultrafilter α) :=
  ⨅ S : Setoid (Ultrafilter α),
  ⨅ (_ : ∀ F G : Ultrafilter α, (∃ (x : α), F ≤ 𝓝 x ∧ G ≤ 𝓝 x) → S.r F G),
  ⨅ (_ : ∀ F G : Ultrafilter (Ultrafilter α),
      F.map (Quotient.mk S) = G.map (Quotient.mk S) → S.r (joinM F) (joinM G)),
    S

But this is a mess. So it's probably just easier to use the t2quotient :)

[Steven Clontz]

Yury G. Kudryashov said:

How do I show that the quotient by the transitive closure of this relation is T2?

I had sketched a proof but it had an oversight. I asked the question at https://math.stackexchange.com/questions/4918434/what-is-a-t-2-quotient and may self-answer, but it's getting late and if I don't I'd expect someone else will by the morning.

[Steven Clontz]

Turns out the answer is "you can't" - the process must be repeated inductively.

[Steven Clontz]

This thesis seems to be a decent overview: https://math.leidenuniv.nl/scripties/BachVanMunster.pdf

[Antoine Chambert-Loir]

Once you have a quotient of X that works in a universe u, and if your target Y is a space in universe v, you can take the image Y' of X in Y, which will be u-small (because it is equivalent to a set quotient of X), take an u-representative and work from there.

[Patrick Massot]

Antoine, this has been proposed several times already, but it feels cleaner to have a direct definition that does not depend on universes.

[Patrick Massot]

Since we want t2Quotient anyway, I guess I will clean up my approach and PR it.

[Anatole Dedecker]

Antoine Chambert-Loir said:

Once you have a quotient of X that works in a universe u, and if your target Y is a space in universe v, you can take the image Y' of X in Y, which will be u-small (because it is equivalent to a set quotient of X), take an u-representative and work from there.

I was about to say "oh yes, this is obviously nicer, I just wanted compactness in order to use the quotient topology rather than just inducing the topology", but then decided I wanted to start formalizing first, and it's not as easy as it seems. I just opened #13010 as a draft with this approach (but I agree that Patrick's solution is probably nicer). Here are the subtleties I encountered along the way.

1. After reading Antoine's message, I was going to ignore the construction details and just deduce the polymorphic universal property from the existing one, but then realized it didn't work, because if you start from a noncompact α then the range of f is not necessarily closed, so in order to factor through a compact space in the lower universe one needs to build something which is in bijection with the closure of the range, not just the range. This would require the cardinality bound mentioned above, which I definitely didn't want to formalize. However, since Ultrafilter α is compact, this doesn't rule out showing that if two ultrafilters are equivalent for docs#stoneCechSetoid, then they actually satisfy the equality you want independently of the universe of the target. And indeed this works.

2. The relation in stoneCechSetoid does not take into account all maps from Ultrafilter α to compact spaces, only those which are extensions of continuous maps from α, so we need to check that the new map that we obtain instead of Ultrafilter.extend f can still be written in this way. This is indeed true by density of α in Ultrafilter α, and by the fact that the new target space is compact hence its (quotient) topology is the same as the topology induced by the original target space.

[Adam Topaz]

I think that if we had some general API for algebras and their quotients for (type theoretic) monads then the approach I mentioned could be reasonable. But right now I agree the t2quotient approach would be the cleanest

[Patrick Massot]

I opened #13061 with the part that we want in any case: the construction of the largest T2 quotient of a space. I did not change anything that already existed. @Anatole Dedecker @Yury G. Kudryashov

[Patrick Massot]

The file length linter complains…

[Ruben Van de Velde]

You can add an exception

[Patrick Massot]

I know, but I’m meant to feel bad doing so.

[Patrick Massot]

The main drawback of this guilt inducing system is that it pushes to split files and add content in the same PR.

[Yaël Dillies]

I think you should just add the exception

[Yaël Dillies]

I hate the file length linter because it doesn't tell you how to ignore it. Just as with shake, there should be a command to run to automatically ignore the suggestion of the file length linter.

[Yaël Dillies]

Patrick Massot said:

The main drawback of this guilt inducing system is that it pushes to split files and add content in the same PR.

... and that random contributors are tasked with splitting files rather than people who actually understand the file structure (eg me with algebraic order theory)

[Patrick Massot]

We already have a Topology/Separation folder, with a single file. The obvious split here is given by numbering, gathering the T and R versions. So we would have Topology/Separation/T0R0.lean, Topology/Separation/T1R1.lean etc…

[Yaël Dillies]

(although in that specific case I trust the random contributor actually knows the file structure pretty well :wink:)

[Patrick Massot]

Actually that file was already an exception…

[Patrick Massot]

After three attempts, I managed to setup the new exception.

[Steven Clontz]

I have a WIP that improves regular+2ndCount implies normal to just regular+Lindelof. Part of why it's a WIP is because I hadn't found time to learn the right way to satisfy the file size limit. I'm also interested in contributing perfectly normal and completing the chain to show metrizable implies perfectly normal.

The separation file seems quite large; it'd be nice to see it factored out.

[Kim Morrison]

@Steven Clontz, if you link to the PR someone can walk you through satisfying the file size limit.

[Yury G. Kudryashov]

Note that R1 corresponds to T2

[Yury G. Kudryashov]

I think that we also should move all defs to a single file.

[Steven Clontz]

Thx @Kim Morrison - ran a workshop a week ago, in another this week... Once this has come and gone I'll clean up the WIP and request such help (barring a refactor that makes file size moot).

[Patrick Massot]

Yury G. Kudryashov said:

I think that we also should move all defs to a single file.

What would be the gain here? Having definitions but no lemmas seems not very useful. We sometimes do that with definitions that can be used for programming without proving, but this does not apply here.

[Kim Morrison]

I disagree here. I would like the .Defs / .Basic split that we have in the algebra hierarchy to continue much further into Mathlib. My experience has been that it really helps with reducing unnecessary imports. Definitions don't have to be used for programming: often they are just used for more definitions.

[Steven Clontz]

Ruben Van de Velde said:

You can add an exception

I'm working on another PR for Separation.lean at #13176 and would like to know how this is done as I've also hit the upper limit.

(I think the file was obscenely long before I made it worse, but figure that refactor shou;dn't be mixed up in my work.)

[Steven Clontz]

(maybe it's moot - when I merged master, the linter stopped complaining)

[Michael Rothgang]

Yaël Dillies said:

I hate the file length linter because it doesn't tell you how to ignore it. Just as with shake, there should be a command to run to automatically ignore the suggestion of the file length linter.

This command is called ./scripts/update-style-exceptions.py. Granted, it only becomes the most useful when coupled with that file being updated weekly (so it's generally up-to-date).

That said, if you find this too annoying: I'm happy to write a separate executable just for the file length in Lean. Ping me again in three weeks :-)

[Yaël Dillies]

Whatever you do, please include it in the error message! We don't want anyone splitting a file because they have no idea that there is an alternative.

[Michael Rothgang]

@Yaël Dillies @Patrick Massot Your wish was granted, the rewriteMichael tactic got bored enough to implement this sooner. #13623 implements nicer output on "file too long" errors, including a new Lean command to fix the error, and a suggestion how to add it (in a fine-grained way). Testing (to see I didn't miss anything) and reviewing welcome - this depends on #13620 for rewriting the check in Lean.

[Patrick Massot]

I am sorry I neglected this discussion for a long time, but I just opened #14108 with the two-step construction of the inter-universal Stone-Čech compactification.