Charts transported along partial diffeomorphisms

A chart φ of the maximal analytic atlas of M₁, composed with the inverse of a partial diffeomorphism g : M₁ → M₂, is a chart transportChart g φ = g⁻¹ ≫ φ of the maximal atlas of M₂ (transportChart_mem_maximalAtlas: an open partial homeomorphism of E which is C^ω in both directions lies in the analytic groupoid, mem_contDiffGroupoid_of_contMDiffOn). When g carries Y₁ ∩ g.source onto Y₂ ∩ g.target it carries the adapted charts of Y₁ inside its source to adapted charts of Y₂ (isAdaptedChart_transportChart); hence the preimage h⁻¹(Y) of a closed submanifold of codimension c under a local analytic isomorphism h : N → M is a closed submanifold of codimension c, its adapted charts being those of Y transported along the local inverses of h (IsClosedSubmanifold.preimage_of_isLocalDiffeomorph; the analytic form of the centres Z_i ×_X Y of the pull-back of a blow-up sequence [Kol07, 30.1]).

These are the chart-level ingredients of the functoriality of the blowing-up under local isomorphisms (Hironaka.Manifold.BlowUp.Functor) and of its lift along local analytic isomorphisms (Hironaka.Manifold.FiniteSuccession.Lift).

Charts transported along a partial diffeomorphism

theorem Manifold.analyticOnNhd_of_contMDiffOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → E} {s : Set E} (h : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f s) (hs : IsOpen s) : AnalyticOnNhd 𝕜 f s

A C^ω map between open subsets of E is analytic there.

theorem Manifold.mem_contDiffGroupoid_of_contMDiffOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : OpenPartialHomeomorph E E) (hf : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑f) f.source) (hf' : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑f.symm) f.target) : f ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)

An open partial homeomorphism of E which is C^ω in both directions lies in the analytic groupoid.

noncomputable def Manifold.transportChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) (φ : OpenPartialHomeomorph M₁ E) : OpenPartialHomeomorph M₂ E

A chart of M₁ composed with the inverse of a partial diffeomorphism g : M₁ → M₂.

Equations

• Manifold.transportChart g φ = g.symm.toOpenPartialHomeomorph.trans φ

@[simp]

theorem Manifold.transportChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) {φ : OpenPartialHomeomorph M₁ E} : (transportChart g φ).source = g.target ∩ g.invFun ⁻¹' φ.source

The source of the transported chart: the points of g.target whose preimage lies in φ.source.

theorem Manifold.transportChart_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) {φ : OpenPartialHomeomorph M₁ E} (x : M₂) : ↑(transportChart g φ) x = ↑φ (g.invFun x)

The transported chart reads φ after g⁻¹.

theorem Manifold.transportChart_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) {φ : OpenPartialHomeomorph M₁ E} : (transportChart g φ).target = φ.target ∩ ↑φ.symm ⁻¹' g.source

The target of the transported chart.

theorem Manifold.transportChart_symm_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) {φ : OpenPartialHomeomorph M₁ E} (v : E) : ↑(transportChart g φ).symm v = ↑g.toPartialEquiv (↑φ.symm v)

The inverse of the transported chart is g ∘ φ⁻¹.

theorem Manifold.transportChart_target_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) {φ : OpenPartialHomeomorph M₁ E} (hsub : φ.source ⊆ g.source) : (transportChart g φ).target = φ.target

When φ.source ⊆ g.source the transported chart keeps the target of φ.

theorem Manifold.mem_maximalAtlas_of_contMDiffOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂] (χ : OpenPartialHomeomorph M₂ E) (hχ : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑χ) χ.source) (hχ' : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑χ.symm) χ.target) : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M₂

A chart χ : M₂ → E which is C^ω with C^ω inverse lies in the maximal atlas.

theorem Manifold.transportChart_mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) {φ : OpenPartialHomeomorph M₁ E} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂] (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M₁) : transportChart g φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M₂

The transported chart lies in the maximal atlas.

Charts carrying one centre to another

theorem Manifold.mem_iff_apply_mem_of_image_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] {Y₁ : Set M₁} {Y₂ : Set M₂} (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) (hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target) {x : M₁} (hx : x ∈ g.source) : x ∈ Y₁ ↔ ↑g.toPartialEquiv x ∈ Y₂

g carries the centre to the centre, pointwise on its source.

theorem Manifold.image_symm_eq_of_image_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] {Y₁ : Set M₁} {Y₂ : Set M₂} (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) (hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target) : ↑g.symm.toPartialEquiv '' (Y₂ ∩ g.symm.source) = Y₁ ∩ g.symm.target

The hypothesis on the centres for the inverse partial diffeomorphism.

theorem Manifold.isAdaptedChart_transportChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M₁ : Type u} [TopologicalSpace M₁] [ChartedSpace E M₁] {M₂ : Type u} [TopologicalSpace M₂] [ChartedSpace E M₂] {Y₁ : Set M₁} {Y₂ : Set M₂} {c : ℕ} (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤) (hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target) {φ : OpenPartialHomeomorph M₁ E} {σ : Fin c ↪ Fin n} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂] (hφ : IsAdaptedChart ψ Y₁ φ σ) : IsAdaptedChart ψ Y₂ (transportChart g φ) σ

An adapted chart of Y₁ inside the source of g transports to an adapted chart of Y₂.

The preimage of a closed submanifold under a local analytic isomorphism

theorem Manifold.image_preimage_eq_of_eqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {h : N → M} {Y : Set M} (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N M ⊤) (hΦ : Set.EqOn h (↑Φ.toPartialEquiv) Φ.source) : ↑Φ.toPartialEquiv '' (h ⁻¹' Y ∩ Φ.source) = Y ∩ Φ.target

A partial diffeomorphism Φ : N → M agreeing with h on its source carries h⁻¹(Y) to Y (the hypothesis under which a partial diffeomorphism lifts to the blowings-up).

theorem Manifold.IsClosedSubmanifold.preimage_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] {h : N → M} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h) : IsClosedSubmanifold ψ (h ⁻¹' Y) c

The preimage of a closed submanifold of codimension c under a local analytic isomorphism is a closed submanifold of codimension c: its adapted charts are the adapted charts of Y transported along the local inverses of h (transportChart, isAdaptedChart_transportChart). This is the analytic form of the centres Z_i ×_X Y of the pull-back [Kol07, 30.1].