Dieudonne complete

[Moniker1998]

Resolves#477
Essentially, completely uniformizable spaces are those spaces whose Kolmogorov quotient is realcompact.

Perhaps some theorems about realcompact spaces could be replaced by those involving completely uniformizable spaces

[yhx-12243]

Later I (or you of others) may propose a property namely “Extent less than every measurable cardinal”, as a complete helper for this. (I've preparing for the property of “Extent < 𝖈”, as mentioned in #1398 (comment))

[Moniker1998]

@yhx-12243 we could, but we won't be introducing any spaces of size larger than the first measurable cardinal, as far as I know

[yhx-12243]

Yes, just like P164 (Cardinality less than every measurable cardinal).

[Moniker1998]

P164 has its use, and this is the reason why the extent property is not needed

[prabau]

It seems "Dieudonné complete" is a better primary name for this. (see Engelking 8.5.13 and Encyclopedia of General Topology pp. 205, 254, 262.)

See Engelking for more topological characterizations for this, in particular items (2) and (3).

[prabau]

Are you sure about "topologically complete" as an alias?
Which source uses that for Dieudonne complete?

If I recall, that term may have been used for various other things as well, maybe for completely metrizable or Cech-complete. It's rather confusing.

[Moniker1998]

@prabau wikipedia, which cites Kelley

[Moniker1998]

@prabau I don't think another alias is bad, I did the same thing with ultranormal property. There shouldn't be confusion as those are just aliases.
Thanks for the references by the way. I am trying to go through Engelking's exercise and will add it once I verify it's true

[prabau]

Adding another alias is fine if it has been used somewhere for the same concept. In that case, we should put a note at the bottom mentioning the alternate name with reference.

[Moniker1998]

T382 could be replaced by $R_0$ + normal + submetacompact $\implies$ Dieudonne complete, perhaps
T386 we can replace with pseudocompact + Dieudonne complete $\implies$ compact

[yhx-12243]

T382 could be replaced by R₀ + normal + submetacompact ⟹ Dieudonne complete

Wrong. See notes in https://www.ams.org/journals/proc/1973-040-02/S0002-9939-1973-0322812-9/S0002-9939-1973-0322812-9.pdf, if measurable cardinality exists.

So I suggest add an extra weaker but correct theorem: R₁ + paracompact ⟹ Dieudonne complete (it can solve the unknown traits in pi-base now, though)

T386 we can replace with pseudocompact + Dieudonne complete ⟹ compact

This is right.

[Moniker1998]

@prabau I've noticed there's no spaces which are $T_4$ and subparacompact, but not paracompact. I'm guessing those are equivalent?

[yhx-12243]

@prabau I've noticed there's no spaces which are T 4 and subparacompact, but not paracompact. I'm guessing those are equivalent?

#742 is the counterexample. See https://scispace.com/pdf/on-subparacompact-spaces-2o1ji8yodk.pdf.

[Moniker1998]

Ah okay. Another reason to add this eventually

[yhx-12243]

How do you think to add “R₁ + paracompact ⟹ Dieudonne complete” ?

[Moniker1998]

There is an exercise in Engelking referencing three papers, I assume one of them contains a somewhat easier proof of this

[Moniker1998]

Oddly enough, I haven't found easy proof online, but I did find converse for GO-spaces

[Moniker1998]

@prabau please review

[Moniker1998]

@felixpernegger that'd be great 👍
After, if you think nothing else should be added, then you could approve and @prabau can merge if there's no problems

[felixpernegger]

For me this is good now, but im sure @prabau will have more comments :)

[Moniker1998]

Uniform spaces and pseudometrics.pdf

here's a pdf where I wrote some of the "standard" things about the equivalence of definitions of uniform spaces
note I haven't proved last statement about uniformly continuous pseudometrics belonging to $\mathcal{D}$. I must have proved it as an exercise in GJ but I've solved the exercises like 2 years ago. Nonetheless they contain a hint if anyone wants to show that themselves. I don't really want to reprove it.

Edit: Sorry, I've saved it wrong and the previous version was just a tex file saved as pdf

[prabau]

I have not checked your latest changes, but will soon.
One thing about the equivalence between the various characterizations: it's proved in Dieudonne (https://zbmath.org/65.0877.01). It's also most certainly somewhere in detail in Bourbaki, which we could cite here. I'll need to look where exactly.

[Moniker1998]

@prabau what is proven in Dieudonne?

[prabau]

@prabau what is proven in Dieudonne?

The characterization as a closed subset of a product of metrizable spaces.
I looked in Bourbaki and couldn't find it there though.

[Moniker1998]

@prabau then I can add that source and we'll just move on? Or you can add a suggestion. I'll be away for couple of days, though, so maybe @felixpernegger can get to it if I can't

[prabau]

@prabau then I can add that source and we'll just move on? Or you can add a suggestion. I'll be away for couple of days, though, so maybe @felixpernegger can get to it if I can't

I can maybe add a suggestion. I have more suggestions to come, nothing major, mostly cosmetic. But there is no rush. We have waited so long already that one more week will not make a difference.

[prabau]

I committed an update for P221 directly, as I was unable to make a suggestion for it (too many lines):
More readable overall layout, removed "uniform space" from the refs: (but it's still accessible directly from the link at the top), add Dieudonne reference, add two meta-properties. Feel free to comment.

[Moniker1998]

@prabau anything else?

[prabau]

Looks good to me