Boundary of [x,y], as a real manifold

Stream: mathlib4

[Michael Rothgang]

I'm slowly working in proving that a non-empty real interval [x,y] has boundary ${x,y}$ (as a real manifold; I know about docs#frontier_Icc). With the current Lean definitions, I think this is false - I'm claiming that the definition of docs#modelWithCornersEuclideanHalfSpace ought to change.

Under the current definition, a manifold M modelled on I is a BoundarylessManifold iff every point x : M satisfies extChartAt I x ∈ interior (range I).
However, the model docs#modelWithCornersEuclideanHalfSpace maps to a subtype EuclideanHalfSpace. As I understand it, every point which lies on the "mathematical" boundary lies in the interior of the subtype, implying we get a BoundarylessManifold (which is not what we want, mathematically).

More precisely: a point x : EuclideanHalfSpace with first coordinate 0 lies on the mathematical boundary of the half-space. If EuclideanHalfSpace were a subset of EuclideanSpace, x also lay on the boundary of range I. With the current formal definition, however, an open set (in the half space) containing x is the intersection of any Euclidean open ball around x with the half-space: this is open in the subtype EuclideanHalfSpace.

Can we change the definition of boundary points? Not really, a model with corners need not map into some subtype.
Thus, I propose changing the definition of modelWithCornersEuclideanHalfSpace, to map into EuclideanSpace instead.

Update: trying to actually change this, my proposal does not work, as the source of a model with corners must be univ. That issue about boundary is still unfortunately, though.

[Michael Rothgang]

@Sébastien Gouëzel You introduced this; what you do think?

[Sébastien Gouëzel]

I'm not sure I understand the question, so let me try to explain some points, hoping it will clarify things.

First, in a charted space X with respect to a space H, the charts are local homeomorphisms between open subsets of X and open subsets of H. By design, there can be no boundary points here, everything is interior wrt the topologies of X and H.

However, when we want to do differential calculus, we need to embed H into a vector space. This is the role of I : ModelWithCorners 𝕜 E H. The composition of I and the charts, called extended charts, are not local homeos any more, and for these it can make sense to ask which points have a chart which is locally onto in E, and which points don't. This is how one can define the boundary of a manifold in our framework.

Does it help?