Documentation

Hironaka.Resolution.Analytic.Kol07Thm45.ResolutionAssembly

Resolution of analytic spaces from an embedded desingularization family #

The assembly of the resolution of analytic spaces. Given a family functor bed : BEDanFamStar K that is an embedded desingularization (hbed : bed.IsEmbeddedDesing, Functor/EmbeddedDesingFam.lean: the exceptional divisors have simple normal crossings, the centres lie over the non-simple points, the final strict transform is smooth and meets the exceptional divisors with simple normal crossings, the total transform of the ideal factors accordingly, and the functor commutes with local isomorphisms; the commutation with closed embeddings is the field closedEmbedding of BEDanFamStar), the local resolutions of the pieces of a reduced analytic space X — a piece is an open X|V embedded as a closed subspace of an open G ⊆ 𝕜ⁿ, resolved by running bed on (G, 𝓘_{X|V}, ∅) (PieceEmbedding.lean) — glue to a resolution Π_X : R(X) → X (Resolution.lean), and the glued space has the properties that the main theorem exists_functorial_resolution asks of a ResolutionAssignment. This is Kollár's construction of the resolution functor from the embedded one — the proof of [Kol07, Theorem 36], carried to analytic spaces by [Kol07, 44] and stated as [Kol07, Theorem 45] — with the gluing over the disjoint union of a cover [Kol07, Proposition 37, proof] and the independence of the embedding [Kol07, Theorem 36, proof]; in Włodarczyk's form, the passage from the canonical embedded desingularization to the canonical resolution of an analytic space [Wlo09, §4, (3)⇒(4)] and its gluing over an exhaustion [Wlo09, §4.3].

The one hypothesis the gluing theorems carry beyond hbed, the independence of the local resolution from the embedding (LocalResolutionIndependentOn X bed), is discharged here by localResolution_independent_local (LocalResolutionShear.lean), Kollár's comparison of two embeddings through the shear of [Kol07, Lemma 39]. The main theorem exists_functorial_resolution instantiates analyticSpace_resolution_of_isEmbeddedDesing at the concrete family concreteBEDanFamStar (Hironaka/Resolution/Analytic/Wlo09/Concrete.lean).

source
theorem Hironaka.analyticSpace_resolution_of_isEmbeddedDesing (K : Type) [RCLike K] (bed : Manifold.BEDanFamStar K) (hbed : Manifold.BEDanFamStar.IsEmbeddedDesing K bed) :
∃ (R : AnalyticSpace.ResolutionAssignment (AnalyticSpace K)), ∀ (X : AnalyticSpace K), X.IsReduced → (R.space X).IsNonsingular ∧ AnalyticSpace.Hom.IsIsoOver (R.map X) X.regularLocus ∧ (∃ (E : (R.space X).ClosedSubspace), E.IsSncBoundary ∧ Manifold.IdealSheaf.support E = ↑(R.map X) ⁻¹' X.singularLocus) ∧ IsProperMap ↑(R.map X) ∧ AnalyticSpace.Hom.IsLocallyFiniteAmbientBlowUpComposite (R.map X) ∧ Set.range ↑(R.map X) = closure X.regularLocus ∧ ∀ (Y : AnalyticSpace K), Y.IsReduced → ∀ (U : Set ↑↑X.toPresheafedSpace) (V : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsOpen V → ∀ (φ : X.restrictSet U ⟶ Y.restrictSet V), CategoryTheory.IsIso φ → ∃! ψ : (R.space X).restrictSet (↑(R.map X) ⁻¹' U) ⟶ (R.space Y).restrictSet (↑(R.map Y) ⁻¹' V), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (AnalyticSpace.Hom.restrictSet (R.map Y) V) = CategoryTheory.CategoryStruct.comp (AnalyticSpace.Hom.restrictSet (R.map X) U) φ

The resolution of analytic spaces from an embedded desingularization family: for any bed with hbed, a ResolutionAssignment X ↦ (Π_X : R(X) → X) satisfying, for every reduced X, the clauses of exists_functorial_resolution (non-singularity, the isomorphism over the simple locus, the simple normal crossings divisor, properness, the ambient blow-up factorization, the image, the unique lifting of isomorphisms); instantiated at concreteBEDanFamStar in the proof of that theorem.

source
theorem AnalyticSpace.exists_functorial_resolution (K : Type) [RCLike K] :
∃ (R : ResolutionAssignment (ReducedSpace K)), (∀ (X : ReducedSpace K), Hom.IsStrongResolutionOntoClosureRegularLocus (R.map X) ∧ Hom.IsLocallyFiniteAmbientBlowUpComposite (R.map X)) ∧ R.LiftsLocalIsomorphisms

Resolution of analytic spaces [Kol07, Theorem 45]; [Wlo09, Theorem 2.0.1], over K = ℝ or K = ℂ. There is a resolution assignment X ↦ (Π_X : R(X) → X) on the reduced K-analytic spaces (ResolutionAssignment (ReducedSpace K)) such that

  • every Π_X is a strong resolution of X onto the closure of its simple locus (Hom.IsStrongResolutionOntoClosureRegularLocus): Π_X is proper and bimeromorphic onto its image, (1) R(X) is non-singular, (2) Π_X is an isomorphism over the simple locus X.regularLocus, (3) Π_X⁻¹(X.singularLocus) is the support of a simple normal crossing divisor of R(X), and the image of Π_X is the closure of X.regularLocus (in neither source; see the relation to the source below);
  • (4) over every relatively compact open subset of X the morphism Π_X is the composite of a finite sequence of blow-ups of smooth centres of an ambient manifold, restricted to strict transforms (Hom.IsLocallyFiniteAmbientBlowUpComposite);
  • (5) R lifts local analytic isomorphisms (ResolutionAssignment.LiftsLocalIsomorphisms): every isomorphism between open subspaces of two inputs lifts to exactly one morphism between their preimages in the resolutions over it, an isomorphism; and every local analytic isomorphism φ : X' → X between inputs (Hom.IsLocalIso: locally an isomorphism onto an open subspace, injective or not) lifts to exactly one morphism R(X') → R(X) over it, itself a local analytic isomorphism ([Wlo09, Theorem 2.0.1 (3)]). Over every open on which φ is injective, the lift of φ restricts to the lift of the isomorphism of open subspaces (ResolutionAssignment.LiftsLocalIsomorphisms.lift_restrict).

Kollár's (4), "Π_X is projective over any compact subset of X", is split between the properness of Hom.IsResolution and the factorization clause, whose ambient manifold is the disjoint union of finitely many opens of Kⁿ, one per piece of a finite open cover of the relatively compact open, with the identification with Π_X given piecewise. The non-singularity of R(X) is repeated by (3), since ClosedSubspace.IsSncBoundary asks for a regular system of parameters at every point of R(X).

Relation to the source.

  • Translation. R.space X and R.map X are Kollár's $R(X)$ and $\Pi_X$ for the input X, whose underlying space is X.obj; X.regularLocus is the set of simple points (his $X^{ns}$) and X.singularLocus its complement; clause (3) is a closed subspace E with E.IsSncBoundary and E.support equal to $\Pi_X^{-1}(\operatorname{Sing} X)$. Composition ≫ is in diagrammatic order: in (5), ψ ≫ (R.map Y).restrictSet V = (R.map X).restrictSet U ≫ φ is $\Pi_Y|_V \circ \psi = \varphi \circ \Pi_X|_U$, and ψ ≫ R.map X = R.map X' ≫ φ is $\Pi_X \circ \psi = \varphi \circ \Pi_{X'}$.
  • Interpretation. Kollár's resolution is birational and Włodarczyk's bimeromorphic. Here $\Pi_X$ is bimeromorphic onto its image: an isomorphism over an open set whose preimage is dense.
  • Gap. Kollár states the theorem for any locally compact field $K$ of characteristic zero; here K = ℝ or K = ℂ (RCLike K).
  • Gap. Kollár states the theorem for every separable $K$-analytic space. His notion of resolution [Kol07, (2), (3)] is stated for varieties, and his proofs are for reduced spaces, extended to reducible ones [Kol07, Theorem 36, proof; Proposition 37]. Here the inputs are the reduced spaces (ReducedSpace); a non-reduced $X$ is resolved through its reduction, by $\Pi_{X_{\mathrm{red}}}$ followed by the closed immersion $X_{\mathrm{red}} \to X$.
  • Gap. Kollár's clause (4), "$\Pi_X$ is projective over any compact subset of $X$", is replaced by properness together with the ambient blow-up factorization over relatively compact opens [Kol07, Warning 23]; [Wlo09, Theorem 2.0.2, (∗)].
  • Strengthening. Over $\mathbb{R}$ the simple locus of a reduced space need not be dense Hir64, Introduction: the subspace $x^2 + y^2 = 0$ of $\mathbb{R}^2$ is reduced and has support the origin and no simple point (in HironakaExamples: Hironaka.Space.circleSpace_isReduced, Hironaka.Manifold.circleIdeal_cosupport_eq_singleton and Hironaka.Manifold.circleIdeal_regSet_eq_empty). So $\Pi_X$ need not be surjective; its image is the closure of the simple locus, a clause printed in neither source.
  • Gap. Kollár's clause (5), "$R$ commutes with smooth $K$-morphisms", is replaced by the unique lifting of isomorphisms between open subspaces and of local analytic isomorphisms, the smooth morphisms of relative dimension zero, Kollár's étale morphisms. Since the lifts are unique, they respect identities and composition, so $R$ is functorial for the étale morphisms between inputs. Smooth morphisms of positive relative dimension are not lifted, and the isomorphism $R(Y) \cong Y \times_X R(X)$ is not stated.
  • Strengthening. Włodarczyk's clause (3) lifts every local analytic isomorphism $\varphi \colon Y' \to Y$ to a natural local analytic isomorphism $\tilde\varphi \colon \tilde Y' \to \tilde Y$. Here the lift is the only morphism $R(Y') \to R(Y)$ over $\varphi$, and a local analytic isomorphism; the lift of an isomorphism between open subspaces is likewise the only morphism over it, so the lift of $\varphi$ restricts, over every open on which $\varphi$ is injective, to the lift of the isomorphism of open subspaces, and the naturality follows from the uniqueness. The lift is glued from those lifts over the opens on which $\varphi$ is injective, and the uniqueness rests on the rigidity of morphisms out of a non-singular space: two morphisms that agree on a dense open subspace agree.

Source statement: [Kol07, Theorem 45]

Source statement: [Wlo09, Theorem 2.0.1]

source
theorem AnalyticSpace.exists_surjective_resolution_of_isReduced (X : AnalyticSpace ℂ) (hX : X.IsReduced) :
∃ (R : AnalyticSpace ℂ) (π : R ⟶ X), Hom.IsStrongResolution π ∧ Hom.IsLocallyFiniteAmbientBlowUpComposite π ∧ Function.Surjective ↑π

Resolution of a reduced complex-analytic space [Kol07, Theorem 45 (1)–(4)]; [Wlo09, Theorem 2.0.1], for K = ℂ. Let X be a reduced complex-analytic space. Then there is a morphism π : R → X such that

  • π is a strong resolution of X (Hom.IsStrongResolution): π is proper and bimeromorphic onto its image, and (1) R is non-singular; (2) π is an isomorphism over the simple locus X.regularLocus; (3) π⁻¹(X.singularLocus) is the support of a simple normal crossing divisor of R;
  • (4) over every relatively compact open subset of X, π is the composite of a finite sequence of blow-ups of smooth centres of an ambient manifold, restricted to strict transforms (Hom.IsLocallyFiniteAmbientBlowUpComposite);
  • π is surjective.

Relation to the source.

  • Gap. The statement is not printed in this form: it is [Kol07, Theorem 45 (1)–(4)] and Wlo09, Theorem 2.0.1 (1)–(2) for K = ℂ and a single space, without the functoriality of Kollár's (5) and Włodarczyk's (3).
  • Gap. As in AnalyticSpace.exists_functorial_resolution: Kollár's Theorem 45 concerns every separable complex space and here X is reduced, and Kollár's "projective over any compact subset" is replaced by properness together with the ambient blow-up factorization over relatively compact opens.
  • Strengthening. Surjectivity is not a printed clause. It is what Włodarczyk's "proper bimeromorphic" gives for a reduced complex space, whose simple locus is dense Hir64, Introduction.

Source statement: [Kol07, Theorem 45 (1)–(4)]

Source statement: [Wlo09, Theorem 2.0.1] (surjectivity from the density of the simple locus over ℂ)