Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have edited at Tychonoff theorem:
tidied up the Idea-section. (Previously there was a long paragraph on the spelling of the theorem before the content of the theorem was even mentioned)
moved the proofs into a subsection “Proofs”, and added a pointer to an elementary proof of the finitary version, here
Notice that there is an ancient query box in the entry, with discussion between Todd and Toby. It would be good to remove this box and turn whatever conclusion was reached into a proper part of the entry.
At then end of the entry there is a line:
More details to appear at Tychonoff theorem for locales
which however has not “appeared” yet.
But since the page is not called “Tychonoff theorem for topological spaces”, and since it already talks about locales a fair bit in the Idea section, I suggest to remove that line and to simply add all discussion of localic Tychonoff to this same entry.
In fact I have this localic Tychonoff material on my web, here. I hadn’t moved it over to the main Lab because I wasn’t satisfied with it yet. Should I?
Oh, I see, thanks for the pointer. Yes, please, that would be nice if this were moved to the main Lab.
And since it’s a long page, maybe I take back my suggestion not to split it off. Maybe best to give it a separate entry, as originally intended.
I tried to copy it over, but I get a Bad Gateway message. Will try again later.
Trivial point, but doesn’t everyone say ’Tychonoff’s theorem’ rather than ’(The) Tychonoff theorem’?
I tried to copy it over, but I get a Bad Gateway message. Will try again later.
Was that in trying to create a new entry? Then maybe try a different entry name, or try inserting it into the existing entry after all. Because it must be that there is some bug involved when the software checks a new entry name. For instance one gets bad gateways when a name is different but similar to an existing name (which is curious: this means that the software is trying to be unexpectedly sophisticated).
Trivial point, but doesn’t everyone say ’Tychonoff’s theorem’ rather than ’(The) Tychonoff theorem’?
True, I have changed the entry name. Also I have added references to the original articles. And I moved the remark about spelling to where it belogs, the category:peopl-entry A. N. Tychonoff. And I added more redirects there.
Is there also a version of Tychonoff’s theorem when the indexing set is itself replaced by a locale?
I think I might have seen somewhere a statement like this:
if p:X→B is a proper map of locales (and possibly B should be required to be compact or locally compact), then the locale of sections of p is itself compact.
If B is discrete, we recover the classical formulation of Tychonoff’s theorem.
True, I have changed the entry name.
I don’t have a problem with that, but it’s not true that “everyone” says “Tychonoff’s theorem”. Google says otherwise. [I think I myself got in the habit of saying “(the) Tychonoff theorem”, and I suppose I got that from somewhere.]
Re #9: Here are some Google ngrams (press the blue button to display the graphs): https://books.google.com/ngrams/graph?content=Tychonoff%27s+theorem%2CTychonoff+theorem&year_start=1900&year_end=2000&corpus=15&smoothing=20&share=&direct_url=t1%3B%2CTychonoff%20%27s%20theorem%3B%2Cc0%3B.t1%3B%2CTychonoff%20theorem%3B%2Cc0
Maybe I don’t know how to read an ngram, but it looks like Tychonoff theorem is ahead to me.
Re #6: it’s there now (i.e., success!).
I based my comment on 9 of the first 10 Google hits even for “Tychonoff theorem” having the ’s, but I see it’s more even. Anyway, it seems he has more than one theorem to his name, including a fixed point theorem.
Thanks, Todd!
Might you have energy left to look into turning your old query box discussion with Toby (here) into a proper part of the entry?
I’m not sure what to do with it, so I’ll remove it and stick it here for now. I’d be delighted if Toby looked into it more, but the issue is a little remote from my brain at the moment.
+–{.query}
Todd: Regarding the need for excluded middle: it’s not so clear that there’s any direct argument. For it’s at this point where we have to use the ultrafilter theorem, in order to produce a witnessing ultrafilter. Witness to what? The statement as it stands involves universal quantification over ultrafilters, so the witness would be in view of a contradiction.
Toby: Note that we use excluded middle in two places for a proof by contradiction; I'll try to remove these if possible. (Todd: I’ve rearranged the argument in the first step; the first formulation I gave looked unnecessarily “choice-y”.)
Todd: Yes, although I’m not too fussed about using indirect arguments, since in a topos, excluded middle follows from AC. I don’t know whether it also follows from a weaker choice principle equivalent to the ultrafilter theorem, but I guess I wouldn’t be surprised if it did.
Toby: As far as I know, UF and EM are independent (although I'm not certain). So I'm interested in whether the Hausdorff case requires EM as well as UF.
Todd: I wrote John Bell about this, and he kindly responded. Apparently you are right: UF (or BPIT) implies only a weakened version of EM: . He referred me to his paper Boolean Algebras and Distributive Lattices Treated Constructively, for this (among much else).
Toby: Great, hard results! Although I'm not sure that his ultrafilter theorem is the same as mine, since he talks about ultrafilters in arbitrary distributive lattices, while I would use a constructively stronger definition of ultrafilter in a powerset. But I should be able to figure out what carries over, now that I have a result to go for.
I remember looking at that paper and trying to translate the result from ultrafilters in a distributive lattice to ultrafilters in a set (which are not simply ultrafilters in the distributive lattice that is the power set because of the difference in definitions), but I wasn't able to then.
The Tychonoff theorem follows from the fact that being proper (compact) is a lifting property; (Bourbaki, General Topology, I\S10.2, Thm.1(d), p.101) gives a characterisation via ultrafilters which is a lifting property wrt maps associated with ultrafilters (namely, maps S–>S\cup{*} such that the open neighbourhoods of * are the F-big subsets of S, where F is an ultrafilter F on S).
In fact, there is a characterisation here of being proper in terms of the lifting property and finite spaces, but only for T4 spaces.
There are somewhat more details in there but that’s a very rough draft…)
I have written out the proof of the Tychonoff theorem via net convergence, here (the proof due to Chernoff 92)
I have also added more References (here), using Chernoff’s commented list of references.
Urs, you undid all the work I just put into an edit. Why?
I’ve added a short exposition of the proof of Tychonoff theorem in terms of ultrafilters.
Thanks. I have edited the (sub-)section structure slightly. Check if you agree.
I have also added a remark and an open question which may not belong here;
I have given this its own subsection, here
they use my own notation for finite topological spaces and lifting properties.
Is there a possibility to point to one of your articles or notes for further details?
By the way, unfortunately here with Instiki, the code
\text{ }
does not produce a white space. Also
\text{ something }
does not equip ’something’ with space around it. To make horizontal space, use
\,
or
\phantom{A}
or the like.
Due to this, your two definitions for and after “For a property of arrows…” came out hard to read. I have reformatted them. Check if you agree.
Urs, I refer to my comment in #21. I was going to announce my edit and explain my thinking, but I had to take my daughter to school.
Sorry, Todd, I didn’t know I was overwriting anything. I was just editing and saving as usual.
Since this has happened before, maybe next time when you are editing for a long time, it would help to make intermediate submits every now and then. That prevents the timeout of your edit block.
Urs, the progress I had made was saved before I took my daughter to school (at least it was from the POV of my screen), and then when I came back it was gone. Don’t know what is going on. It may need looking into.
Edit: Just to make sure I wasn’t hallucinating, I checked again, and it’s here. By way of explanation, I just thought Misha’s text (whose proof I like very much by the way) might be too concise for some readers to follow easily, so I gave some expansion and put in some environments. I was going to enter Bourbaki into the references when I got back, hopefully with an online link so that people could check that proof. If no one minds (and particularly Misha), then I’d like the contents of that edit reinstated.
Sure, I have switched back to version 30. (Now the typesitting problems highlighted in #23 are back, but I am out of time now.)
Don’t know what is going on.
I think what happens is these cases is that
a) person A starts to edit
b) the edit block times out
c) person B starts to edit
d) person A hits “submit”
e) person B hits “submit”
Okay, my understanding had been that as long as person A was editing (and hadn’t let 15 minutes go by without a keystroke), then person B should still be getting the message that person A was editing. Maybe that understanding was incorrect, but if so, it’s annoying to have to hit “save” when one is still in mid-sentence and trying to think carefully.
Anyway, what I’ll do is actually just rollback to version 31, but then copy and paste in what I had written and then hopefully everyone is happy.
Thanks, Todd, for merging the content!
(I didn’t think that the software is watching keystrokes to determine if an entry is still being edited. Is that so? Maybe then there is some problem when one of the internet connections is slow or shaky, as mine here is.)
1 to 33 of 33