Real TVS Initial PR

[GeoffreySangston]

Based on the Issue thread #1743.

[prabau]

P87 (has a group topology): Munkres does not seem too useful here. How about replacing it in the refs: with https://en.wikipedia.org/wiki/Topological_group (which itself has a bunch of good references, so no need for another one).

And in the first sentence of the text we can also make "topological group" link to wikipedia.

(and we could do a similar linking for the first sentence in P238)

[prabau]

T880: To close the argument, it would be helpful to have an additional sentence at the end mentioning that a balanced set in $X$ is contractible. No justification needed.

[prabau]

T881 (loc. compact Hausdorff TVS are n-manifolds) This looks too artificial.
The conclusion we really want (from the point of view of TVS) is that it is a finite dimensional vector space. And your version seems a contrived way of hinting at that.

At this point, is this theorem even useful to have? Can it help derive some traits that cannot be derived otherwise?

Or, in the same way that we have "locally $n$-Euclidean" as a property, we could have a corresponding global property: $n$-Euclidean (= homeomorphic to some $\mathbb R^n$) and use that, which is really the desired conclusion. (Not actually sure we want this, but it would be better than the current version. That's if we really need this thm.)

As an aside: Even in this context, I find it helpful to say "n-manifold" instead of just "manifold", which could be all kinds of other things, like infinite dimensional ones.)

[GeoffreySangston]

I think we definitely need to encode the theorem that locally compact hausdorff TVS's are homeomorphic to Euclidean spaces. I.e. it's each of famous, basic, and interesting. Why do you think this fact seems optional?

The tactical question of whether to do it now or to add a "Homeomorphic to Euclidean n-space" property (analogous to other family properties like "Has a cofinite topology" is different. I'm open to waiting until we added "Homeomorphic to Euclidean n-space" (also seems like a clear positive to include since a lot of topology was invented to understand this property).

---

Here's an argument for your side. The Malcev-Iwasawa theorem says that a connected locally compact Hausdorff topological group is homeomorphic to $K \times \mathbb{R}^n$, for a maximal compact subgroup $K$; see MO, and this MO post is also interesting. Then I believe it is true that a contractible compact Hausdorff group is trivial, but I'm looking for a reference (Edit: See below) or planning on asking an MSE question about this. So I believe this theorem could be strengthened.

From the comprehensive looking treatise on compact Hausdorff groups by Hofmann-Morris:

Corollary 10.71. A (weakly) contractible quotient of a compact group is singleton.
In particular, a contractible compact group is a point.

[prabau]

Interesting results. Even if it can be generalized in the context of topological groups, the desired result here (that loc. compact Hausdorff TVS are n-Euclidean) is more straightforward and still very important, worth stating separately, I think. With n-Euclidean in the conclusion instead of n-manifold.
So if we add the n-Euclidean property later on, we can add the theorem at that point.
Feel free to open a separate issue for proposing the new property.