The padded reading opens

Kollár's proof of Theorem 36 embeds X ⊂ ℂⁿ ⊂ ℂᴺ and passes to the ideal (𝓘, z_{n+1}, …, z_N) [Kol07, Theorem 36, proof]; Włodarczyk's resolution of a marked ideal commutes with closed embeddings of the ambient manifold [Wlo09, §7.1]. The padding identity of the local resolutions (the value of the functor on the padded triple against its value on the original one) is read on relatively compact opens, and the padded model must be read on an open W⁺ of the padded ambient padOpens σ G whose trace on the coordinate slice — the image of the zero extension padExt σ G : Sp(G) → Sp(padOpens σ G) — is the given reading open W of Sp(G). The choice made here is the product of W with the open unit ball in the padding coordinates:

• padReadingOpens σ G W := padCoordProj σ G ⁻¹' W ∩ {z_k ∈ 𝔻 for k ∉ range σ}, with mem_padReadingOpens;
• preimageOpens_padExt_padReadingOpens: the zero extension reads it back as W (padCoordProj ∘ padExt = id, the padding coordinates of padExt w are 0);
• isCompact_closure_padReadingOpens: relatively compact when W is — its closure lies in the preimage under the coordinate chart pieceCoord of the closed bounded box {z | z ∘ σ ∈ pieceCoord '' closure W, ‖z_k‖ ≤ 1 off range σ} of 𝕜ⁿ', compact by Heine–Borel and inside padOpens σ G, and pieceCoord is an open embedding;
• exists_padOpens_preimage_eq: the existence statement — a relatively compact open of the padded ambient reading back as W.

Not in the sources; bookkeeping.

The open unit ball in the padding coordinates

def Hironaka.Manifold.padBall {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Set (pieceAmbient 𝕜 (padOpens σ G)).carrier

The open unit ball in the padding coordinates — the points of the padded ambient whose coordinates off range σ have norm below 1.

Equations

• Hironaka.Manifold.padBall σ G = {p : (Hironaka.Manifold.pieceAmbient 𝕜 (Hironaka.Manifold.padOpens σ G)).carrier | ∀ k ∉ Set.range ⇑σ, ‖↑p.snd k‖ < 1}

theorem Hironaka.Manifold.mem_padBall {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) {p : (pieceAmbient 𝕜 (padOpens σ G)).carrier} : p ∈ padBall σ G ↔ ∀ k ∉ Set.range ⇑σ, ‖↑p.snd k‖ < 1

Membership in the padding ball, unfolded.

theorem Hironaka.Manifold.isOpen_padBall {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : IsOpen (padBall σ G)

The ball in the padding coordinates is open — a finite intersection of the open conditions ‖z_k‖ < 1.

theorem Hironaka.Manifold.padExt_mem_padBall {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : padExt σ G w ∈ padBall σ G

The zero extension lands in the ball — its padding coordinates are 0.

The padded reading open

def Hironaka.Manifold.padReadingOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens σ G)).carrier

The padded reading open of a reading open W ⊆ Sp(G) — the product of W with the open unit ball in the padding coordinates, p⁻¹(W) ∩ {‖z_k‖ < 1, k ∉ range σ}, an open of the padded ambient of [Kol07, Theorem 36, proof].

Equations

• Hironaka.Manifold.padReadingOpens σ G W = { carrier := Hironaka.Manifold.padCoordProj σ G ⁻¹' ↑W ∩ Hironaka.Manifold.padBall σ G, is_open' := ⋯ }

theorem Hironaka.Manifold.mem_padReadingOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) {W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier} {p : (pieceAmbient 𝕜 (padOpens σ G)).carrier} : p ∈ padReadingOpens σ G W ↔ padCoordProj σ G p ∈ W ∧ ∀ k ∉ Set.range ⇑σ, ‖↑p.snd k‖ < 1

Membership in the padded reading open — the coordinate projection lies in W and the padding coordinates have norm below 1.

theorem Hironaka.Manifold.preimageOpens_padExt_padReadingOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) : Manifold.preimageOpens (padExt σ G) ⋯ (padReadingOpens σ G W) = W

The zero extension reads the padded reading open back as W — p ∘ s = id (padCoordProj_padExt) and the padding coordinates of s w vanish (padExt_apply_of_notMem_range).

theorem Hironaka.Manifold.isCompact_closure_padReadingOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) (hW : IsCompact (closure ↑W)) : IsCompact (closure ↑(padReadingOpens σ G W))

The padded reading open of a relatively compact open is relatively compact — its closure lies in the preimage under the coordinate chart pieceCoord of the closed bounded box {z | z ∘ σ ∈ K, ‖z_k‖ ≤ 1 off range σ} (K := pieceCoord '' closure W, compact and inside G), a compact set of 𝕜ⁿ' inside padOpens σ G (Heine–Borel), and pieceCoord is an open embedding.

theorem Hironaka.Manifold.exists_padOpens_preimage_eq {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 G).carrier) (hW : IsCompact (closure ↑W)) : ∃ (Wp : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens σ G)).carrier), IsCompact (closure ↑Wp) ∧ Manifold.preimageOpens (padExt σ G) ⋯ Wp = W

The padded reading open exists — for a relatively compact reading open W of Sp(G) there is a relatively compact open W⁺ of the padded ambient Sp(padOpens σ G) whose preimage under the zero extension is W (the witness is padReadingOpens σ G W).