Boundaryless manifold and interior point

Stream: mathlib4

[Winston Yin (尹維晨)]

Now that there’s docs#ModelWithCorners.IsInteriorPoint, does it make more sense to redefine docs#ModelWithCorners.Boundaryless as “every point on the manifold is an interior point”? For example, I’d like to give Lie groups a boundaryless instance. Currently, it requires the ModelWithCorners to map to the whole model vector space, so that excludes half spaces as the intermediate model space, even though you can still model boundaryless manifolds including Lie groups on the half space.

Another point is that I.Boundaryless just looks a bit awkward. With the suggested change in definition I’d like to write Boundaryless I M.

[Winston Yin (尹維晨)]

@Michael Rothgang

[Sébastien Gouëzel]

There are two different notions here: a model with corners I without boundary, and a manifold modelled on I without boundary, where the former implies the latter. It would make sense to have the two notions as two different typeclasses, with an instance from the former to the latter.

About Lie groups, the model space is naturally the whole space, no? Do you have examples in mind where the natural model space for a Lie group would be a half space?

[Winston Yin (尹維晨)]

No, but one could use a half space. Then I’d have to show that any Lie group could be modelled on the whole space, but that model with corners wouldn’t be the same one.

[Winston Yin (尹維晨)]

Your suggestion of two type classes makes sense. As a user, I would find it more intuitive to see Boundaryless I M for the manifold, and maybe WithoutCorners I for the model.

[Winston Yin (尹維晨)]

Would it be welcome for me to make a PR introducing the boundaryless type class on manifolds?

[Winston Yin (尹維晨)]

#9323 implements this new type class. Naming TBD

[Michael Rothgang]

See also this thread for an actual instance of proving "this manifold has boundary such and such".