Re-charting a manifold by charts of its maximal atlas

Mathlib's ChartedSpace fixes one preferred chart chartAt H x at every point, and statements such as "in the chart at p, the function is a monomial in the coordinates" refer to it. A manifold M admits many charted-space structures with the same maximal atlas; this module picks one with prescribed charts and moves it to a homeomorphic copy of M (for instance a ULift, to change universes).

Given a homeomorphism e : M' ≃ₜ M and, for every point x : M, a chart c x of the maximal atlas of M whose source contains x, rechartedSpace e c hc is the charted-space structure on M' whose chart at p is e followed by c (e p). Its transition maps are those of the charts c x of M, so it is a manifold (isManifold_rechartedSpace) for which e is a diffeomorphism (rechartedDiffeomorph): in the charts e ≫ c x of M' and c x of M, the map e reads as the identity. The extended chart of M' at p is c (e p) ∘ e followed by the model embedding (extChartAt_rechartedSpace).

@[instance_reducible]

def Manifold.rechartedSpace {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) : ChartedSpace H M'

The charted space on M' with the charts e ≫ c (e p): for a homeomorphism e : M' ≃ₜ M and charts c x of M with x ∈ (c x).source, the atlas {e ≫ c x} with the chart at p equal to e ≫ c (e p).

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.chartAt_rechartedSpace {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (p : M') : chartAt H p = e.toOpenPartialHomeomorph.trans (c (e p))

The chart of rechartedSpace e c hc at p is e ≫ c (e p).

theorem Manifold.extChartAt_rechartedSpace {𝕜 : 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_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (p q : M') : ↑(extChartAt I p) q = ↑I (↑(c (e p)) (e q))

The extended chart of the re-charted space at p is I ∘ c (e p) ∘ e.

theorem Manifold.trans_symm_trans_trans_toOpenPartialHomeomorph {H : Type u_3} [TopologicalSpace H] {M : Type u_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (x y : M) : (e.toOpenPartialHomeomorph.trans (c x)).symm.trans (e.toOpenPartialHomeomorph.trans (c y)) = (c x).symm.trans (c y)

The transition map between two charts e ≫ c x and e ≫ c y is that between c x and c y: the homeomorphism e cancels.

theorem Manifold.isManifold_rechartedSpace {𝕜 : 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_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M] [IsManifold I n M] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (hcm : ∀ (x : M), c x ∈ IsManifold.maximalAtlas I n M) : IsManifold I n M'

The re-charted space is a manifold when the charts c x belong to the maximal atlas of M: its transition maps are the transition maps (c x)⁻¹ ≫ c y of M (trans_symm_trans_trans_toOpenPartialHomeomorph), which lie in the groupoid.

theorem Manifold.contMDiff_rechartedSpace {𝕜 : 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_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M] [IsManifold I n M] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (hcm : ∀ (x : M), c x ∈ IsManifold.maximalAtlas I n M) : ContMDiff I I n ⇑e

In the re-charted structure, e : M' → M is smooth: read in the charts e ≫ c x and c x, it is the identity.

theorem Manifold.contMDiff_symm_rechartedSpace {𝕜 : 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_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M] [IsManifold I n M] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (hcm : ∀ (x : M), c x ∈ IsManifold.maximalAtlas I n M) : ContMDiff I I n ⇑e.symm

In the re-charted structure, e⁻¹ : M → M' is smooth: read in the charts c x and e ≫ c x, it is the identity.

def Manifold.rechartedDiffeomorph {𝕜 : 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_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M] [IsManifold I n M] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (hcm : ∀ (x : M), c x ∈ IsManifold.maximalAtlas I n M) : Diffeomorph I I M' M n

e as a diffeomorphism from M' with the re-charted structure to M.

Equations

• Manifold.rechartedDiffeomorph e c hc hcm = { toEquiv := e.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem Manifold.coe_rechartedDiffeomorph {𝕜 : 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_4} [TopologicalSpace M] {M' : Type u_5} [TopologicalSpace M'] [ChartedSpace H M] [IsManifold I n M] (e : M' ≃ₜ M) (c : M → OpenPartialHomeomorph M H) (hc : ∀ (x : M), x ∈ (c x).source) (hcm : ∀ (x : M), c x ∈ IsManifold.maximalAtlas I n M) : ⇑(rechartedDiffeomorph e c hc hcm) = ⇑e

The diffeomorphism rechartedDiffeomorph is e on points.