Charts of the maximal atlas as partial diffeomorphisms

Bookkeeping for the charts of the maximal analytic atlas of a manifold: an analytic open partial homeomorphism of the model space with analytic inverse lies in the analytic groupoid (mem_contDiffGroupoid_omega_of_analytic', from mem_contDiffGroupoid_self with AnalyticOnNhd.contDiffOn); every chart of the maximal atlas is a PartialDiffeomorph 𝓘 𝓘 M E ω (Mathlib's contMDiffOn_of_mem_maximalAtlas and contMDiffOn_symm_of_mem_maximalAtlas), so the composite e'⁻¹ ∘ e of two charts is a PartialDiffeomorph 𝓘 𝓘 M M ω (PartialDiffeomorph.chartChange, from PartialDiffeomorph.trans and .symm) and a local analytic isomorphism at every point of its source (PartialDiffeomorph.isLocalDiffeomorphAt). The composite of a chart with an analytic open partial homeomorphism of E with analytic inverse is again a chart of the maximal atlas (trans_mem_maximalAtlas_of_analytic' of Hironaka/Manifold/AdaptedChart.lean). The chart change is the coordinate swap of Hironaka/Manifold/Chart/Swap.lean.

theorem Manifold.mem_contDiffGroupoid_omega_of_analytic' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e₀ : OpenPartialHomeomorph E E) (h : AnalyticOnNhd 𝕜 (↑e₀) e₀.source) (h' : AnalyticOnNhd 𝕜 (↑e₀.symm) e₀.target) : e₀ ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)

An open partial homeomorphism of E that is analytic with analytic inverse lies in the analytic groupoid of the model space; the form used by trans_mem_maximalAtlas_of_analytic' and by the blow-up atlas.

def PartialDiffeomorph.ofMemMaximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M E ⊤

A chart of the maximal atlas as a PartialDiffeomorph 𝓘 𝓘 M E ω.

Equations

• PartialDiffeomorph.ofMemMaximalAtlas he = { toPartialEquiv := e.toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }

theorem PartialDiffeomorph.ofMemMaximalAtlas_toPartialEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : (ofMemMaximalAtlas he).toPartialEquiv = e.toPartialEquiv

The underlying partial equivalence of ofMemMaximalAtlas is the chart's.

theorem Manifold.exists_partialDiffeomorph_of_mem_maximalAtlas' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : ∃ (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M E ⊤), Φ.toPartialEquiv = e.toPartialEquiv

Every chart of the maximal atlas is a PartialDiffeomorph 𝓘 𝓘 M E ω.

def PartialDiffeomorph.chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤

The chart change e'⁻¹ ∘ e of two charts of the maximal atlas as a PartialDiffeomorph 𝓘 𝓘 M M ω.

Equations

• PartialDiffeomorph.chartChange he he' = (PartialDiffeomorph.ofMemMaximalAtlas he).trans (PartialDiffeomorph.ofMemMaximalAtlas he').symm

theorem PartialDiffeomorph.chartChange_toPartialEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : (chartChange he he').toPartialEquiv = (e.trans e'.symm).toPartialEquiv

The chart change as a partial equivalence is e ≫ e'.symm.

theorem Manifold.exists_partialDiffeomorph_chartChange' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : ∃ (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤), Φ.toPartialEquiv = (e.trans e'.symm).toPartialEquiv ∧ ∀ x ∈ Φ.source, IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑Φ.toPartialEquiv) x

The composite e'⁻¹ ∘ e of two charts of the maximal atlas is a PartialDiffeomorph 𝓘 𝓘 M M ω, a local analytic isomorphism at every point of its source.