Adapted charts off the centre and their coordinate changes

Two inputs of the gluing of the blowing-up of a manifold along a closed submanifold Y [BM88, Definition 4.1]:

• the maximal atlas is stable under composition with an element of the structure groupoid of the model, and an analytic automorphism of E (a translation, say) is such an element; hence every point off the centre Y has a chart adapted to Y (IsAdaptedChart): a chart inside M ∖ Y, shrunk so that one block coordinate varies by less than 1, then translated so that this coordinate is nonzero, which makes both sides of the adaptedness condition false on its source;
• the coordinate change between two charts φ, φ' of the maximal atlas, read in 𝕜ⁿ through ψ (chartChange ψ φ φ' = ψ ∘ φ' ∘ φ⁻¹ ∘ ψ⁻¹ on chartChangeDom ψ φ φ'), is an analytic bijection between open subsets of 𝕜ⁿ satisfying the inverse and cocycle laws; between two adapted charts it carries the centre {x_σ = 0} onto the centre {x_σ' = 0}. These are the hypotheses of the lifting lemma of Hironaka.Manifold.BlowUp.Lift.

The blown-up manifold is glued from the blow-up charts over these adapted charts in Hironaka.Manifold.BlowUp.Glue. None of this is stated in the source; the arguments are routine.

The maximal atlas and the groupoid of the model

theorem Manifold.mem_maximalAtlas_trans_of_mem_groupoid {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M G) {f : OpenPartialHomeomorph H H} (hf : f ∈ G) : e.trans f ∈ StructureGroupoid.maximalAtlas M G

The maximal atlas is stable under composition with an element of the groupoid.

theorem Manifold.addRight_mem_contDiffGroupoid {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (t : E) : (Homeomorph.addRight t).toOpenPartialHomeomorph ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)

The translation x ↦ x + t of the model is an element of the analytic groupoid.

Adapted charts at the points off the centre

theorem Manifold.exists_isAdaptedChart_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (σ : Fin c ↪ Fin n) (i₀ : Fin c) {a : M} (ha : a ∉ Y) : ∃ (φ : OpenPartialHomeomorph M E), a ∈ φ.source ∧ IsAdaptedChart ψ Y φ σ

Every point off the centre has a chart adapted to Y for any block σ: a chart inside M ∖ Y, shrunk so that the block coordinate σ i₀ varies by less than 1, then translated so that this coordinate is nonzero, which makes both sides of the adaptedness condition fail on the source.

Coordinate changes read in Kⁿ

def Manifold.chartChangeDom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] (φ φ' : OpenPartialHomeomorph M E) : Set (Fin n → 𝕜)

The domain in Kⁿ of the coordinate change from the chart φ to the chart φ': ψ(φ(φ.source ∩ φ'.source)).

Equations

• Manifold.chartChangeDom ψ φ φ' = ⇑ψ '' (φ.target ∩ ↑φ.symm ⁻¹' φ'.source)

def Manifold.chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] (φ φ' : OpenPartialHomeomorph M E) (x : Fin n → 𝕜) : Fin n → 𝕜

The coordinate change ψ ∘ φ' ∘ φ⁻¹ ∘ ψ⁻¹ from the chart φ to the chart φ'.

Equations

• Manifold.chartChange ψ φ φ' x = ψ (↑φ' (↑φ.symm (ψ.symm x)))

theorem Manifold.isOpen_chartChangeDom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} : IsOpen (chartChangeDom ψ φ φ')

The chart-change domain is open (the image under ψ of an open subset of φ.target).

theorem Manifold.mem_chartChangeDom_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} {x : Fin n → 𝕜} : x ∈ chartChangeDom ψ φ φ' ↔ ψ.symm x ∈ φ.target ∧ ↑φ.symm (ψ.symm x) ∈ φ'.source

Membership in the chart-change domain, unfolded.

theorem Manifold.mem_chartChangeDom_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} {y : M} (hy : y ∈ φ.source) (hy' : y ∈ φ'.source) : ψ (↑φ y) ∈ chartChangeDom ψ φ φ'

A point of both chart sources has its φ-coordinates in the chart-change domain.

theorem Manifold.chartChangeDom_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} : chartChangeDom ψ φ φ' ⊆ ⇑ψ '' φ.target

The chart-change domain lies in the coordinate image of φ.target.

theorem Manifold.chartChange_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} {x : Fin n → 𝕜} (hx : x ∈ chartChangeDom ψ φ φ') : chartChange ψ φ φ' x ∈ chartChangeDom ψ φ' φ

The chart change maps its domain into the domain of the reverse change.

theorem Manifold.chartChange_chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} {x : Fin n → 𝕜} (hx : x ∈ chartChangeDom ψ φ φ') : chartChange ψ φ' φ (chartChange ψ φ φ' x) = x

The reverse chart change inverts the chart change on its domain.

theorem Manifold.bijOn_chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} : Set.BijOn (chartChange ψ φ φ') (chartChangeDom ψ φ φ') (chartChangeDom ψ φ' φ)

The chart change is a bijection from its domain onto the domain of the reverse change.

theorem Manifold.chartChange_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ : OpenPartialHomeomorph M E} {x : Fin n → 𝕜} (hx : x ∈ chartChangeDom ψ φ φ) : chartChange ψ φ φ x = x

The chart change of a chart with itself is the identity on its domain.

theorem Manifold.chartChange_mem_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' φ'' : OpenPartialHomeomorph M E} {x : Fin n → 𝕜} (hx : x ∈ chartChangeDom ψ φ φ') (hx' : x ∈ chartChangeDom ψ φ φ'') : chartChange ψ φ φ' x ∈ chartChangeDom ψ φ' φ''

Composable chart changes: chartChange φ φ' x lies in the domain of the change φ' → φ'' when x lies in the domains of the changes φ → φ' and φ → φ''.

theorem Manifold.chartChange_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' φ'' : OpenPartialHomeomorph M E} {x : Fin n → 𝕜} (hx : x ∈ chartChangeDom ψ φ φ') : chartChange ψ φ' φ'' (chartChange ψ φ φ' x) = chartChange ψ φ φ'' x

The cocycle law of the coordinate changes.

theorem Manifold.analyticOnNhd_chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} [ChartedSpace E M] (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hφ' : φ' ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : AnalyticOnNhd 𝕜 (chartChange ψ φ φ') (chartChangeDom ψ φ φ')

The coordinate change between two charts of the maximal atlas is analytic.

theorem Manifold.mem_center_iff_chartChange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] {φ φ' : OpenPartialHomeomorph M E} [ChartedSpace E M] {Y : Set M} {c : ℕ} {σ σ' : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) (hφ' : IsAdaptedChart ψ Y φ' σ') {x : Fin n → 𝕜} (hx : x ∈ chartChangeDom ψ φ φ') : x ∈ blowUpCenter σ ↔ chartChange ψ φ φ' x ∈ blowUpCenter σ'

Between two adapted charts the coordinate change carries the centre {x_σ = 0} onto the centre {x_σ' = 0}: both are the coordinate image of Y.