Replacing a boundaryless model by its vector space

BoundarylessModel I M carries the topology of M, but its charts take values in the model vector space E rather than in H. A chart c is replaced by I ∘ c. The extended charts do not change, and the identity is a diffeomorphism.

This lets constructions stated for self-modelled manifolds apply to arbitrary boundaryless models without installing a second atlas on the original manifold. In particular, local normal forms and implicit-function constructions can retain their actual coordinates.

def TauCeti.BoundarylessModel {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (_I : ModelWithCorners 𝕜 E H) (M : Type u_4) : Type u_4

A copy of a manifold on which the charts of a boundaryless model I take values in its vector space. The topology is unchanged; the original manifold retains its original atlas.

@[instance_reducible]

instance TauCeti.BoundarylessModel.instTopologicalSpace {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] : TopologicalSpace (BoundarylessModel I M)

The model copy inherits the topology of the original manifold.

def TauCeti.BoundarylessModel.homeomorph {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] : M ≃ₜ BoundarylessModel I M

The identity homeomorphism to the copy with vector-space-valued charts.

theorem TauCeti.BoundarylessModel.coe_homeomorph {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] : ⇑(homeomorph I M) = id

The carrier map of the homeomorphism is the identity.

theorem TauCeti.BoundarylessModel.coe_homeomorph_symm {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] : ⇑(homeomorph I M).symm = id

The inverse carrier map is also the identity.

@[simp]

theorem TauCeti.BoundarylessModel.homeomorph_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] (x : M) : (homeomorph I M) x = x

The homeomorphism sends each point to the same point of the model copy.

@[simp]

theorem TauCeti.BoundarylessModel.homeomorph_symm_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_4) [TopologicalSpace M] (x : BoundarylessModel I M) : (homeomorph I M).symm x = x

The inverse homeomorphism sends each point back to the same original point.

def TauCeti.BoundarylessModel.chart {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) : OpenPartialHomeomorph (BoundarylessModel I M) E

Replace an H-valued chart by its E-valued extended coordinates.

@[simp]

theorem TauCeti.BoundarylessModel.chart_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) (y : BoundarylessModel I M) : ↑(chart I c) y = ↑I (↑c ((homeomorph I M).symm y))

@[simp]

theorem TauCeti.BoundarylessModel.chart_symm_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) (v : E) : ↑(chart I c).symm v = (homeomorph I M) (↑c.symm (↑I.symm v))

@[simp]

theorem TauCeti.BoundarylessModel.chart_source {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) : (chart I c).source = ⇑(homeomorph I M).symm ⁻¹' c.source

@[simp]

theorem TauCeti.BoundarylessModel.chart_target {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) : (chart I c).target = ↑I.symm ⁻¹' c.target

theorem TauCeti.BoundarylessModel.chart_toPartialEquiv {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) : (chart I c).toPartialEquiv = c.extend I

The new chart has exactly the old extended partial equivalence. The carrier and topology of the copy are definitionally those of M, so the two partial equivalences have the same type.

def TauCeti.BoundarylessModel.originalChart {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) : OpenPartialHomeomorph M H

Return a vector-space-valued chart on the copy to the original model.

@[simp]

theorem TauCeti.BoundarylessModel.chart_originalChart {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) : chart I (originalChart I φ) = φ

Returning a chart to the original model and extending it again recovers the same chart.

@[simp]

theorem TauCeti.BoundarylessModel.originalChart_chart {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (c : OpenPartialHomeomorph M H) : originalChart I (chart I c) = c

Extending an original chart and returning it to its model recovers the original chart.

theorem TauCeti.BoundarylessModel.originalChart_extend {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) : (originalChart I φ).extend I = φ.toPartialEquiv

An arbitrary chart on the copy and its corresponding original chart have identical extended coordinates, source and target.

@[simp]

theorem TauCeti.BoundarylessModel.originalChart_source {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) : (originalChart I φ).source = ⇑(homeomorph I M) ⁻¹' φ.source

A chart of the copy and the corresponding original chart have the same source.

theorem TauCeti.BoundarylessModel.originalChart_extend_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) (y : M) : ↑((originalChart I φ).extend I) y = ↑φ ((homeomorph I M) y)

The extended original chart of a chart of the copy has the same coordinates.

theorem TauCeti.BoundarylessModel.originalChart_extend_symm_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) (v : E) : ↑((originalChart I φ).extend I).symm v = (homeomorph I M).symm (↑φ.symm v)

The extended original chart of a chart of the copy has the same inverse.

theorem TauCeti.BoundarylessModel.originalChart_extend_target {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) : ((originalChart I φ).extend I).target = φ.target

The extended original chart of a chart of the copy has the same target.

@[instance_reducible]

instance TauCeti.BoundarylessModel.instChartedSpace {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] : ChartedSpace E (BoundarylessModel I M)

The model copy receives the atlas obtained by extending the original charts to E.

theorem TauCeti.BoundarylessModel.atlas_eq {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] : atlas E (BoundarylessModel I M) = chart I '' atlas H M

The atlas consists of the extended original charts.

theorem TauCeti.BoundarylessModel.chartAt_eq {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (x : BoundarylessModel I M) : chartAt E x = chart I (chartAt H ((homeomorph I M).symm x))

Preferred charts are transported without making any new choices.

theorem TauCeti.BoundarylessModel.chartAt_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (z y : BoundarylessModel I M) : ↑(chartAt E z) y = ↑(extChartAt I ((homeomorph I M).symm z)) ((homeomorph I M).symm y)

The preferred chart of the copy has the coordinates of the preferred extended chart.

theorem TauCeti.BoundarylessModel.chartAt_symm_apply {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (z : BoundarylessModel I M) (v : E) : (homeomorph I M).symm (↑(chartAt E z).symm v) = ↑(extChartAt I ((homeomorph I M).symm z)).symm v

The inverse preferred chart of the copy is the inverse preferred extended chart.

theorem TauCeti.BoundarylessModel.extChartAt_eq {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (x : BoundarylessModel I M) : extChartAt (modelWithCornersSelf 𝕜 E) x = extChartAt I ((homeomorph I M).symm x)

The extended preferred chart is unchanged by the model transport.

@[simp]

theorem TauCeti.BoundarylessModel.chart_mem_maximalAtlas_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (c : OpenPartialHomeomorph M H) (n : WithTop ℕ∞) : chart I c ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) n (BoundarylessModel I M) ↔ c ∈ IsManifold.maximalAtlas I n M

Membership in the maximal atlas is preserved by extending a chart to the vector space.

@[simp]

theorem TauCeti.BoundarylessModel.originalChart_mem_maximalAtlas_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (φ : OpenPartialHomeomorph (BoundarylessModel I M) E) (n : WithTop ℕ∞) : originalChart I φ ∈ IsManifold.maximalAtlas I n M ↔ φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) n (BoundarylessModel I M)

Every maximal chart on the copy corresponds to a maximal chart on the original manifold.

instance TauCeti.BoundarylessModel.instIsManifoldModelWithCornersSelf {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] : IsManifold (modelWithCornersSelf 𝕜 E) n (BoundarylessModel I M)

Replacing a boundaryless model by its vector space preserves manifold regularity.

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

The identity, as a diffeomorphism from the original model to the self-modelled copy.

@[simp]

theorem TauCeti.BoundarylessModel.coe_diffeomorph {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (n : WithTop ℕ∞) : ⇑(diffeomorph I n) = ⇑(homeomorph I M)

The diffeomorphism has the same underlying map as the identity homeomorphism.

@[simp]

theorem TauCeti.BoundarylessModel.coe_diffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] (n : WithTop ℕ∞) : ⇑(diffeomorph I n).symm = ⇑(homeomorph I M).symm

The inverse diffeomorphism has the inverse identity map as its underlying function.

@[simp]

theorem TauCeti.BoundarylessModel.mdifferentiableAt_source_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (x : BoundarylessModel I M) : MDiffAt (f ∘ ⇑(homeomorph I M).symm) x ↔ MDiffAt f ((homeomorph I M).symm x)

Changing the source model preserves differentiability, even when no manifold regularity assumption is imposed on either atlas.

theorem TauCeti.BoundarylessModel.mfderiv_source {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (x : BoundarylessModel I M) : mfderiv% (f ∘ ⇑(homeomorph I M).symm) x = mfderiv% f ((homeomorph I M).symm x) ∘SL ↑(tangentSpaceCastModel I ((homeomorph I M).symm x)).symm ∘SL ↑(tangentSpaceCastModel (modelWithCornersSelf 𝕜 E) x)

The source-side derivative comparison, with the tangent spaces identified explicitly through their common model vector space. No differentiability hypothesis is needed.

@[simp]

theorem TauCeti.BoundarylessModel.mfderiv_source_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace N] [ChartedSpace H' N] (f : M → N) (x : BoundarylessModel I M) : mfderiv% (f ∘ ⇑(homeomorph I M).symm) x = 0 ↔ mfderiv% f ((homeomorph I M).symm x) = 0

Changing the source model does not change whether the derivative vanishes.

@[simp]

theorem TauCeti.BoundarylessModel.mdifferentiableAt_target_iff {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace N] [ChartedSpace H' N] (f : N → M) (x : N) : MDiffAt (⇑(homeomorph I M) ∘ f) x ↔ MDiffAt f x

Changing the target model preserves differentiability.

theorem TauCeti.BoundarylessModel.mfderiv_target {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [I.Boundaryless] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace N] [ChartedSpace H' N] (f : N → M) (x : N) : mfderiv% (⇑(homeomorph I M) ∘ f) x = ↑(tangentSpaceCastModel (modelWithCornersSelf 𝕜 E) ((homeomorph I M) (f x))).symm ∘SL ↑(tangentSpaceCastModel I (f x)) ∘SL mfderiv% f x

The target-side derivative comparison through the common model vector space.