Strong resolutions from the isomorphism over the simple locus

A morphism π : R → X of analytic spaces with R non-singular, π proper, π an isomorphism over the simple locus of X and π⁻¹(Sing X) the support of a simple normal crossing divisor is a strong resolution (Hom.IsStrongResolution): the one field not listed, the bimeromorphy of π onto its image, is the density of π⁻¹(Reg X), the complement of the support of a simple normal crossing divisor (ClosedSubspace.isSncDivisorSet_of_isSncBoundary, IsSncDivisorSet.dense_compl). The lemma Hom.isStrongResolution_of_isIsoOver_regularLocus serves the assembly of the resolution of analytic spaces (ResolutionAssembly.lean).

theorem AnalyticSpace.Hom.isStrongResolution_of_isIsoOver_regularLocus {K : Type} [RCLike K] {X R : AnalyticSpace K} {π : R ⟶ X} (hR : R.IsNonsingular) (hπ : IsProperMap ↑π) (hiso : IsIsoOver π X.regularLocus) (hsnc : ∃ (E : R.ClosedSubspace), E.IsSncBoundary ∧ Manifold.IdealSheaf.support E = ↑π ⁻¹' X.singularLocus) : IsStrongResolution π

A morphism with the other fields of a strong resolution is bimeromorphic onto its image, hence a strong resolution: the preimage of the simple locus, over which π is an isomorphism, is the complement of the support of a simple normal crossing divisor of R, hence dense (ClosedSubspace.isSncDivisorSet_of_isSncBoundary, IsSncDivisorSet.dense_compl).