ChartedSpace.t2Space

Stream: Is there code for X?

[Geoffrey Irving]

Is it true that every ChartedSpace over a T2Space is a T2Space? That is, do we have

import Mathlib.Geometry.Manifold.ChartedSpace

lemma ChartedSpace.t2Space {A M : Type} [TopologicalSpace A] [TopologicalSpace M] [ChartedSpace A M] [T2Space A] :
    T2Space M := sorry

[Sébastien Gouëzel]

No, it's not true. If you take the real line with a double origin, it has a charted space structure wrt the real line, but it is not T2.

[Geoffrey Irving]

What does a double origin mean?

[Geoffrey Irving]

Ah, two points that are “far apart” but arbitrarily close to small nonzero values?

[Sébastien Gouëzel]

Yes. Take two real lines, and glue them together at every point but the origin.

[Geoffrey Irving]

Notably that isn’t a SmoothManifoldWithCorners using the identity ModelWithCorners. Is that enough for T2 in general?

[Sébastien Gouëzel]

No, that is definitely a SmoothManifoldWithCorners. Differential geometry books often start with this example, and the long line, and then say: from this point on, we will assume that all manifolds are T2 and sigma-compact, to exclude pathologies. The mathlib practice is to add the assumptions [T2Space M] and [SecondCountableTopology M] whenever needed.

[Sébastien Gouëzel]

For instance, you can have a look at the formulation of docs#exists_embedding_euclidean_of_compact

[Geoffrey Irving]

Yep, adding the extra assumptions is what I’ve been doing, but was hoping I could drop them. Alas!

[Geoffrey Irving]

And I guess once you have T2 you get all higher T<n>, since in each of the separate neighborhoods you can have single charts.