thank you for your excellent edits, I agree with all of it,

except that I'd keep a reference to (Bourbaki, I\S6.5, Definition 5, Example) defining X\cup {\infty}.

>>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?

Notation for the finite topological spaces is now introduced at the page about

separation axioms....

Notation for the finite spaces is introduced on page 6-7 \S3 of

http://mishap.sdf.org/by:gavrilovich/expressive_power_of_lifting_property.pdf

Notation for the lifting properites is introduced in the beginning of the paper

(and in this page).

Some details about the Tychonoff theorem are given in

\S2.6 of http://mishap.sdf.org/by:gavrilovich/mints-elementary-topology-as-diagram-chasing.pdf

I'm a bit reluctant to give a reference though, it was never carefully proofread. ]]>

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.)

]]>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.

]]>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”

]]>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.

]]>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, 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.

]]>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 $C^l$ and $C^r$ after “For a property $C$ of arrows…” came out hard to read. I have reformatted them. Check if you agree.

]]>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?

]]>Urs, you undid all the work I just put into an edit. Why?

]]>I have also added a remark and an open question which may not belong here;

they use my own notation for finite topological spaces and lifting properties.

Please feel free to remove them or move elsewhere

as you see fit. ]]>

I have also added more References (here), using Chernoff’s commented list of references.

]]>I have written out the proof of the Tychonoff theorem via net convergence, here (the proof due to Chernoff 92)

]]>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 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.

]]>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: $\neg x \vee \neg\neg x = 1$. 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.

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 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.

]]>Re #6: it’s there now (i.e., success!).

]]>Maybe I don’t know how to read an ngram, but it looks like Tychonoff theorem is ahead to me.

]]>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

]]>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.]

]]>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.

]]>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.