pi-base
Add equivalent formulations for P41 (locally connected)
@GeoffreySangston I re-read the proof of Lemma 5.9.6 in the Stacks project (https://stacks.math.columbia.edu/tag/0050) that shows that (locally) Noetherian spaces are locally compact (T651).
Our definition of locally connected (P41) is that the topology of the space has a base of open connected sets. It's equivalent to say that each nbhd of a point $x$ contains an open connected nbhd of $x$.
But as far as I call tell, the proof of that Lemma does not show that. Given a nbhd $E$ of $x$, it finds a connected nbhd $E''$ of $x$ contained in $E$, with $E''$ not necessarily open. That's a slightly different notion, called "connected im kleinen" at the point $x$. See Definitions section in https://en.wikipedia.org/wiki/Locally_connected_space.
But it's a theorem that a space connected im kleinen at at each of its points is in fact locally connected.
I think we should expand the pi-base page for P41 to state some of these equivalent characterizations to make that clear.
What do you think?
Originally posted by @prabau in https://github.com/pi-base/data/issues/1014#issuecomment-2521945528
@prabau
Given a nbhd E of x , it finds a connected nbhd E ″ of x contained in E , with E ″ not necessarily open.
I agree that $E''$ doesn't seem to be necessarily open, but I'm not that familiar with a lot of the basics of irreducible sets / hyperconnectedness (I have looked a bit a the Stacks project pages now). Just for edification purposes, how do you actually construct an example showing this? I don't think an excluded point topology works. I don't think pi-base has any spaces serving as suitable examples π-Base, Search for Noetherian + ~Hyperconnected
But it's a theorem that a space connected im kleinen at at each of its point is in fact locally connected.
I think we should expand the pi-base page for P41 to state some of these equivalent characterizations to make that clear.
Sounds good to me. I think connected im kleinen at $x$ for all $x$ (also called weakly locally connected on Wikipedia) is a weakly local property in the sense of pi- base. https://github.com/pi-base/data/wiki/Conventions-and-Style#local-properties
Both properties are equivalent: $X$ locally connected iff $X$ weakly locally connected. If we cared about a local property at only a specific point, they would not be equivalent. But they would still both be a "local property" and not a "weakly local property" in the convention of pi-base (i.e., in both cases we need to find a special kind of nbhd within an arbitrarily small nbhd of the point).
@prabau Oh my mistake. I misunderstood the pi-base definition of weakly local.
Okay well I can try to gather references for these tomorrow.
About the question whether $E''$ is open or not, I don't have an example to show it may not be open.
But from the proof, all we know is that we can assume $E$ is open and $E'$ is open, so $E\cap E'$ is open. Now each $Y_i$ is an irreducible component of $E\cap E'$, so it closed in $E\cap E'$. And therefore $E''$ is closed in $E\cap E'$. And on the other hand, the set equal to $E\cap E'$ minus the $Y_i$ that don't contain $x$, is an open set in $E\cap E'$, but it need not be connected anymore.
But the desired result is true anyway if we further use the equivalence of "locally compact" and "weakly locally compact" (in the sense of "im kleinen").
Okay well I can try to gather references for these tomorrow.
I think https://en.wikipedia.org/wiki/Locally_connected_space and the references there cover it. Maybe enough to refer to wikipedia plus references therein.
@prabau Alright well it sounds like everything's covered then. I'm happy with reviewing a PR about this whenever. I can't imagine this is a particularly controversial issue.
I thought about it some more. It turns out that the final set $V=(E \cap E') -\bigcup\{ $Y_j: x\notin Y_j\}$is actually connected. It is an open connected nbhd of $x$.
Reason: an open subset of a hyperconnected set is itself hyperconnected. So let $A$ be the union of the $Y_j$ that don't contain $x$, which is closed in $E\cap E'$. For each irreducible $Y_i$ containing $x$, the set $Y_i\setminus A$ is irreducible, hence it's a connected set containing $x$. So $V$, which is their union, is also connected.
Still a good idea to add the equivalent definitions for P41, which could be useful in general.