Charts of the model vector space read through a preferred chart

On a manifold with a boundaryless model I, the extended chart at a point identifies a neighbourhood of that point with an open subset of the model vector space E. A chart c of the C^n maximal atlas of E itself can therefore be read through it: the composite I.symm ∘ c ∘ extChartAt I x is a chart of the manifold, and it lies in the C^n maximal atlas. This carries normal forms found in the model vector space, such as those produced by an inverse function theorem in coordinates, back to the manifold.

A chart φ of the maximal atlas of a manifold modelled on E, times the identity of a normed space F, is smooth on its source as a map M × F → E × F, and so is its inverse on its target; here E × F carries the model 𝓘(𝕜, E × F) of the vector space rather than the product model.

Similarly, a maximal-atlas chart c transported to another normed space F by a C^n homeomorphism Ψ : E ≃ₜ F via OpenPartialHomeomorph.extendTrans is C^n on its source, and its inverse is C^n on its target when Ψ.symm is C^n.

Main results

• TauCeti.conj_chartAt_mem_maximalAtlas: a chart of the model vector space, read through the preferred chart at a point, is a chart of the manifold's maximal atlas.

• TauCeti.contMDiffAt_prodMap_id_of_mem_maximalAtlas, TauCeti.contMDiffAt_prodMap_symm_id_of_mem_maximalAtlas: a chart times the identity, and its inverse, are smooth.

• TauCeti.conj_chartAt_source and TauCeti.comp_conj_chartAt: the domain of that chart is where the extended chart lands in the domain of c, and in the model vector space it reads as c ∘ extChartAt I x.

• OpenPartialHomeomorph.toDiffeomorphSourceTarget: a maximal-atlas chart as a native C^n diffeomorphism between its intrinsic open source and target, including models with corners.

• TauCeti.extChartAtDiffeomorph: on a boundaryless model, the extended chart at a point as a native C^n diffeomorphism from TauCeti.chartSourceOpens onto TauCeti.extChartTargetOpens, the open target of the chart in the model vector space.

• OpenPartialHomeomorph.contMDiffOn_extendTrans and OpenPartialHomeomorph.contMDiffOn_extendTrans_symm: C^n regularity of a maximal-atlas chart transported by OpenPartialHomeomorph.extendTrans and of its inverse.

theorem TauCeti.conj_chartAt_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] (x : M) (c : OpenPartialHomeomorph E E) : ((((chartAt H x).transHomeomorph I.toHomeomorph).trans c).transHomeomorph I.toHomeomorph.symm).source = (extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' c.source

On a boundaryless model, the domain of a chart c of the model vector space read through the preferred chart at x is the set of points of the domain of extChartAt I x that it sends into the domain of c.

theorem TauCeti.comp_conj_chartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] (x : M) (c : OpenPartialHomeomorph E E) : ↑I ∘ ↑((((chartAt H x).transHomeomorph I.toHomeomorph).trans c).transHomeomorph I.toHomeomorph.symm) = ↑c ∘ ↑(extChartAt I x)

On a boundaryless model, a chart c of the model vector space read through the preferred chart at x is c ∘ extChartAt I x in the model vector space.

theorem TauCeti.conj_chartAt_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [I.Boundaryless] [IsManifold I n M] (x : M) {c : OpenPartialHomeomorph E E} (hc : c ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) n E) : (((chartAt H x).transHomeomorph I.toHomeomorph).trans c).transHomeomorph I.toHomeomorph.symm ∈ IsManifold.maximalAtlas I n M

A chart of the model vector space, read through the preferred chart at x of a manifold with a boundaryless model, is a chart of the manifold's maximal atlas.

theorem TauCeti.contMDiffAt_prodMap_id_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {F : Type u_5} {M' : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace M'] [ChartedSpace E M'] {φ : OpenPartialHomeomorph M' E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) n M') {y : M' × F} (hy : y.1 ∈ φ.source) : ContMDiffAt ((modelWithCornersSelf 𝕜 E).prod (modelWithCornersSelf 𝕜 F)) (modelWithCornersSelf 𝕜 (E × F)) n (Prod.map (↑φ) id) y

A chart of the maximal atlas times the identity of a normed space F is smooth on its source, as a map into the vector space E × F.

theorem TauCeti.contMDiffAt_prodMap_symm_id_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {F : Type u_5} {M' : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace M'] [ChartedSpace E M'] {φ : OpenPartialHomeomorph M' E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) n M') {y : E × F} (hy : y.1 ∈ φ.target) : ContMDiffAt (modelWithCornersSelf 𝕜 (E × F)) ((modelWithCornersSelf 𝕜 E).prod (modelWithCornersSelf 𝕜 F)) n (Prod.map (↑φ.symm) id) y

The inverse of a chart of the maximal atlas, times the identity of a normed space F, is smooth on its target, as a map out of the vector space E × F.

theorem OpenPartialHomeomorph.contMDiffOn_extendTrans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (c : OpenPartialHomeomorph M H) (hc : c ∈ IsManifold.maximalAtlas I n M) {Ψ : E ≃ₜ F} (hΨ : ContDiff 𝕜 n ⇑Ψ) : ContMDiffOn I (modelWithCornersSelf 𝕜 F) n (↑(c.extendTrans I Ψ)) (c.extendTrans I Ψ).source

A chart c of the maximal C^n atlas, read in E and moved to F by a C^n homeomorphism Ψ, is C^n on its source.

theorem OpenPartialHomeomorph.contMDiffOn_extendTrans_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (c : OpenPartialHomeomorph M H) (hc : c ∈ IsManifold.maximalAtlas I n M) {Ψ : E ≃ₜ F} (hΨ : ContDiff 𝕜 n ⇑Ψ.symm) : ContMDiffOn (modelWithCornersSelf 𝕜 F) I n (↑(c.extendTrans I Ψ).symm) (c.extendTrans I Ψ).target

The inverse of c.extendTrans I Ψ, for c in the maximal C^n atlas and Ψ.symm of class C^n, is C^n on its target.

def OpenPartialHomeomorph.toDiffeomorphSourceTarget {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (c : OpenPartialHomeomorph M H) (hc : c ∈ IsManifold.maximalAtlas I n M) : Diffeomorph I I (↥{ carrier := c.source, is_open' := ⋯ }) (↥{ carrier := c.target, is_open' := ⋯ }) n

A chart in the maximal atlas is a native diffeomorphism between its intrinsic open source and open target. The target is open in H; no boundaryless hypothesis is needed.

@[simp]

theorem OpenPartialHomeomorph.toDiffeomorphSourceTarget_apply_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (c : OpenPartialHomeomorph M H) (hc : c ∈ IsManifold.maximalAtlas I n M) (x : ↥{ carrier := c.source, is_open' := ⋯ }) : ↑((c.toDiffeomorphSourceTarget hc) x) = ↑c ↑x

@[simp]

theorem OpenPartialHomeomorph.toDiffeomorphSourceTarget_symm_apply_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} (c : OpenPartialHomeomorph M H) (hc : c ∈ IsManifold.maximalAtlas I n M) (x : ↥{ carrier := c.target, is_open' := ⋯ }) : ↑((c.toDiffeomorphSourceTarget hc).symm x) = ↑c.symm ↑x

def TauCeti.chartSourceOpens (H : Type u_3) {M : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : TopologicalSpace.Opens M

The domain of the preferred chart at x, as an open subset of the manifold.

@[simp]

theorem TauCeti.coe_chartSourceOpens {H : Type u_3} {M : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : ↑(chartSourceOpens H x) = (chartAt H x).source

@[simp]

theorem TauCeti.mem_chartSourceOpens {H : Type u_3} {M : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {x y : M} : y ∈ chartSourceOpens H x ↔ y ∈ (chartAt H x).source

def TauCeti.extChartTargetOpens {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] (x : M) : TopologicalSpace.Opens E

On a boundaryless model, the target of the extended chart at x, as an open subset of the model vector space.

@[simp]

theorem TauCeti.coe_extChartTargetOpens {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] (x : M) : ↑(extChartTargetOpens I x) = (extChartAt I x).target

@[simp]

theorem TauCeti.mem_extChartTargetOpens {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] {x : M} {z : E} : z ∈ extChartTargetOpens I x ↔ z ∈ (extChartAt I x).target

def TauCeti.extChartAtDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] (n : WithTop ℕ∞) [I.Boundaryless] [IsManifold I n M] (x : M) : Diffeomorph I (modelWithCornersSelf 𝕜 E) (↥(chartSourceOpens H x)) (↥(extChartTargetOpens I x)) n

On a boundaryless model, the extended chart at x is a native C^n diffeomorphism from the domain of the chart onto its open target in the model vector space.

@[simp]

theorem TauCeti.coe_extChartAtDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [I.Boundaryless] [IsManifold I n M] (x : M) (p : ↥(chartSourceOpens H x)) : ↑((extChartAtDiffeomorph n x) p) = ↑(extChartAt I x) ↑p

@[simp]

theorem TauCeti.coe_extChartAtDiffeomorph_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [I.Boundaryless] [IsManifold I n M] (x : M) (z : ↥(extChartTargetOpens I x)) : ↑((extChartAtDiffeomorph n x).symm z) = ↑(extChartAt I x).symm ↑z