The piece family after a blow-up realises the transformed boundary

The piece family after the blow-up of a centre realises the total transform of the boundary family, that is, the strict transforms of the members in their old order followed by the exceptional divisor π⁻¹(Z) as the last member ([Kol07, Definition 65]), through the label embedding extended by the exceptional member (extendEmb). An old member's strict transform is the union of the strict transforms of its pieces (the strict transform of a finite union is the union of the strict transforms), the exceptional divisor is the union of the new pieces (one per face of the centre, the preimages of the loci), the members off the range are empty, and pieces with the same label stay pairwise disjoint: strict transforms of disjoint pieces lie over disjoint pieces, and the new pieces lie over the disjoint loci of the faces of the centre.

theorem Hironaka.Manifold.strictTransformSet_biUnion {M M' : Type u} [TopologicalSpace M'] (π : M' → M) (Y : Set M) {ι : Type u_1} (s : Finset ι) (H : ι → Set M) : Manifold.strictTransformSet π Y (⋃ i ∈ s, H i) = ⋃ i ∈ s, Manifold.strictTransformSet π Y (H i)

The strict transform of a finite union is the union of the strict transforms.

theorem Hironaka.Manifold.disjoint_strictTransformSet_of_disjoint {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} (hπ : Continuous π) (Y : Set M) {H₁ H₂ : Set M} (h₁ : IsClosed H₁) (h₂ : IsClosed H₂) (hd : Disjoint H₁ H₂) : Disjoint (Manifold.strictTransformSet π Y H₁) (Manifold.strictTransformSet π Y H₂)

Strict transforms of disjoint closed sets are disjoint.

theorem Hironaka.Manifold.BMO.PieceFamily.filter_label_blowUpPieces_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {l : ℕ} (hl : l < Φ.nextLabel) : {c ∈ Finset.range (Φ.blowUpPieces S m hZ).nextComp | (Φ.blowUpPieces S m hZ).label c = l} = {c ∈ Finset.range Φ.nextComp | Φ.label c = l}

The pieces of the transported family with an old label are the old pieces with that label.

theorem Hironaka.Manifold.BMO.PieceFamily.mem_filter_label_blowUpPieces_nextLabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} : c ∈ {c ∈ Finset.range (Φ.blowUpPieces S m hZ).nextComp | (Φ.blowUpPieces S m hZ).label c = Φ.nextLabel} ↔ Φ.nextComp ≤ c ∧ c < Φ.nextComp + S.card

The pieces with the new label are exactly the new pieces.

theorem Hironaka.Manifold.BMO.PieceFamily.biUnion_piece_blowUpPieces_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) : ⋃ c ∈ {c ∈ Finset.range (Φ.blowUpPieces S m hZ).nextComp | (Φ.blowUpPieces S m hZ).label c = Φ.nextLabel}, (Φ.blowUpPieces S m hZ).piece c = ⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' Φ.centerOf S

The union of the new pieces is the exceptional divisor.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.realizes_blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) : (Φ.blowUpPieces S m hZ).Realizes (Manifold.HypersurfaceFamily.totalTransform (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) F) (extendEmb e)

The family after the blow-up of a centre realises the total transform of the boundary family through the extended label embedding ([Kol07, Definition 65]: the strict transforms of the members in the old order, the exceptional divisor last).