Włodarczyk's divisor E and strict transform Ỹ for the embedded desingularization

The global objects of [Wlo09, Theorem 2.0.2] for the embedded desingularization of a reduced closed subspace Y on the standard model (embeddedDesingFam, Hironaka/Resolution/Analytic/Wlo09/EmbeddedDesingModel.lean): the exceptional divisor embeddedDesingExceptional and the strict transform embeddedDesingStrictTransform on the glued space M̃, the glued objects of Hironaka/Resolution/Analytic/Wlo09/GlobalObjects.lean for the pieces embeddedDesingPieces of the family. The per-piece hypotheses of that module are the clauses of the concrete functor on the pieces (concreteBEDanFamStar_isEmbeddedDesing), the identification of the boundaries with the reduced ideal sheaves of the exceptional families (boundarySeq_seqOn_embeddedDesingPiecesOfNonzero), the desingularization clauses for 𝓘_Y (isDesingularizedBy_seqOn_embeddedDesingPieces) and the transversal chart and monomial clauses with the last exceptional family named (exists_adaptedChart_seqOn_embeddedDesingPieces, exists_monomial_seqOn_embeddedDesingPieces):

• isGloballyDesingularizedBy_embeddedDesingFam: E and Ỹ are the exceptional divisor and the strict transform of the embedded desingularization of Y by the family (IdealSheaf.IsGloballyDesingularizedBy, defined in Hironaka/Resolution/Analytic/ModelTransport/Family.lean), with the clauses (1), (3), (6) on M̃, restricting over every compact to the last exceptional divisor and the last strict transform;
• isLocallyFinitelyDesingularizedBy_embeddedDesingFam: the family is a locally finite embedded desingularization of Y (IdealSheaf.IsLocallyFinitelyDesingularizedBy).

For any compatible family whose successions desingularize Y over every compact, divisors E and Ỹ on M̃ with the clauses of IsGloballyDesingularizedBy have the remaining properties of [Wlo09, Theorem 2.0.2] on M̃, read on the pieces through toSpace: E is a simple normal crossings divisor (IsGloballyDesingularizedBy.isSncBoundary) with support res_{Y,M}⁻¹(Sing Y) (IsGloballyDesingularizedBy.support_eq), and Ỹ is smooth (IsGloballyDesingularizedBy.isNonsingular).

The divisor and the strict transform on the glued space, from their restrictions

theorem AnalyticManifold.IdealSheaf.IsGloballyDesingularizedBy.isSncBoundary {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {F : M.ExtensionCompatibleFamily} {D Y : F.space.IdealSheaf} (h : I.IsGloballyDesingularizedBy F D Y) : D.IsSncBoundary

E is a simple normal crossings divisor on M̃: the hypersurface family of the transversal clause.

theorem AnalyticManifold.IdealSheaf.IsGloballyDesingularizedBy.support_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {F : M.ExtensionCompatibleFamily} {D Y : F.space.IdealSheaf} (h : I.IsGloballyDesingularizedBy F D Y) (hdes : ∀ (K : TopologicalSpace.Compacts M.carrier), (I.restrict (F.nhd K)).IsDesingularizedBy (F.seq K)) : Manifold.IdealSheaf.support D = ⇑F.map ⁻¹' (Manifold.IdealSheaf.support I \ I.regularLocus)

The support of E is res_{Y,M}⁻¹(Sing Y), the exceptional locus of [Wlo09, Theorem 2.0.2], when the successions desingularize Y over every compact: a point q of M̃ lies in the image of the last stage over the singleton compact of res_{Y,M}(q) (exists_toSpace_eq), where E is E_r (pullback_toSpace_eq_boundarySeq, read along the local analytic isomorphism toSpace, mem_cosupport_comap_iff) and |E_r| = σ_K⁻¹(Sing Y).

theorem AnalyticManifold.IdealSheaf.IsGloballyDesingularizedBy.isNonsingular {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {F : M.ExtensionCompatibleFamily} {D Y : F.space.IdealSheaf} (h : I.IsGloballyDesingularizedBy F D Y) (hdes : ∀ (K : TopologicalSpace.Compacts M.carrier), (I.restrict (F.nhd K)).IsDesingularizedBy (F.seq K)) : Y.IsNonsingular

Ỹ is smooth, when the successions desingularize Y over every compact: at a point q of Ỹ, in the image of the last stage over the singleton compact of res_{Y,M}(q) (exists_toSpace_eq), the local ring of Ỹ is that of the smooth Y_r (pullback_toSpace_eq_strictTransform, isRegularLocalRing_quotient_stalkIdeal_comap_iff).

noncomputable def Hironaka.Manifold.embeddedDesingExceptional {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : (embeddedDesingFam M I hI).space.IdealSheaf

Włodarczyk's exceptional divisor E on M̃ for the embedded desingularization of Y: the reduced ideal sheaf of the exceptional families of the pieces, glued along the exhaustion (CompatibleFamily.gluedExceptionalIdeal).

Equations

• Hironaka.Manifold.embeddedDesingExceptional M I hI = (Hironaka.Manifold.embeddedDesingPieces M I hI).gluedExceptionalIdeal

noncomputable def Hironaka.Manifold.embeddedDesingStrictTransform {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : (embeddedDesingFam M I hI).space.IdealSheaf

Włodarczyk's strict transform Ỹ on M̃ for the embedded desingularization of Y: the saturation of the total transform of 𝓘_Y by the exceptional divisor (CompatibleFamily.globalStrictTransform).

Equations

• Hironaka.Manifold.embeddedDesingStrictTransform M I hI = (Hironaka.Manifold.embeddedDesingPieces M I hI).globalStrictTransform I

theorem Hironaka.Manifold.isGloballyDesingularizedBy_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : I.IsGloballyDesingularizedBy (embeddedDesingFam M I hI) (embeddedDesingExceptional M I hI) (embeddedDesingStrictTransform M I hI)

E and Ỹ are the exceptional divisor and the strict transform of the embedded desingularization of Y (IdealSheaf.IsGloballyDesingularizedBy, [Wlo09, Theorem 2.0.2 (1), (3), (6)]): the clauses of the glued objects (isSncBoundaryTransversalTo_globalStrictTransform, isMulBoundaryMonomial_globalStrictTransform) and their identifications on the pieces (gluedExceptionalIdeal_pullback_toLimitMap, globalStrictTransform_pullback_toLimitMap), from the clauses of the concrete functor on the pieces.

theorem Hironaka.Manifold.isLocallyFinitelyDesingularizedBy_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) : I.IsLocallyFinitelyDesingularizedBy (embeddedDesingFam M I hI)

The family is a locally finite embedded desingularization of Y (IdealSheaf.IsLocallyFinitelyDesingularizedBy): the three clauses per compact, the absence of empty centres, the codimension of the centres (FiniteSuccession.two_le_codim_or_boundarySeq_le_center_iff) and the global objects.