Submetrizable implies Dieudonne complete (for completely regular spaces)

[Moniker1998]

No description provided.

[prabau]

the theorem number conflicts with #1819.

[Moniker1998]

@prabau do you want me to rename it

[prabau]

yes, please.

[Moniker1998]

@prabau comments on the substance?

[prabau]

I won't have time to look at it today. Hopefully tomorrow.

[Moniker1998]

@prabau this result is easier though, so maybe you want to review it first. Also, possibly more for you to do here, although I don't know if there's any other references for this.

[Moniker1998]

https://topology.pi-base.org/theorems/T000742 is essentially a version of this for realcompact spaces

Here we similarly have hereditary Dieudonne completeness, though we'll probably not add hereditary property on pi-base

The conclusion of hereditary Dieudonne completeness is essentially a stronger version of T742, given the two properties are equivalent for sizes < measurable.

Note this cannot be concluded in the same way as in T742. There is a T_4 metacompact space which is not Dieudonne complete. T382 does not translate to Dieudonne completeness

As far as I can see, all theorems that we have on pi-base about Dieudonne completeness and realcompactness are "strongest" versions. In the sense that when one can conclude stronger realcompactness, it is, and when weaker assumption of Dieudonne completeness can be used, it also is. The only case when this is not the case is when those are just non-theorems.

[Moniker1998]

I've added remarks on how realcompact and Dieudonne complete connect on the relevant pages. I think that's important, and I didn't do that before

[prabau]

Yes, I had noticed that for Hausdorff spaces with size < measurable, Dieudonne complete and realcompact are equivalent. So for space with such cardinality, T742 is actually an equivalent result (since the hypotheses are hereditary properties). I don't think we'll be having examples with higher cardinality any time soon. But is my understanding correct then that for higher cardinality one could have a T2 space that is Dieudonne complete and not realcompact?

[Moniker1998]

@prabau yeah, take a large enough metrizable space. Metrizable spaces are Dieudonne complete, and realcompact iff < measurable.

Note this is a corollary of a result which says that a $T_0$ Dieudonne complete space is realcompact iff every closed discrete subspace is < measurable (Shirota's theorem)

Even though in essence it won't add anything, I'd still like pi-base to have the sharpest theorems though

[prabau]

Suggested change

	- P000012: true
	- P000112: true
	- P000112: true
	- P000006: true

better match with T742

[Moniker1998]

@prabau why did you change completely regular to $T_{3\frac{1}{2}}$?

[prabau]

Look at the page https://topology.pi-base.org/properties/P000112/theorems and see the theorems T742 and T923, right on top of each other. T742 also makes the same assumption, so it will make it easier to see the relationship between the two theorems.

It's similar to the discussion we had for #1819. In this case, submetrizable spaces are Hausdorff. So submetrizable + completely regular is equivalent to submetrizable + Tychonoff.

[prabau]

Suggested change

	From {T915} and {T916}, it follows that if a space is {P164},
	then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.
	Note: If $X$ has {P164}, then $X$ is {P221} iff $\text{Kol}(X)$ is {P162}.

I agree that mentioning this fact is useful. But specifying the theorems justifying this feels too cluttered. Since the theorems being used for this are right on the same page as the property definitions and applying them is straightforward, I think it's fine to just state the result.

(and same comment for P221)

[prabau]

That reminds me of #1814. You were not in favor of adding such a space and maybe you are right. But maybe it could be useful, if we make clear what extra set-theoretic assumptions this would depend on. Just leaving this as a comment.

@StevenClontz FYI