Zulip Chat Archive

Stream: Is there code for X?

Topic: topological basis on Inf topology

Adam Topaz (May 26 2021 at 19:26):

Given a collection of topological spaces $X_i$ and maps $f_i : X \to X_i$ from a fixed $X$ , we can form the coarsest topology on $X$ for which the $f_i$ are continuous. We can formalize this in lean as the Inf of the induced topologies along the $f_i$ as $i$ varies. Do we have a description of a topological basis for this topology on $X$ ?

Patrick Massot (May 26 2021 at 19:31):

We have very few results describing bases for topologies, because they are much less useful than filter bases. Here we definitely have results about the neighborhoods for this topology. What are you trying to do?

Kevin Buzzard (May 26 2021 at 19:31):

I don't know the answer but one could break this into two constructions. You can ask about a basis for the topology on $\Pi_i X_i$ and then you could use the fact that the pullback of a basis will be a basis (this is the definition of the topology on $X$ I guess).

Adam Topaz (May 26 2021 at 19:32):

This is the goal:
https://github.com/leanprover-community/lean-liquid/blob/cef5b005860b8b66695a923737a6357e23cd1e89/src/for_mathlib/Profinite/clopen_limit.lean#L77

Adam Topaz (May 26 2021 at 19:37):

It's a bit hard to decipher, but what's going on is that we have a cofiletered system $X_i$ of profinite spaces, and $X$ is the limit, whose topology, at the end of the day, is defined as above. This assertion is that for any clopen $U$ in $X$ there is some $i$ and some clopen $U_i$ in $X_i$ such that $U$ is the pullback of $U_i$ . The cofiltered assertion is crucial for this, but for now I'm just trying to get a handle of working with the (cl)opens in $X$ .

Adam Topaz (May 26 2021 at 19:41):

I would be happy to get a basis on the product of the $X_i$ as well (although then the explicit cone Top.limit_cone_Inf should be changed to Top.limit_cone whose topology is defeq to the subspace topology of the product)