Properness and non-singularity of the resolution R(X) → X

Kollár's Theorem 45: R(X) is smooth and Π_X is projective over any compact subset of X [Kol07, Theorem 45(1), (4)]; Włodarczyk's Theorem 2.0.1: the canonical desingularization is a manifold with a proper bimeromorphic morphism to Y [Wlo09, Theorem 2.0.1], des_V : Ṽ → V proper [Wlo09, §4, (3)⇒(4)] and des : Ỹ → Y proper [Wlo09, §4.3]; the smoothness of the final strict transform is [Wlo09, Theorem 2.0.2(3)]. Two clauses of exists_functorial_resolution (ResolutionAssembly.lean) in the form the assembly uses:

• BEDanFamStar.isProperMap_resolutionMap: Π_X : R(X) → X is proper, with NO hypotheses: off the class (X not reduced) and without a gluing datum the pair is ⟨X, 𝟙 X⟩; with one, over every member U_n of the exhaustion the descended map is the map Π_{U_n}, proper by isProperMap_resolutionOnMap (PieceGlueDatum.lean), and properness is local on the target;
• BEDanFamStar.resolution_isNonsingular_of_independent: R(X) is non-singular — the exhaustion's pieces resolutionOn (D n) bed are open subspaces of the glued spaces Ṽ_n, glued from the local resolutions Ỹ_i, which are non-singular by clause (3) of hbed (isNonsingular_localResolution); a glued space of non-singular pieces is non-singular (isNonsingular_gluedOver, twice).

The independence of the local resolution enters as the hypothesis hind where a gluing datum is needed. Not in the sources beyond the statements cited; bookkeeping.

theorem Hironaka.Manifold.LocalEmbeddingData.range_toFun_resolutionOnToSpace_subset {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hU : IsOpen U) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed)) ⊆ U

The map resolutionOnToSpace into X lands in the OPEN U (openOf X U = U for an open U).

theorem Hironaka.Manifold.LocalEmbeddingData.isProperMap_resolutionOnToSpace_dom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hU : IsOpen U) : IsProperMap fun (y : ↑↑(D.resolutionOn bed).toPresheafedSpace) => ⟨AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed) y, ⋯⟩

The map resolutionOnToSpace onto the OPEN U is proper (Włodarczyk's des_V proper, [Wlo09, §4, (3)⇒(4)]) — isProperMap_resolutionOnMap, its target X|U read as the subtype U (openOf_of_isOpen).

theorem Hironaka.Manifold.LocalEmbeddingData.isNonsingular_resolutionOnFull_of_independent {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : (D.resolutionOnFull bed).IsNonsingular

The glued space of the pieces is non-singular ([Wlo09, Theorem 2.0.2(3)]; [Kol07, Theorem 45(1)]) — every local resolution Ỹ_i is non-singular by clause (3) of hbed (isNonsingular_localResolution), and a glued space of non-singular pieces is non-singular (isNonsingular_gluedOver); the space resolutionOnFull unfolds to the chosen datum's glued space (resolutionOnFull_eq_of_glues).

theorem Hironaka.Manifold.LocalEmbeddingData.isNonsingular_resolutionOn_of_independent {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : (D.resolutionOn bed).IsNonsingular

Non-singularity of the space resolutionOn over U, under hbed and the independence hind: an open subspace of a non-singular space (isNonsingular_restrictSet, isNonsingular_resolutionOnFull_of_independent).

theorem Hironaka.Manifold.BEDanFamStar.isProperMap_resolutionMap {𝕜 : Type} [RCLike 𝕜] (X : AnalyticSpace 𝕜) (bed : BEDanFamStar 𝕜) : IsProperMap ↑(bed.resolutionMap X)

Π_X : R(X) → X is proper ([Kol07, Theorem 45(4)]: projective over every compact subset; [Wlo09, Theorem 2.0.1]: proper; [Wlo09, §4.3]) — with NO hypotheses: off the class and without a gluing datum the pair is ⟨X, 𝟙 X⟩ (resolutionPair_eq_of_not_isReduced, resolutionPair_eq_of_not_glues), the identity being proper; with a gluing datum, over every member U_n of the exhaustion the descended map is the map Π_{U_n}, proper by isProperMap_resolutionOnToSpace_dom, and properness is local on the target (isProperMap_descMap_of_iUnion). Neither the reducedness of X nor IsEmbeddedDesing is needed.

theorem Hironaka.Manifold.BEDanFamStar.resolution_isNonsingular_of_independent {𝕜 : Type} [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : (bed.resolution X).IsNonsingular

R(X) is non-singular ([Wlo09, Theorem 2.0.1]: Ỹ is a manifold; [Kol07, Theorem 45(1)]), for a reduced X, under hbed and with the independence of the local resolution as hind — the exhaustion's pieces resolutionOn (D n) bed are non-singular (isNonsingular_resolutionOn_of_independent) and the glued space of non-singular pieces is non-singular (isNonsingular_gluedOver); the space bed.resolution X unfolds to the chosen datum's glued space (resolution_eq_of_glues).