The glued space is Hausdorff and second countable, and the blow-down is proper

A blowing-up M' is required to be an analytic manifold, here Hausdorff and second countable, and π to be proper [BM88, Definition 4.1]. For the glued space:

• Hausdorff: two points over distinct points of M are separated by the preimages of separating open sets; two points over the same point a lie in pieces over one adapted chart at a; in the same piece they are separated inside it, and in the pieces i ≠ k with neither point in the other's chart, the open sets {|u_k| < 1} and {|u'_i| < 1} are disjoint since the transition T_ik has u'_i = 1/u_k;
• second countable: countably many adapted charts cover M (second countable), and the images of countable bases of the corresponding pieces form a countable basis of the glued space;
• proper: the preimage of a compact set is covered by finitely many compact boxes {π_k u ∈ closedBall, |u_l| ≤ 1 (l ≠ k)} (the boxes are compact, and every point of a piece is carried into a box by some T_ik, Hironaka.Manifold.BlowUp.Transition), and it is closed.

These are the remaining clauses showing that the glued space is a blowing-up (Hironaka.Manifold.BlowUp.Exists). The arguments are not in the source.

theorem Manifold.BlowUpGlue.exists_disjoint_open_of_ne_same_piece {𝕜 : 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) {u u' : ↑(pieceSet j)} (h : u ≠ u') : ∃ (U : Set (Glued ψ Y c)) (V : Set (Glued ψ Y c)), IsOpen U ∧ IsOpen V ∧ toGlued j u ∈ U ∧ toGlued j u' ∈ V ∧ Disjoint U V

Two distinct points of a piece are separated in the glued space.

theorem Manifold.BlowUpGlue.exists_disjoint_open_same_chart {𝕜 : 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 : ℕ} (s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c)) (k k' : Fin c) (w : ↑(pieceSet (s, k))) (w' : ↑(pieceSet (s, k'))) (hne : toGlued (s, k) w ≠ toGlued (s, k') w') : ∃ (U : Set (Glued ψ Y c)) (V : Set (Glued ψ Y c)), IsOpen U ∧ IsOpen V ∧ toGlued (s, k) w ∈ U ∧ toGlued (s, k') w' ∈ V ∧ Disjoint U V

Two distinct points of the glued space in pieces over one chart are separated.

noncomputable def Manifold.BlowUpGlue.chartIdxAt {𝕜 : 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) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) (a : M) : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c)

A chart (shrunk index) at each point of M.

Equations

• Manifold.BlowUpGlue.chartIdxAt hY σ₀ i₀ a = ⋯.choose

theorem Manifold.BlowUpGlue.mem_source_chartIdxAt {𝕜 : 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) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) (a : M) : a ∈ (pieceChart (chartIdxAt hY σ₀ i₀ a, i₀)).source

The chosen adapted chart at a contains a in its source.

theorem Manifold.BlowUpGlue.t2Space_glued {𝕜 : 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) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) [T2Space M] : T2Space (Glued ψ Y c)

The glued space is Hausdorff.

theorem Manifold.BlowUpGlue.secondCountableTopology_glued {𝕜 : 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) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) [SecondCountableTopology M] : SecondCountableTopology (Glued ψ Y c)

The glued space is second countable.

theorem Manifold.BlowUpGlue.isProperMap_gluedProj {𝕜 : 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) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) [T2Space M] : IsProperMap gluedProj

The blow-down is proper, as [BM88, Definition 4.1] requires.