The resolution of a triple as one family over the manifold

CompatibleFamily.toExtensionCompatibleFamily C is the extension-compatible family of a compatible family C along the exhaustion of M by relatively compact opens (ExtensionCompatibleFamily.ofCompatibleFamily), and its blow-down is proper (CompatibleFamily.isProperMap_toExtensionCompatibleFamily_map). It is the gluing both of the resolution of a triple below and of the embedded desingularization (Hironaka/Resolution/Analytic/Wlo09/EmbeddedDesingularization.lean).

resolveFamExt bo T is the extension-compatible family of the resolution resolveFam bo T (Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean) along the exhaustion of M by relatively compact opens (ExtensionCompatibleFamily.ofCompatibleFamily; Włodarczyk's compatible family of resolutions [Wlo09, Theorem 2.0.3 (4)], Kollár's passage from neighbourhoods of compacts to the whole space [Kol07, 44]). Its map is the glued blow-down σ:

• isProperMap_resolveFamExt_map — σ is proper (Hironaka's canonical modification is a proper morphism [Hir64, p. 155]; [Wlo09, Theorem 2.0.3]; the gluing of the local principalizations [Wlo09, §4.1]), one application of CompatibleFamily.isProperMap_limitBlowDown;
• isAnalyticIsoOver_resolveFamExt_map — σ is an analytic isomorphism off the cosupport of the ideal sheaf ([Kol07, Theorem 35 (3)]; [Wlo09, Lemma 4.0.3]), one application of CompatibleFamily.isAnalyticIsoOver_limitBlowDown.

noncomputable def Hironaka.Manifold.CompatibleFamily.toExtensionCompatibleFamily {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) : M.ExtensionCompatibleFamily

A compatible family of blow-up sequences as one family over the manifold: the extension-compatible family of C along the exhaustion of M (ExtensionCompatibleFamily.ofCompatibleFamily; Włodarczyk's gluing of the local principalizations and desingularizations [Wlo09, §4.1 and §4.2]).

Equations

• C.toExtensionCompatibleFamily = AnalyticManifold.ExtensionCompatibleFamily.ofCompatibleFamily C (Hironaka.Manifold.exhaustion M) ⋯ ⋯ ⋯ ⋯

theorem Hironaka.Manifold.CompatibleFamily.isProperMap_toExtensionCompatibleFamily_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) : IsProperMap ⇑C.toExtensionCompatibleFamily.map

The glued blow-down of a compatible family is proper (CompatibleFamily.isProperMap_limitBlowDown).

noncomputable def Hironaka.Manifold.resolveFamExt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : M.ExtensionCompatibleFamily

The resolution of T as one family over M: the extension-compatible family of resolveFam bo T along the exhaustion of M (ExtensionCompatibleFamily.ofCompatibleFamily), Włodarczyk's compatible family of resolutions of the relatively compact opens [Wlo09, Theorem 2.0.3 (4)] (CompatibleFamily.toExtensionCompatibleFamily). Its map is the glued blow-down σ.

Equations

• Hironaka.Manifold.resolveFamExt bo T = (Hironaka.Manifold.resolveFam bo T).toExtensionCompatibleFamily

theorem Hironaka.Manifold.isProperMap_resolveFamExt_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : IsProperMap ⇑(resolveFamExt bo T).map

σ is proper (Hironaka's canonical modification is a proper morphism [Hir64, p. 155]; [Wlo09, Theorem 2.0.3]; [Wlo09, §4.1]): one application of the gluing tool CompatibleFamily.isProperMap_limitBlowDown (CompatibleFamily.isProperMap_toExtensionCompatibleFamily_map).

theorem Hironaka.Manifold.isAnalyticIsoOver_resolveFamExt_map {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : (resolveFamExt bo T).map.IsIsoOver (Manifold.IdealSheaf.support T.I)ᶜ

σ is an analytic isomorphism off the cosupport of 𝓘 ([Kol07, Theorem 35 (3)]; [Wlo09, Lemma 4.0.3]): one application of CompatibleFamily.isAnalyticIsoOver_limitBlowDown fed per piece by isAnalyticIsoOver_stageMap_last_resolveSeqOn.