The model with corners over the interior of its range

A model with corners I : H → E need not have open range, so it is in general not an open partial homeomorphism onto a subset of E. Restricting I to the preimage of the interior of its range repairs this. Its inverse then converts a C^n map from a manifold onto an open subset of E lying in the interior of the range of I, with C^n inverse, into a chart of the C^n maximal atlas. So coordinates found on an open subset of E are charts around interior points of a manifold, even when the model I itself has a boundary.

Main definitions

• ModelWithCorners.interiorChart: the restriction of I to the preimage of the interior of its range, as an open partial homeomorphism.

Main results

• OpenPartialHomeomorph.trans_interiorChart_symm_mem_maximalAtlas: an open partial homeomorphism from a manifold to E that is C^n with C^n inverse, followed by the inverse of I.interiorChart, is a chart of the C^n maximal atlas.
• PartialDiffeomorph.trans_trans_interiorChart_symm_mem_maximalAtlas: a partial diffeomorphism from a manifold to E, followed by a chart of the maximal atlas of E and by the inverse of I.interiorChart, is a chart of the C^n maximal atlas.

def ModelWithCorners.interiorChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : OpenPartialHomeomorph H E

The restriction of a model with corners I to the preimage of the interior of its range, as an open partial homeomorphism onto that interior.

@[simp]

theorem ModelWithCorners.interiorChart_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : ↑I.interiorChart = ↑I

@[simp]

theorem ModelWithCorners.interiorChart_coe_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : ↑I.interiorChart.symm = ↑I.symm

@[simp]

theorem ModelWithCorners.interiorChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : I.interiorChart.source = ↑I ⁻¹' interior (Set.range ↑I)

@[simp]

theorem ModelWithCorners.interiorChart_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} : I.interiorChart.target = interior (Set.range ↑I)

theorem OpenPartialHomeomorph.trans_interiorChart_symm_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 ℕ∞} [IsManifold I n M] {e : OpenPartialHomeomorph M E} (he : ContMDiffOn I (modelWithCornersSelf 𝕜 E) n (↑e) e.source) (he' : ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑e.symm) e.target) : e.trans I.interiorChart.symm ∈ IsManifold.maximalAtlas I n M

An open partial homeomorphism from a C^n manifold to the model vector space that is C^n with C^n inverse, followed by the inverse of I.interiorChart, is a chart of the C^n maximal atlas. No hypothesis on the model I is needed.

theorem PartialDiffeomorph.trans_trans_interiorChart_symm_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 ℕ∞} [IsManifold I n M] (Φ : PartialDiffeomorph I (modelWithCornersSelf 𝕜 E) M E n) {σ : OpenPartialHomeomorph E E} (hσ : σ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) n E) : (Φ.toOpenPartialHomeomorph.trans σ).trans I.interiorChart.symm ∈ IsManifold.maximalAtlas I n M

A partial diffeomorphism from M to the model vector space, followed by a chart σ of the maximal atlas of the vector space and read back through the interior chart of the model, is a chart of the maximal atlas of M.