Charts pulled back along a local homeomorphism

Let p : M → B be a local homeomorphism onto a charted space B. Each point x : M has an open neighbourhood that p maps homeomorphically onto an open subset of B; following this homeomorphism by the preferred chart of B at p x gives a chart of M at x. These charts form the pulled-back charted-space structure IsLocalHomeomorph.chartedSpaceComap. Every chart of M reads a point y as the chart of B at p x reads p y.

This is how a covering space of a manifold, such as the universal cover, receives its atlas. Mathlib pushes charts forward along a surjective local homeomorphism (IsLocalHomeomorph.chartedSpaceOfRightInverse); this file supplies the dual construction.

The transition maps of the pulled-back atlas are restrictions of transition maps of B, so the pulled-back charts form a C^n manifold whenever B is one, and p is then a C^n local diffeomorphism. A map into M is C^n exactly when it is continuous and its composite with p is C^n: in the pulled-back charts the two composites have the same coordinate expression. Conversely, any C^n manifold structure on M for which p is a C^n local diffeomorphism is compatible with the pulled-back charts, since a continuous map into M is C^n whenever its composite with a C^n local diffeomorphism is.

Main definitions

• IsLocalHomeomorph.chartedSpaceComap: the charts of B pulled back along p.

Main results

• IsLocalHomeomorph.isManifold_chartedSpaceComap: the pulled-back charts of a C^n manifold form a C^n manifold.
• IsLocalHomeomorph.contMDiff_chartedSpaceComap_iff: a map into M is C^n if and only if it is continuous and its composite with p is C^n; also in Within, At and On forms.
• IsLocalHomeomorph.isLocalDiffeomorph_chartedSpaceComap: p is a C^n local diffeomorphism for the pulled-back charts.
• IsLocalHomeomorph.compatible_chartedSpaceComap: any C^n manifold structure on M for which p is a C^n local diffeomorphism is compatible with the pulled-back charts.

References

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

@[instance_reducible]

noncomputable def IsLocalHomeomorph.chartedSpaceComap {H : Type u_3} [TopologicalSpace H] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) : ChartedSpace H M

The charted-space structure on the source of a local homeomorphism p : M → B pulled back from B: the chart at x is the local inverse of p at x, inverted, followed by the chart of B at p x.

theorem IsLocalHomeomorph.chartAt_chartedSpaceComap {H : Type u_3} [TopologicalSpace H] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) (x : M) : chartAt H x = (hp.localInverseAt x).symm.trans (chartAt H (p x))

The pulled-back chart at x is the local inverse of p at x, inverted, followed by the chart of B at p x.

@[simp]

theorem IsLocalHomeomorph.chartAt_chartedSpaceComap_apply {H : Type u_3} [TopologicalSpace H] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) (x y : M) : ↑(chartAt H x) y = ↑(chartAt H (p x)) (p y)

The pulled-back chart at x reads y as the chart of B at p x reads p y.

theorem IsLocalHomeomorph.extChartAt_chartedSpaceComap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) (x y : M) : ↑(extChartAt I x) y = ↑(extChartAt I (p x)) (p y)

The pulled-back extended chart at x reads y as the extended chart of B at p x reads p y.

theorem IsLocalHomeomorph.isManifold_chartedSpaceComap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) [IsManifold I n B] : IsManifold I n M

The charts of a C^n manifold pulled back along a local homeomorphism form a C^n manifold: their transition maps are restrictions of transition maps of the base.

theorem IsLocalHomeomorph.contMDiffWithinAt_chartedSpaceComap_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] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) {f : N → M} {s : Set N} {z : N} : ContMDiffWithinAt I' I n f s z ↔ ContinuousWithinAt f s z ∧ ContMDiffWithinAt I' I n (p ∘ f) s z

A map into the source of a local homeomorphism p is C^n within s at z for the pulled-back charts if and only if it is continuous within s at z and its composite with p is C^n within s at z.

theorem IsLocalHomeomorph.contMDiffAt_chartedSpaceComap_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] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) {f : N → M} {z : N} : ContMDiffAt I' I n f z ↔ ContinuousAt f z ∧ ContMDiffAt I' I n (p ∘ f) z

A map into the source of a local homeomorphism p is C^n at z for the pulled-back charts if and only if it is continuous at z and its composite with p is C^n at z.

theorem IsLocalHomeomorph.contMDiffOn_chartedSpaceComap_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] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) {f : N → M} {s : Set N} : ContMDiffOn I' I n f s ↔ ContinuousOn f s ∧ ContMDiffOn I' I n (p ∘ f) s

A map into the source of a local homeomorphism p is C^n on s for the pulled-back charts if and only if it is continuous on s and its composite with p is C^n on s.

theorem IsLocalHomeomorph.contMDiff_chartedSpaceComap_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] {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) {f : N → M} : ContMDiff I' I n f ↔ Continuous f ∧ ContMDiff I' I n (p ∘ f)

A map into the source of a local homeomorphism p is C^n for the pulled-back charts if and only if it is continuous and its composite with p is C^n.

theorem IsLocalHomeomorph.contMDiff_chartedSpaceComap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) : ContMDiff I I n p

A local homeomorphism is C^n for the charts it pulls back.

theorem IsLocalHomeomorph.isLocalDiffeomorph_chartedSpaceComap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) : IsLocalDiffeomorph I I n p

A local homeomorphism onto a C^n manifold is a C^n local diffeomorphism for the charts it pulls back.

theorem IsLocalHomeomorph.compatible_chartedSpaceComap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_7} [TopologicalSpace M] {B : Type u_8} [TopologicalSpace B] [ChartedSpace H B] {p : M → B} (hp : IsLocalHomeomorph p) [IsManifold I n B] [c : ChartedSpace H M] [IsManifold I n M] (hpc : IsLocalDiffeomorph I I n p) (e : OpenPartialHomeomorph M H) : e ∈ ChartedSpace.atlas → ∀ e' ∈ ChartedSpace.atlas, e.symm.trans e' ∈ contDiffGroupoid n I

Any C^n manifold structure on the source of a local homeomorphism p onto a C^n manifold, for which p is a C^n local diffeomorphism, is compatible with the charts pulled back along p. So the pulled-back structure is the only such structure, up to equivalence of atlases.