Density of the complement of the exceptional locus of a finite succession

For a finite succession U_0 ← U_1 ← ⋯ ← U_r of blow-ups with smooth centres C_i ⊆ U_i (FiniteSuccession), the subset of U_0 over which something is blown up is the union Z = ⋃_i σ^i(C_i) of the images of the centres under the composite blow-downs (centerImages). Off Z the composite σ^r : U_r → U_0 is an analytic isomorphism ([Kol07, Theorem 35 (3)]; condition (1) of [BM88, Definition 4.1] iterated). This module proves that the preimage (σ^r)⁻¹(U_0 ∖ Z) is dense in U_r (dense_preimage_compl_centerImages), so that two continuous maps out of U_r which agree over U_0 ∖ Z are equal — the point-set input to the coherence of the identifications of an extension-compatible family (Hironaka.Resolution.Analytic.Wlo09.FamilyCoherence).

• IsBlowUp.dense_compl_preimage_union: for a blowing-up π : M' → M with centre Y and a set A ⊆ M with dense complement, π⁻¹(A ∪ Y) has dense complement in M'. The complement of the exceptional divisor π⁻¹(Y) is dense (IsBlowUp.dense_preimage_compl) and π is a local homeomorphism off it, so the image of an open set meeting M' ∖ π⁻¹(Y) contains a nonempty open set of M, which meets M ∖ A.
• centerImagesLT j, the images ⋃_{k<j} σ^k(C_k) of the first j centres, and injOn_and_dense_stageMapAux: by induction on j, σ^j is injective over the complement of centerImagesLT j and the preimage of that complement is dense in U_j. At the step, a point of U_j over σ^j(C_j) but not over the earlier images lies in C_j (by the injectivity), so (σ^{j+1})⁻¹(centerImagesLT (j+1)) is contained in the preimage under σ_{j+1} of (σ^j)⁻¹(centerImagesLT j) ∪ C_j, and the blow-up step applies.

No surjectivity of the blow-downs is used, so a centre of codimension 0 (for which IsBlowUp forces π⁻¹(Y) = ∅, the blow-down being an isomorphism onto the complement of the centre) needs no separate treatment.

theorem Manifold.IsBlowUp.dense_compl_preimage_union {𝕜 : 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 : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {A : Set M} (hA : Dense Aᶜ) : Dense (π ⁻¹' (A ∪ Y))ᶜ

The blow-up step. For a blowing-up π : M' → M with centre Y and a set A ⊆ M whose complement is dense, the complement of π⁻¹(A ∪ Y) is dense in M': an open set O ⊆ M' meets the dense complement of the exceptional divisor π⁻¹(Y) (IsBlowUp.dense_preimage_compl), on which π is a local homeomorphism (condition (1) of [BM88, Definition 4.1]), so π(O ∖ π⁻¹(Y)) contains a nonempty open set of M, which meets the dense set M ∖ A.

The images of the centres

def AnalyticManifold.FiniteSuccession.centerImagesLT {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (j : ℕ) : Set M.carrier

The images in U_0 of the first j centres under the composite blow-downs, ⋃_{k<j} σ^k(C_k).

Equations

• S.centerImagesLT j = ⋃ (k : Fin S.length), ⋃ (_ : ↑k < j), ⇑(S.stageMap k.castSucc) '' Manifold.IdealSheaf.support (S.center k)

def AnalyticManifold.FiniteSuccession.centerImages {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : Set M.carrier

The images in U_0 of all the centres, Z = ⋃_k σ^k(C_k): the set over which the succession blows up (off it the composite blow-down is an analytic isomorphism, [Kol07, Theorem 35 (3)]).

Equations

• S.centerImages = S.centerImagesLT S.length

theorem AnalyticManifold.FiniteSuccession.centerImagesLT_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : S.centerImagesLT 0 = ∅

theorem AnalyticManifold.FiniteSuccession.centerImagesLT_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {j : ℕ} (hj : j < S.length) : S.centerImagesLT (j + 1) = S.centerImagesLT j ∪ ⇑(S.stageMap ⟨j, hj⟩.castSucc) '' Manifold.IdealSheaf.support (S.center ⟨j, hj⟩)

The images of the first j + 1 centres: those of the first j and the image of C_j.

theorem AnalyticManifold.FiniteSuccession.image_stageMap_center_subset_centerImages {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (k : Fin S.length) : ⇑(S.stageMap k.castSucc) '' Manifold.IdealSheaf.support (S.center k) ⊆ S.centerImages

The image of every centre lies in centerImages.

Density of the preimage of the complement

theorem AnalyticManifold.FiniteSuccession.injOn_and_dense_stageMapAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (j : ℕ) (hj : j < S.length + 1) : Set.InjOn (⇑(S.stageMapAux j hj)) (⇑(S.stageMapAux j hj) ⁻¹' (S.centerImagesLT j)ᶜ) ∧ Dense (⇑(S.stageMapAux j hj) ⁻¹' (S.centerImagesLT j)ᶜ)

Along the partial composites σ^j : U_j → U_0, by induction on j: σ^j is injective over the complement of the images Z_{<j} = ⋃_{k<j} σ^k(C_k) of the earlier centres, and the preimage (σ^j)⁻¹(U_0 ∖ Z_{<j}) is dense in U_j. At the step, a point of U_j over σ^j(C_j) but not over Z_{<j} lies in C_j (by the injectivity), so (σ^{j+1})⁻¹(Z_{<j+1}) is the preimage under σ_{j+1} of (σ^j)⁻¹(Z_{<j}) ∪ C_j, whose complement is dense by the blow-up step (IsBlowUp.dense_compl_preimage_union); the injectivity of σ^{j+1} off it composes that of σ_{j+1} off C_j (condition (1) of [BM88, Definition 4.1]) with that of σ^j off Z_{<j}.

theorem AnalyticManifold.FiniteSuccession.dense_preimage_compl_centerImages {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : Dense (⇑S.composite ⁻¹' S.centerImagesᶜ)

The preimage under the composite blow-down σ^r : U_r → U_0 of the complement of the images of the centres is dense in U_r.