Interior points of group manifolds #
Every point of a group manifold whose multiplication is C^n, for n ≠ 0, is an interior point;
smooth inversion is not required. It suffices to find one interior point in a chart and transport
it to the desired point by C^n left multiplication.
This supplies a prerequisite for Deliverable A, Layer 1 of
TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.
Main results #
ContMDiffMul.isInteriorPoint: every point of a group manifold withC^nmultiplication, forn ≠ 0, is an interior point.ContMDiffMul.boundarylessManifold: a group manifold withC^1multiplication is boundaryless (opt-in, not an instance).
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The group adjoint".
theorem
ContMDiffMul.isInteriorPoint
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
{n : WithTop ℕ∞}
[ContMDiffMul I n G]
(hn : n ≠ 0)
(g : G)
:
I.IsInteriorPoint g
Every point of a group manifold with C^n multiplication, for n ≠ 0, is an interior point.
theorem
ContMDiffMul.boundarylessManifold
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{G : Type u_4}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[ContMDiffMul I 1 G]
:
A group manifold with C^1 multiplication is boundaryless.
This theorem is deliberately not an instance: consumers can opt in with
attribute [local instance] ContMDiffMul.boundarylessManifold.