Universal covers of Lie groups and subgroup covers of manifolds

Let X be a charted space that is locally path-connected and semilocally simply connected. The endpoint projection UniversalCover.proj : UniversalCover x₀ → X is a covering map, hence a local homeomorphism, and pulling the charts of X back along it makes the universal cover a charted space over the same model. When X is a C^n manifold, so is its universal cover, and the projection is a C^n local diffeomorphism. A map into the universal cover is C^n exactly when it is continuous and its composite with the projection is C^n. The same pulled-back atlas makes every subgroup cover a C^n manifold, with a C^n local diffeomorphism to the base.

For a Lie group G, the universal cover UniversalCover (1 : G) based at the identity is a group under pointwise multiplication of paths, and its multiplication and inversion lie over those of G. The criterion above therefore makes them C^n, so the universal cover is a Lie group, and the covering homomorphism UniversalCover.projHom, whose underlying map is the projection, is a C^n local diffeomorphism. This is the smooth half of the simply connected covering group of a connected Lie group.

Main results

• TauCeti.UniversalCover.instChartedSpace, TauCeti.UniversalCover.instIsManifold: the universal cover of a C^n manifold is a C^n manifold over the same model.
• TauCeti.UniversalCover.isLocalDiffeomorph_proj: the projection is a C^n local diffeomorphism.
• TauCeti.UniversalCover.instChartedSpaceSubgroupQuotient, TauCeti.UniversalCover.instIsManifoldSubgroupQuotient: the analogous atlas and manifold structure for an arbitrary subgroup cover.
• TauCeti.UniversalCover.isLocalDiffeomorph_subgroupQuotientProj: every subgroup-cover projection is a C^n local diffeomorphism.
• TauCeti.UniversalCover.contMDiff_iff: a map into the universal cover is C^n if and only if it is continuous and its composite with the projection is C^n.
• TauCeti.UniversalCover.instLieGroup: the universal cover of a Lie group is a Lie group.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Graduate Texts in Mathematics 218, Springer, 2013, Chapter 4, "Smooth Covering Maps", and Chapter 7, "Covering Groups".

@[instance_reducible]

noncomputable instance TauCeti.UniversalCover.instChartedSpace {H : Type u_3} [TopologicalSpace H] {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : ChartedSpace H (UniversalCover x₀)

The universal cover of a charted space carries the charts of the base pulled back along the covering projection.

instance TauCeti.UniversalCover.instIsManifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) [IsManifold I n X] : IsManifold I n (UniversalCover x₀)

The universal cover of a C^n manifold is a C^n manifold.

theorem TauCeti.UniversalCover.isLocalDiffeomorph_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : IsLocalDiffeomorph I I n proj

The covering projection of the universal cover is a C^n local diffeomorphism.

theorem TauCeti.UniversalCover.contMDiff_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : ContMDiff I I n proj

The covering projection of the universal cover is C^n.

theorem TauCeti.UniversalCover.contMDiffWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] {x₀ : X} {f : N → UniversalCover x₀} {s : Set N} {z : N} : ContMDiffWithinAt I' I n f s z ↔ ContinuousWithinAt f s z ∧ ContMDiffWithinAt I' I n (proj ∘ f) s z

A map into the universal cover is C^n within s at z if and only if it is continuous within s at z and its composite with the projection is C^n within s at z.

theorem TauCeti.UniversalCover.contMDiffAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] {x₀ : X} {f : N → UniversalCover x₀} {z : N} : ContMDiffAt I' I n f z ↔ ContinuousAt f z ∧ ContMDiffAt I' I n (proj ∘ f) z

A map into the universal cover is C^n at z if and only if it is continuous at z and its composite with the projection is C^n at z.

theorem TauCeti.UniversalCover.contMDiffOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] {x₀ : X} {f : N → UniversalCover x₀} {s : Set N} : ContMDiffOn I' I n f s ↔ ContinuousOn f s ∧ ContMDiffOn I' I n (proj ∘ f) s

A map into the universal cover is C^n on s if and only if it is continuous on s and its composite with the projection is C^n on s.

theorem TauCeti.UniversalCover.contMDiff_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] {x₀ : X} {f : N → UniversalCover x₀} : ContMDiff I' I n f ↔ Continuous f ∧ ContMDiff I' I n (proj ∘ f)

A map into the universal cover is C^n if and only if it is continuous and its composite with the projection is C^n.

@[instance_reducible]

noncomputable instance TauCeti.UniversalCover.instChartedSpaceSubgroupQuotient {H : Type u_3} [TopologicalSpace H] {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (K : Subgroup (FundamentalGroup X x₀)) : ChartedSpace H (SubgroupQuotient x₀ K)

A subgroup cover carries the atlas pulled back from the base along its projection.

instance TauCeti.UniversalCover.instIsManifoldSubgroupQuotient {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (K : Subgroup (FundamentalGroup X x₀)) [IsManifold I n X] : IsManifold I n (SubgroupQuotient x₀ K)

A subgroup cover of a C^n manifold is a C^n manifold.

theorem TauCeti.UniversalCover.isLocalDiffeomorph_subgroupQuotientProj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u_7} [TopologicalSpace X] [ChartedSpace H X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (K : Subgroup (FundamentalGroup X x₀)) : IsLocalDiffeomorph I I n (subgroupQuotientProj x₀ K)

The subgroup-cover projection is a C^n local diffeomorphism for the lifted atlas.

instance TauCeti.UniversalCover.instLieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {G : Type u_7} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I n G] : LieGroup I n (UniversalCover 1)

The universal cover of a Lie group, based at the identity, is a Lie group: its multiplication and inversion are continuous and lie over the C^n multiplication and inversion of G.