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]

@prabau want to review this one?

[felixpernegger]

@prabau this is an important property. I really think we should review this

[prabau]

@felixpernegger I agree it's an important property and it would be nice to have.

When we approve and merge something into pi-base, it's not a matter of just looking that the results are plausible, reading theorem statements in references and checking some boxes. One would normally assume that at least one reviewer has looked at the topic in detail and has fully validated the PR. There are several suggestions I would make to improve the exposition slightly, including asking to fill out some missing steps (Some of them can be done with (Explore) links.) At this point I unfortunately don't have enough background on this topic to do it justice. Seems it would require having spent quite a bit of time with Gillman-Jerison. And also the main thing is exercise 8.5.13 in Engelking, which one would have to spend the time to prove or verify; we really need refs to some details here, maybe in mathse, maybe in some other sources. Basically, personally I think there is too much material in there to approve all in one go (which is why I never got into it).

So if you could dive into this, that would be a very good thing.

What do you think of this PR? What is it missing? Should it be split, or is it fine as is?

[felixpernegger]

Ill look into it