The coordinate swap between two charts at a point

For two charts e, e' of the maximal atlas centred at p, the coordinate swap φ_p = e'⁻¹ ∘ e is the chart change of Hironaka/Manifold/Chart/Atlas.lean (PartialDiffeomorph.chartChange), an analytic isomorphism from U(p) = e.source ∩ e⁻¹(e'.target) onto V(p) = e'.source ∩ e'⁻¹(e.target) — two neighbourhoods of p, in general distinct — with e' ∘ φ_p = e (IsCoordinateSwap). It fixes p, pulls the coordinate functions of e' back to those of e (Kollár's φ^*(x'_1, x_2, …, x_n) = (x_1, x_2, …, x_n) [Kol07, 95]), induces the pullback of germs φ_p^* : 𝒪_{M,p} →+* 𝒪_{M,p} — the stalk map germMapOn of an analytic map fixing p — and satisfies the Taylor identity T_e ∘ φ_p^* = T_{e'}: the e-expansion of g ∘ φ_p is the e'-expansion of g, because (g ∘ φ_p) ∘ e⁻¹ = g ∘ e'⁻¹ near 0 = e p = e' p, so T_e ∘ φ_p^* satisfies the specification IsTaylorHom of the Taylor homomorphism of the chart e' and equals it by uniqueness (IsTaylorHom.eq). Kollár's formal automorphism φ^* of 𝒪̂_{M,p} ≅ 𝕜[[x]] [Kol07, 95] is T_{e'} ∘ T_e⁻¹, the composite of the two completion isomorphisms taylorCompletionEquiv; with the Taylor identity this reads T_e ∘ φ_p^* = φ^* ∘ T_e. Włodarczyk's coordinate change φ_{uv} between two tangent directions is the same construction [Wlo09, Lemma 5.5.3, proof, step (0)]. It is used to compare hypersurfaces of maximal contact given by different charts (Hironaka/Resolution/Analytic/MaximalContact/SwapRealizes.lean).

theorem Manifold.isCoordinateSwap_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) {p : M} (hp : p ∈ e.source) (hp' : p ∈ e'.source) (h0 : ↑e p = 0) (h0' : ↑e' p = 0) : IsCoordinateSwap E M e e' p (PartialDiffeomorph.chartChange he he')

The chart change of two charts centred at p is their coordinate swap in the sense of the specification IsCoordinateSwap.

theorem Manifold.exists_isCoordinateSwap' {𝕜 : 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) {p : M} (hp : p ∈ e.source) (hp' : p ∈ e'.source) (h0 : ↑e p = 0) (h0' : ↑e' p = 0) : ∃ (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤), IsCoordinateSwap E M e e' p Φ

For two charts of the maximal atlas centred at p, the coordinate swap φ_p = e'⁻¹ ∘ e exists as an analytic isomorphism between two neighbourhoods of p.

theorem Manifold.IsCoordinateSwap.apply_mem_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} {p : M} {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤} (h : IsCoordinateSwap E M e e' p Φ) {x : M} (hx : x ∈ Φ.source) : ↑Φ.toPartialEquiv x ∈ e'.source

The coordinate swap maps its source into the source of e'.

theorem Manifold.IsCoordinateSwap.apply_self' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} {p : M} {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤} (h : IsCoordinateSwap E M e e' p Φ) (hp' : p ∈ e'.source) (h0 : ↑e p = 0) (h0' : ↑e' p = 0) : ↑Φ.toPartialEquiv p = p

The coordinate swap of two charts centred at p fixes p.

theorem Manifold.IsCoordinateSwap.mem_target' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} {p : M} {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤} (h : IsCoordinateSwap E M e e' p Φ) (hp' : p ∈ e'.source) (h0 : ↑e p = 0) (h0' : ↑e' p = 0) : p ∈ Φ.target

V(p) = Φ.target is a neighbourhood of p.

theorem Manifold.IsCoordinateSwap.comp_eq' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {e e' : OpenPartialHomeomorph M E} {p : M} {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤} (h : IsCoordinateSwap E M e e' p Φ) {z z' : Fin n → M → 𝕜} (hz : ∀ x ∈ e.source, ∀ (j : Fin n), z j x = ψ (↑e x) j) (hz' : ∀ x ∈ e'.source, ∀ (j : Fin n), z' j x = ψ (↑e' x) j) {x : M} (hx : x ∈ Φ.source) (j : Fin n) : z' j (↑Φ.toPartialEquiv x) = z j x

The coordinate functions of e' pull back along the swap to those of e (Kollár's φ^*(x'_1, x_2, …, x_n) = (x_1, x_2, …, x_n), [Kol07, 95]).

theorem Manifold.IsCoordinateSwap.exists_isPullbackStalk' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e e' : OpenPartialHomeomorph M E} {p : M} {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤} (h : IsCoordinateSwap E M e e' p Φ) (hp' : p ∈ e'.source) (h0 : ↑e p = 0) (h0' : ↑e' p = 0) : ∃ (r : ↑((structureSheaf 𝕜 E M).presheaf.stalk p) →+* ↑((structureSheaf 𝕜 E M).presheaf.stalk p)), IsPullbackStalk E M (↑Φ.toPartialEquiv) r

The pullback of germs along the coordinate swap: the stalk map of an analytic map (germMapOn) for φ_p, which fixes p.

theorem Manifold.IsPullbackStalk.unique' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {p : M} {Φ : M → M} {r r' : ↑((structureSheaf 𝕜 E M).presheaf.stalk p) →+* ↑((structureSheaf 𝕜 E M).presheaf.stalk p)} (hr : IsPullbackStalk E M Φ r) (hr' : IsPullbackStalk E M Φ r') : r = r'

The pullback of germs is determined by its specification (stalkToGerm is injective).

theorem Manifold.IsPullbackStalk.taylorHom_eq' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {e e' : OpenPartialHomeomorph M E} {p : M} {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M M ⊤} (hΦ : IsCoordinateSwap E M e e' p Φ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hp : p ∈ e.source) (hp' : p ∈ e'.source) (h0 : ↑e p = 0) (h0' : ↑e' p = 0) {r : ↑((structureSheaf 𝕜 E M).presheaf.stalk p) →+* ↑((structureSheaf 𝕜 E M).presheaf.stalk p)} (hr : IsPullbackStalk E M (↑Φ.toPartialEquiv) r) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk p)) : (taylorHom E ψ e hp he) (r s) = (taylorHom E ψ e' hp' he') s

T_e ∘ φ_p^* = T_{e'}, the primitive form of Kollár's T_p ∘ φ_p^* = φ^* ∘ T_p [Kol07, 95]: the e-expansion of g ∘ φ_p is the e'-expansion of g, both at 0 = e p = e' p.

theorem Manifold.exists_taylor_automorphism' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {e e' : OpenPartialHomeomorph M E} {p : M} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hp : p ∈ e.source) (hp' : p ∈ e'.source) : ∃ (Φ : MvPowerSeries (Fin n) 𝕜 ≃+* MvPowerSeries (Fin n) 𝕜), ∀ (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk p)), Φ ((taylorHom E ψ e hp he) s) = (taylorHom E ψ e' hp' he') s

Kollár's formal automorphism φ of 𝒪̂_p ≅ 𝕜[[x]] [Kol07, 95]: the composite T_{e'} ∘ T_e⁻¹ of the two completion isomorphisms carries the e-expansion of every germ to its e'-expansion.