The glued space as an analytic manifold

The inclusion toGlued j of a piece into the glued space Glued ψ Y c is an open embedding; its inverse, read through ψ⁻¹, is a chart gluedChart j of the glued space with source the image of the piece and target ψ⁻¹(S_j). These charts, one for each nonempty piece, form an atlas (ChartedSpace E (Glued ψ Y c)), and the chart changes are the transition maps of Hironaka.Manifold.BlowUp.Glue read through ψ, which are analytic; so the glued space is an analytic manifold (IsManifold 𝓘(𝕜, E) ω) and every glued chart lies in its maximal atlas.

This gives the blowing-up of M with centre Y [BM88, Definition 4.1] its structure of analytic manifold. The analyticity of the blow-down is proved in Hironaka.Manifold.BlowUp.GluedBlowDown and its properness in Hironaka.Manifold.BlowUp.GluedTopology.

The charts of the glued space

noncomputable def Manifold.BlowUpGlue.pieceEmbChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : OpenPartialHomeomorph (↑(pieceSet j)) (Glued ψ Y c)

The inclusion of a (nonempty) piece as an open partial homeomorphism.

Equations

• Manifold.BlowUpGlue.pieceEmbChart j hj = Topology.IsOpenEmbedding.toOpenPartialHomeomorph (Manifold.BlowUpGlue.toGlued j) ⋯

theorem Manifold.BlowUpGlue.pieceEmbChart_symm_toGlued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) (u : ↑(pieceSet j)) : ↑(pieceEmbChart j hj).symm (toGlued j u) = u

The inverse of the embedding chart of a piece undoes the inclusion.

theorem Manifold.BlowUpGlue.pieceEmbChart_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : (pieceEmbChart j hj).target = Set.range (toGlued j)

The target of the embedding chart of a piece is the image of the inclusion.

noncomputable def Manifold.BlowUpGlue.gluedChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : OpenPartialHomeomorph (Glued ψ Y c) E

The chart of the glued space over a nonempty piece: the inverse of the inclusion of the piece, followed by ψ⁻¹; source the image of the piece, target ψ⁻¹(S_j).

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.BlowUpGlue.gluedChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : (gluedChart j hj).source = Set.range (toGlued j)

The source of a glued chart is the image of its piece.

theorem Manifold.BlowUpGlue.gluedChart_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : (gluedChart j hj).target = ⇑ψ ⁻¹' pieceSet j

The target of a glued chart is the piece set read in E.

theorem Manifold.BlowUpGlue.gluedChart_toGlued {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) (u : ↑(pieceSet j)) : ↑(gluedChart j hj) (toGlued j u) = ψ.symm ↑u

A glued chart reads the coordinates of a point of its piece.

theorem Manifold.BlowUpGlue.gluedChart_symm_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) {v : E} (hv : ψ v ∈ pieceSet j) : ↑(gluedChart j hj).symm v = toGlued j ⟨ψ v, hv⟩

The inverse of a glued chart is the inclusion of the piece.

theorem Manifold.BlowUpGlue.toGlued_mem_gluedChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) (u : ↑(pieceSet j)) : toGlued j u ∈ (gluedChart j hj).source

Points of a piece lie in the source of its glued chart.

The charted space and manifold structure

theorem Manifold.BlowUpGlue.pieceSet_pieceOf_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (p : Glued ψ Y c) : (pieceSet (pieceOf p)).Nonempty

@[instance_reducible]

noncomputable instance Manifold.BlowUpGlue.gluedChartedSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} : ChartedSpace E (Glued ψ Y c)

The charted-space structure of the glued space: the glued charts of the nonempty pieces (a piece with empty coordinate set has no chart).

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.BlowUpGlue.mem_atlas_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {Φ : OpenPartialHomeomorph (Glued ψ Y c) E} : Φ ∈ atlas E (Glued ψ Y c) ↔ ∃ (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty), Φ = gluedChart j hj

The atlas of the glued space consists of the glued charts of the nonempty pieces.

theorem Manifold.BlowUpGlue.gluedChart_mem_atlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : gluedChart j hj ∈ atlas E (Glued ψ Y c)

Each glued chart of a nonempty piece lies in the atlas.

theorem Manifold.BlowUpGlue.gluedChart_transition {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {j j' : PieceIdx ψ Y c} (hj : (pieceSet j).Nonempty) (hj' : (pieceSet j').Nonempty) {v : E} (hv : v ∈ (gluedChart j hj).target ∩ ↑(gluedChart j hj).symm ⁻¹' (gluedChart j' hj').source) : ψ v ∈ transDom j j' ∧ ↑(gluedChart j' hj') (↑(gluedChart j hj).symm v) = ψ.symm (transMap j j' (ψ v))

The chart change between the charts of two pieces is the transition map read through ψ.

instance Manifold.BlowUpGlue.gluedIsManifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ (Glued ψ Y c)

The glued space is an analytic manifold: its chart changes are the transition maps, analytic on their open domains.

theorem Manifold.BlowUpGlue.gluedChart_mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : gluedChart j hj ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ (Glued ψ Y c)

Every chart of a piece lies in the maximal atlas.