Pulling back charted-space and groupoid structures along a homeomorphism

Given a charted space M modelled on H and a homeomorphism e : N ≃ₜ M, the space N receives the pulled-back charted-space structure Homeomorph.pullbackChartedSpace e, whose atlas is {e.transOpenPartialHomeomorph c | c ∈ atlas H M} and whose chart at x is the chart of M at e x precomposed with e.

The coordinate changes of the pulled-back atlas are equal to the coordinate changes of the original atlas (Mathlib's Homeomorph.transOpenPartialHomeomorph_symm_trans): for a global homeomorphism nothing of the transport survives in the overlaps. Consequently the pulled-back structure satisfies every structure groupoid that M satisfies, with no ClosedUnderRestriction assumption, and e itself is a structomorphism. For the C^n groupoid of a model I this makes N a C^n manifold, and e a C^n diffeomorphism whose underlying map is e.

This complements Mathlib's Homeomorph.chartedSpace, which pushes charts forward through local inverses chosen by the IsLocalHomeomorph machinery, and Tau Ceti's IsLocalHomeomorph.chartedSpaceComap, which pulls charts back along local inverses of a local homeomorphism. Composing with the global homeomorphism instead keeps the charts explicit, and makes the transport strictly functorial: pulling back along Homeomorph.refl returns the original structure, pulling back along a composite is pulling back twice, and pulling back along e and then along e.symm returns the original structure.

The construction does not by itself compare the pulled-back structure with a structure that N already carries. When N is a C^n manifold and e is a C^n diffeomorphism, the pulled-back charts belong to the maximal atlas of N, so the two structures are compatible.

Main definitions

• Homeomorph.pullbackChartedSpace e: the charted-space structure on N pulled back along e : N ≃ₜ M.
• Homeomorph.pullbackStructomorph e G: e as a G-structomorphism for the pulled-back structure.
• Homeomorph.pullbackDiffeomorph e I n: e as a C^n diffeomorphism for the pulled-back structure.

Main results

• Homeomorph.pullback_hasGroupoid: the pulled-back structure satisfies every structure groupoid that the original structure satisfies.
• Homeomorph.pullback_isManifold: the pulled-back structure of a C^n manifold is a C^n manifold.
• Homeomorph.pullbackChartedSpace_refl, Homeomorph.pullbackChartedSpace_trans and Homeomorph.pullbackChartedSpace_symm_pullbackChartedSpace: the identity, composition and inverse laws of the transport.
• Diffeomorph.transOpenPartialHomeomorph_mem_maximalAtlas: a C^n diffeomorphism pulls a chart of the maximal atlas of its target back to a chart of the maximal atlas of its source.
• Diffeomorph.atlas_pullbackChartedSpace_subset_maximalAtlas: the charts pulled back along a C^n diffeomorphism belong to the maximal atlas of its source.

The definitions and the first lemmas follow the Mathlib pull request mathlib4#42847 by Ryan Shin, which adds Mathlib.Geometry.Manifold.PullbackGroupoid.

References

• Shoshichi Kobayashi and Katsumi Nomizu, Foundations of Differential Geometry, Volume I, Chapter I, Section 1, for atlases compatible with a pseudogroup.

@[instance_reducible]

def Homeomorph.pullbackChartedSpace {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) : ChartedSpace H N

The charted-space structure on N pulled back along a homeomorphism e : N ≃ₜ M: the atlas is {e.transOpenPartialHomeomorph c | c ∈ atlas H M} and the chart at x is the chart of M at e x precomposed with e.

@[simp]

theorem Homeomorph.pullbackChartedSpace_chartAt {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) (x : N) : chartAt H x = e.transOpenPartialHomeomorph (chartAt H (e x))

The pulled-back chart at x is the chart of M at e x precomposed with e.

@[simp]

theorem Homeomorph.pullbackChartedSpace_atlas {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) : atlas H N = (fun (x : OpenPartialHomeomorph M H) => e.transOpenPartialHomeomorph x) '' atlas H M

The pulled-back atlas consists of the charts of M precomposed with e.

theorem Homeomorph.transOpenPartialHomeomorph_mem_pullbackChartedSpace_atlas {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) {c : OpenPartialHomeomorph M H} (hc : c ∈ atlas H M) : e.transOpenPartialHomeomorph c ∈ atlas H N

A chart of M precomposed with e is a chart of the pulled-back atlas.

theorem Homeomorph.pullbackChartedSpace_refl {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] : (Homeomorph.refl M).pullbackChartedSpace = inst✝

Pulling back along the identity homeomorphism returns the original structure.

theorem Homeomorph.pullbackChartedSpace_trans {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {P : Type u_4} [TopologicalSpace P] (e₁ : P ≃ₜ N) (e₂ : N ≃ₜ M) : (e₁.trans e₂).pullbackChartedSpace = e₁.pullbackChartedSpace

Pulling back along a composite of homeomorphisms is pulling back twice.

theorem Homeomorph.pullbackChartedSpace_symm_pullbackChartedSpace {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) : e.symm.pullbackChartedSpace = inst✝

Pulling back along e and then along e.symm returns the original structure.

theorem Homeomorph.pullback_hasGroupoid {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) (G : StructureGroupoid H) [HasGroupoid M G] : HasGroupoid N G

The pulled-back structure satisfies every structure groupoid that the original structure satisfies, since its coordinate changes are coordinate changes of M.

def Homeomorph.pullbackStructomorph {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) (G : StructureGroupoid H) [HasGroupoid M G] : Structomorph G N M

A homeomorphism onto a G-structured space is a G-structomorphism for the pulled-back structure.

@[simp]

theorem Homeomorph.pullbackStructomorph_toHomeomorph {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) (G : StructureGroupoid H) [HasGroupoid M G] : (e.pullbackStructomorph G).toHomeomorph = e

The underlying homeomorphism of the pulled-back structomorphism is e.

theorem Homeomorph.pullbackChartedSpace_extChartAt {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (e : N ≃ₜ M) (x : N) : extChartAt I x = e.transPartialEquiv (extChartAt I (e x))

The pulled-back extended chart at x is e followed by the extended chart of M at e x.

theorem Homeomorph.pullback_isManifold {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (e : N ≃ₜ M) [IsManifold I n M] : IsManifold I n N

The structure pulled back from a C^n manifold along a homeomorphism is a C^n manifold.

def Homeomorph.pullbackDiffeomorph {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (e : N ≃ₜ M) : Diffeomorph I I N M n

A homeomorphism onto a charted space is a C^n diffeomorphism for the pulled-back structure: read in a pulled-back chart and in the corresponding chart of M, both it and its inverse are the identity.

@[simp]

theorem Homeomorph.coe_pullbackDiffeomorph {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (e : N ≃ₜ M) : ⇑(pullbackDiffeomorph I n e) = ⇑e

The underlying map of the pulled-back diffeomorphism is e.

@[simp]

theorem Homeomorph.coe_pullbackDiffeomorph_symm {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (e : N ≃ₜ M) : ⇑(pullbackDiffeomorph I n e).symm = ⇑e.symm

The underlying map of the inverse of the pulled-back diffeomorphism is e.symm.

@[simp]

theorem Homeomorph.pullbackDiffeomorph_toHomeomorph {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (e : N ≃ₜ M) : (pullbackDiffeomorph I n e).toHomeomorph = e

The underlying homeomorphism of the pulled-back diffeomorphism is e.

theorem Diffeomorph.transOpenPartialHomeomorph_mem_maximalAtlas {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} [ChartedSpace H N] [IsManifold I n N] (h : Diffeomorph I I N M n) {φ : OpenPartialHomeomorph M H} (hφ : φ ∈ IsManifold.maximalAtlas I n M) : h.toHomeomorph.transOpenPartialHomeomorph φ ∈ IsManifold.maximalAtlas I n N

A C^n diffeomorphism h : N ≃ₘ^n⟮I, I⟯ M pulls a chart φ of the maximal C^n atlas of M back to the chart φ ∘ h of the maximal C^n atlas of N. For a mere homeomorphism the pulled-back chart lies in the topological atlas, but not in general in the maximal C^n atlas.

theorem Diffeomorph.atlas_pullbackChartedSpace_subset_maximalAtlas {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} [ChartedSpace H N] [IsManifold I n N] [IsManifold I n M] (h : Diffeomorph I I N M n) : ChartedSpace.atlas ⊆ IsManifold.maximalAtlas I n N

The charts pulled back along a C^n diffeomorphism h : N ≃ₘ^n⟮I, I⟯ M belong to the maximal C^n atlas of N. So the pulled-back structure is compatible with the structure that N already carries.