Indeed, if you want to record facts about the Dedekind real numbers (which seems to have been the intention of the Anonymous editor who brought this up here), that should go into a dedicated entry on Dedekind real numbers.

If you need help with breaking the existing redirect and creating such an entry, let me know.

]]>Mike Shulman’s definition of a connected space and proof that the Dedekind real numbers are connected could also be placed in an article on axiom R-flat, but that currently redirects to real-cohesive (infinity,1)-topos.

]]>What is needed in this article however is a section on terminology in constructive mathematics, such as Paul Taylor's distinction between connectedness and "overt connectedness". ]]>

I have added a brief section “Constructive definition” (here) in order to reference the material that Anonymous had created a new entry for (here, rev 1),

namely Def. 13.2 in:

- Paul Taylor,
*A lambda calculus for real analysis*, In: Journal of Logic & Analysis**2**5 (2010) 1–115 $[$L&A:63/25, pdf, webpage$]$

I have copied over Anonymous’s paragraph which spells this out, though this definition seems either redundant or incomplete, depending on how much background knowledge about HoTT one assumes the reader to have. By wich I mean: If it is kept then it would seem to deserve more commentary on what it is that the reader is meant to take away here.

]]>Fixed typo and statement that used surjectivity to show preimage preserves union

Anonymous

]]>Corrected typos. Moved the first “example” to a new section, “Properties”. (Originally, the Examples section was meant to give general techniques for *constructing* examples of connected spaces.) Combined two subsections which were both titled “Connected components”.

I have added an elementary point-set proof that arbitrary product spaces of connected spaces are connected: here.

(I left intact, at the beginning of the proof, the pointer to a general abstract proof at *connected object*.)

Woops. Thanks for the alert. I have fixed it now (I hope).

]]>Something weird has happened. Look at the repetition in the table of contents.

]]>I have added to *connected topological space* the proofs that

the connected subsets of the real line are precisely the intervals (here)

the contimnuous images of connected spaces are connected (here)

the intermediate value theorem (here, and also at

*intermediate value theorem*itself: here)

I have further re-arranged the material at *connected space* a little, to easy reading. See the new table of contents.

For instance I moved the definition of connected components to the Definition-secton, and I moved the discussion of “basic results” to “Basic examples” (because all these results are about classes of examples).

Finally I have split off *locally connected topological space* to its own entry.

At *connected space* I have first re-arranged the Definition-section (putting the elemetary definition first, and the category-theoretic definiton after that) and then I expanded a little, adding one more equivalent characterization and some words on the elementrary proof of why these elementary definitions are equivalent.

No, it *wasn't* true even when I wrote it, so I should never have written it. I can't just put things back the way that they used to be (and rephrase or move new material), because it was never correct.

Your phrasing seems to suggest a possibility that the statement might have been true when you wrote it but become false afterwards?

Edit: Oh, do you mean that someone could have edited the definitions without changing the remark about them?

]]>Early on in the history of this page, I had written that various definitions were constructively equivalent, but that wasn’t true even when I wrote it. I took it out just now.

]]>Yes. I think that highlighted statement was just trying to warn people of a *very* common pitfall (that is invariably embarrassing for those who fall in). I agree with your emendation.

… in other words, locally connected spaces are a *cohesive* 1-category over Set. (-:

I think what I object to about the statement I highlighted is that in my mind, “disjoint union” is not an operation on *spaces* except insofar as it means “coproduct”, so it doesn’t make sense to talk about a *space* being a disjoint union of other spaces but not their coproduct. I tried to fix it by inserting references to underlying sets. The result still feels a little awkward, but I like it better at least.

I have been working some more at connected space. The statement that I was comically getting wrong earlier should be replaced by:

There is an adjoint string $\Pi_0 \dashv \Delta \dashv \Gamma \dashv \nabla: Set \to LocConn$.

Relevant to all this is the (previously unrealized by me) statement that locally connected spaces are coreflective in the category of all topological spaces.

I have also been tightening the formatting and structure of the article here and there.

]]>I can’t locate that alleged Wikipedia statement, but more importantly I’m going to have to retract what I said about the discrete space functor having a left adjoint of any form, because the discrete space functor does not preserve infinite products. Oops!

I think someone else wrote the statement you highlighted. The statement and your interpretation are correct, but $(-\infty, 0)$ and $[0, \infty)$ are not connected components of $\mathbb{R}$ even if they are connected.

]]>No, I’ve never thought about this sort of thing. Where is the mistake on Wikipedia? Did you consider correcting it?

The page is very nice (thanks!). One question/comment:

Every space is a disjoint union (but not necessarily a coproduct in the category of spaces) of connected components.

Is the phrase “disjoint union” supposed to mean something stronger than a disjoint union of underlying sets? I mean, $\mathbb{R}$ is the disjoint union of $(-\infty,0)$ and $[0,\infty)$, but my intuition is that the connected components of a space are somehow “more separated” than that. Is there any way to make that precise?

]]>I added a bunch of things to connected space: stuff on the path components functor, an example of a countable connected Hausdorff space, and the observation that the quasi-components functor is left adjoint to the discrete space functor $Set \to Top$ (Wikipedia reports that the connected components functor is left adjoint to the discrete space functor, but that’s wrong).

This bit about quasi-components functor had never occurred to me before, although it seems to be true. I’m having difficulty getting much information on this functor. For example, does it preserve finite products? I don’t know, but I doubt it. Does anyone reading this know?

]]>