Resolutions of analytic spaces

The terms in which the resolution of K-analytic spaces is stated (the form of [Kol07, Theorem 45] in AnalyticSpace.exists_functorial_resolution, and its specialization to K = ℂ in AnalyticSpace.exists_surjective_resolution_of_isReduced), as opposed to the machinery that constructs them.

• f.AmbientBlowUpFactorization U and f.IsLocallyFiniteAmbientBlowUpComposite: over every relatively compact open U ⊆ X, f is the composite of finitely many blow-ups of an ambient manifold with smooth centres, restricted to strict transforms — the form taken here by clause (4) of [Kol07, Theorem 45], "projective over any compact subset", following [Kol07, Warning 23] and the local factorization (∗) of [Wlo09, Theorem 2.0.2]. The ambient is the disjoint union AnalyticManifold.sigmaOpens G of finitely many opens of Kⁿ; its closed subspaces are analytic spaces through IdealSheaf.toAnalyticSpace, and IdealSheaf.overPiece is the part of such a subspace lying over one summand.
• Hom.IsResolution π [Kol07, (2)] and Hom.IsStrongResolution π Kol07, (3); Theorem 45 (1)–(3): the properties of a value π : R → X of the resolution, the analytic counterparts of Scheme.BlowUpSequence.IsResolution and Scheme.BlowUpSequence.IsStrongResolution.
• HasUnderlyingSpace C K: a type C of inputs each with an underlying K-analytic space — the spaces themselves, and the full subcategories of a class of spaces. ResolutionAssignment C: an assignment R of a space R(X) and a morphism Π_X : R(X) → X to every input X, Kollár's "resolution functor R : X ↦ (Π_X : R(X) → X)" of [Kol07, Theorem 45] stripped of its properties.
• Hom.IsStrongResolutionOntoClosureRegularLocus π: a strong resolution whose image is the closure of the simple locus, clauses (1)–(3) of Theorem 45 with the image clause.
• Hom.IsLocalIso φ: φ : X' → X is a local analytic isomorphism, locally an isomorphism onto an open subspace of X (the local analytic isomorphisms of [Wlo09, Theorem 2.0.1 (3)]); and ResolutionAssignment.LiftsLocalIsomorphisms R: every isomorphism between open subspaces of two inputs lifts to exactly one morphism of the resolutions over it, an isomorphism, and every local analytic isomorphism between inputs lifts to exactly one morphism of the resolutions over it, a local analytic isomorphism — clause (5) of Theorem 45 for étale morphisms, and Włodarczyk's clause (3).
• ReducedSpace K: the inputs of the resolution theorem, the reduced K-analytic spaces as a full subcategory of the K-analytic spaces.

The ambient blow-up factorization

def AnalyticManifold.IdealSheaf.overPiece {K : Type} [RCLike K] {n : ℕ} {ι : Type u} [Countable ι] {G : ι → TopologicalSpace.Opens (Fin n → K)} (J : (sigmaOpens G).IdealSheaf) (i : ι) : Set ↑↑J.toAnalyticSpace.toPresheafedSpace

The part of the closed subspace Sp(A)/J of A = ⊔ᵢ Gᵢ lying over the summand Gᵢ: the points whose image in A has index i.

Equations

• J.overPiece i = {y : ↑↑J.toAnalyticSpace.toPresheafedSpace | (↑J.toAnalyticSpaceι y).fst = i}

structure AnalyticSpace.Hom.AmbientBlowUpFactorization {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) (U : Set ↑↑X.toPresheafedSpace) : Type (u + 1)

An ambient blow-up factorization of f : Y → X over the open U ⊆ X (after [Kol07, Warning 23] and the local factorization (∗) of [Wlo09, Theorem 2.0.2], with the disjoint-union ambient of the proof of [Kol07, Proposition 37]): finitely many open subspaces Uᵢ covering U; closed embeddings X|Uᵢ ↪ Gᵢ ⊆ Kⁿ (one n for all i, by padding), given as the ideal sheaf J₀ on the ambient A := ⊔ᵢ Gᵢ (sigmaOpens) of the closed subspace Y₀ = ⊔ᵢ X|Uᵢ together with isomorphisms of X|Uᵢ with the part of Sp(A)/J₀ over Gᵢ; a finite sequence π₀, …, π_{r-1} of blow-ups of A with smooth centres (a FiniteSuccession); the strict transforms Y₀, …, Y_r, Y_{k+1} the strict transform of Y_k under π_k, of finite type (the saturation of the pulled-back ideal along the exceptional divisor has local generators), with Y_r a closed submanifold of A_r; and, for each i, an isomorphism over Uᵢ of f⁻¹(Uᵢ) → Uᵢ with Π_r|_{Y_r} : Y_r → Y₀ = X|Uᵢ, Π_r = π₀ ∘ ⋯ ∘ π_{r-1} (the morphism of closed subspaces over Π_r, unique since the canonical morphism of a closed subspace is a monomorphism), over the piece Gᵢ.

• n : ℕ

  The common dimension n of the ambient pieces Gᵢ ⊆ Kⁿ.

• ι : Type u

  The finite index set of the pieces.

• finite : Finite self.ι
• piece : self.ι → Set ↑↑X.toPresheafedSpace

  The open subspaces Uᵢ ⊆ X …

• isOpen_piece (i : self.ι) : IsOpen (self.piece i)
• subset_iUnion_piece : U ⊆ ⋃ (i : self.ι), self.piece i

  … covering U.

• G : self.ι → TopologicalSpace.Opens (Fin self.n → K)

  The open subsets Gᵢ ⊆ Kⁿ.

• ideal : (AnalyticManifold.sigmaOpens self.G).IdealSheaf

  The ideal sheaf J₀ on A = ⊔ᵢ Gᵢ of the closed subspace Y₀ = ⊔ᵢ X|Uᵢ (locally finitely generated).

• emb (i : self.ι) : X.restrictSet (self.piece i) ⟶ self.ideal.toAnalyticSpace.restrictSet (self.ideal.overPiece i)

  The closed embeddings: X|Uᵢ is isomorphic to the part of Y₀ = Sp(A)/J₀ over Gᵢ …

• emb_isIso (i : self.ι) : CategoryTheory.IsIso (self.emb i)

  … as analytic K-spaces.

• seq : (AnalyticManifold.sigmaOpens self.G).FiniteSuccession

  The finite sequence of blow-ups π₀, …, π_{r-1} of A with smooth centres.

• transform (k : Fin (self.seq.length + 1)) : (self.seq.stage k).IdealSheaf

  The closed subspaces Y_k ⊆ A_k of the stages, …

• transform_zero : self.transform 0 = self.ideal

  … starting with Y₀, …

• transform_succ (k : Fin self.seq.length) : self.transform k.succ = Manifold.strictTransformSubspace ⋯ ⋯ (self.transform k.castSucc)

  … Y_{k+1} the strict transform of Y_k under π_k (strictTransformSubspace at the witnesses of the k-th blow-up), …

• hasLocalGenerators_saturation (k : Fin self.seq.length) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (self.transform k.castSucc))

  … of finite type: the saturation ⋃_m (π_k⁻¹(I_{Y_k}) : I_{F}^m) has local generators, so Y_{k+1} is the saturation and not the unit-ideal fallback of strictTransformSubspace.

• isNonsingular_last : (self.transform (Fin.last self.seq.length)).IsNonsingular

  Y_r is a closed submanifold of A_r: every point of Y_r is simple.

• map : (self.transform (Fin.last self.seq.length)).toAnalyticSpace ⟶ self.ideal.toAnalyticSpace

  Π_r|_{Y_r} : Y_r → Y₀, the morphism of closed subspaces …

• map_comp : CategoryTheory.CategoryStruct.comp self.map self.ideal.toAnalyticSpaceι = CategoryTheory.CategoryStruct.comp (self.transform (Fin.last self.seq.length)).toAnalyticSpaceι (toSpaceHom (ContinuousLinearEquiv.refl K (Fin self.n → K)) self.seq.composite)

  … lying over Π_r = π₀ ∘ ⋯ ∘ π_{r-1} (the composite of the succession).

• lift (i : self.ι) : Y.restrictSet (↑f ⁻¹' self.piece i) ⟶ (self.transform (Fin.last self.seq.length)).toAnalyticSpace.restrictSet (↑self.map ⁻¹' self.ideal.overPiece i)

  The isomorphism over Uᵢ of f⁻¹(Uᵢ) → Uᵢ with Π_r|_{Y_r} over the piece Gᵢ: f⁻¹(Uᵢ) is isomorphic to the part of Y_r over Gᵢ …

• lift_isIso (i : self.ι) : CategoryTheory.IsIso (self.lift i)
• map_lift (i : self.ι) : CategoryTheory.CategoryStruct.comp (self.lift i) (restrictSet self.map (self.ideal.overPiece i)) = CategoryTheory.CategoryStruct.comp (restrictSet f (self.piece i)) (self.emb i)

  … compatibly with f and Π_r|_{Y_r}.

def AnalyticSpace.Hom.IsLocallyFiniteAmbientBlowUpComposite {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : Y ⟶ X) : Prop

Clause (4) of [Kol07, Theorem 45], "Π_X is projective over any compact subset of X", in the form of [Kol07, Warning 23] and of the local factorization (∗) of [Wlo09, Theorem 2.0.2]: over every relatively compact open U ⊆ X, f restricted to f⁻¹(U) is the composite of a finite sequence of blow-ups of smooth centres of an ambient manifold, restricted to strict transforms — an f.AmbientBlowUpFactorization U. The clause plays the role of Hironaka's local finiteness of a succession [Hir64, Ch. 0, §7, p. 155]: every point has a relatively compact open neighbourhood over which f is one finite composite (no compatibility between the factorizations over different opens is asserted).

Equations

• AnalyticSpace.Hom.IsLocallyFiniteAmbientBlowUpComposite f = ∀ (U : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact (closure U) → Nonempty (AnalyticSpace.Hom.AmbientBlowUpFactorization f U)

Resolutions

structure AnalyticSpace.Hom.IsResolution {K : Type} [RCLike K] {X R : AnalyticSpace K} (π : R ⟶ X) : Prop

A morphism π : R → X of K-analytic spaces is a resolution of X: R is non-singular, π is proper, and π is bimeromorphic (Kollár: birational [Kol07, (2)]; [Wlo09, Theorem 2.0.1]), read onto its image: an isomorphism over an open subset U ⊆ X whose preimage is dense in R. Kollár asks for π projective; only the properness that projectivity implies is recorded. The density is asked of the preimage and not of U: over ℝ the simple locus of a reduced space need not be dense ([Hir64, Introduction]), and then no resolution is an isomorphism over a dense open subset of X.

• isNonsingular : R.IsNonsingular

  R is non-singular.

• isProperMap : IsProperMap ↑π

  π is proper [Kol07, (2)] (Kollár: projective).

• exists_isIsoOver_dense_preimage : ∃ (U : Set ↑↑X.toPresheafedSpace), IsOpen U ∧ IsIsoOver π U ∧ Dense (↑π ⁻¹' U)

  π is an isomorphism over an open subset of X whose preimage is dense in R.

theorem AnalyticSpace.Hom.isResolution_iff {K : Type} [RCLike K] {X R : AnalyticSpace K} (π : R ⟶ X) : IsResolution π ↔ R.IsNonsingular ∧ IsProperMap ↑π ∧ ∃ (U : Set ↑↑X.toPresheafedSpace), IsOpen U ∧ IsIsoOver π U ∧ Dense (↑π ⁻¹' U)

structure AnalyticSpace.Hom.IsStrongResolution {K : Type} [RCLike K] {X R : AnalyticSpace K} (π : R ⟶ X) extends AnalyticSpace.Hom.IsResolution π : Prop

A morphism π : R → X of K-analytic spaces is a strong resolution of X [Kol07, (3)], clauses (1)–(3) of [Kol07, Theorem 45]: a resolution (non-singular, proper, bimeromorphic onto its image) that is an isomorphism over the simple locus X.regularLocus (Kollár's smooth locus X^{ns}), and such that π⁻¹(X.singularLocus) is the support of a simple normal crossing divisor of R: a closed subspace which is the reduced divisor of a locally finite family of closed smooth hypersurfaces with simple normal crossings (ClosedSubspace.IsSncBoundary; [Kol07, Definition 24]).

• isNonsingular : R.IsNonsingular
• isProperMap : IsProperMap ↑π
• exists_isIsoOver_dense_preimage : ∃ (U : Set ↑↑X.toPresheafedSpace), IsOpen U ∧ IsIsoOver π U ∧ Dense (↑π ⁻¹' U)
• isIsoOver_regularLocus : IsIsoOver π X.regularLocus

  π is an isomorphism over the simple locus X^{ns}.

• exists_isSncBoundary_preimage : ∃ (E : R.ClosedSubspace), E.IsSncBoundary ∧ Manifold.IdealSheaf.support E = ↑π ⁻¹' X.singularLocus

  π⁻¹(Sing X) is the support of a simple normal crossing divisor.

theorem AnalyticSpace.Hom.isStrongResolution_iff {K : Type} [RCLike K] {X R : AnalyticSpace K} (π : R ⟶ X) : IsStrongResolution π ↔ IsResolution π ∧ IsIsoOver π X.regularLocus ∧ ∃ (E : R.ClosedSubspace), E.IsSncBoundary ∧ Manifold.IdealSheaf.support E = ↑π ⁻¹' X.singularLocus

Resolution assignments

class AnalyticSpace.HasUnderlyingSpace (C : Type w) (K : outParam Type) [RCLike K] : Type (max w (u + 1))

A type C of inputs each with an underlying K-analytic space (the analogue of HasUnderlyingScheme for the algebraic inputs): the K-analytic spaces themselves, and the full subcategories of the spaces of a class.

• toAnalyticSpace : C → AnalyticSpace K

  The underlying analytic space of an input.

@[instance_reducible]

instance AnalyticSpace.hasUnderlyingSpaceSelf {K : Type} [RCLike K] : HasUnderlyingSpace (AnalyticSpace K) K

Every K-analytic space is an input.

Equations

• AnalyticSpace.hasUnderlyingSpaceSelf = { toAnalyticSpace := fun (X : AnalyticSpace K) => X }

@[instance_reducible]

instance AnalyticSpace.FullSubcategory.hasUnderlyingSpace {K : Type} [RCLike K] {C : Type w} [CategoryTheory.Category.{u_1, w} C] [HasUnderlyingSpace C K] (P : CategoryTheory.ObjectProperty C) : HasUnderlyingSpace P.FullSubcategory K

The objects of a full subcategory of inputs are inputs.

Equations

• AnalyticSpace.FullSubcategory.hasUnderlyingSpace P = { toAnalyticSpace := fun (X : P.FullSubcategory) => AnalyticSpace.toAnalyticSpace X.obj }

structure AnalyticSpace.ResolutionAssignment {K : Type} [RCLike K] (C : Type w) [HasUnderlyingSpace C K] : Type (max w (u + 1))

A resolution assignment on the inputs C: a K-analytic space R(X) and a morphism Π_X : R(X) → X to the underlying space of every input X — Kollár's "resolution functor R : X ↦ (Π_X : R(X) → X)" [Kol07, Theorem 45] stripped of its properties, which are the clauses of exists_functorial_resolution. The theorem's inputs are the reduced spaces (ReducedSpace); the constructions behind it produce assignments on all spaces (ResolutionAssignment (AnalyticSpace K)).

• space : C → AnalyticSpace K

  The resolving space R(X).

• map (X : C) : self.space X ⟶ toAnalyticSpace X

  The resolution morphism Π_X : R(X) → X.

Strong resolutions onto the closure of the simple locus

structure AnalyticSpace.Hom.IsStrongResolutionOntoClosureRegularLocus {K : Type} [RCLike K] {X R : AnalyticSpace K} (π : R ⟶ X) extends AnalyticSpace.Hom.IsStrongResolution π : Prop

A morphism π : R → X of K-analytic spaces is a strong resolution onto the closure of the simple locus of X: a strong resolution (Hom.IsStrongResolution: non-singular, proper, bimeromorphic onto its image, an isomorphism over the simple locus X.regularLocus, and π⁻¹(Sing X) the support of a simple normal crossing divisor — clauses (1)–(3) of [Kol07, Theorem 45]) whose image is the closure of the simple locus. Over ℂ the simple locus of a reduced space is dense and the clause says that π is surjective; over ℝ it need not be dense ([Hir64, Introduction]: the subspace x² + y² = 0 of ℝ² is reduced with support the origin and no simple point), and then π misses the part of X away from the closure of the simple points.

Relation to the source.

• Strengthening. The image clause is printed in neither source. It is what a resolution built over the simple locus gives, and over $\mathbb{C}$ it is the surjectivity of $\Pi_X$.

• isNonsingular : R.IsNonsingular
• isProperMap : IsProperMap ↑π
• exists_isIsoOver_dense_preimage : ∃ (U : Set ↑↑X.toPresheafedSpace), IsOpen U ∧ IsIsoOver π U ∧ Dense (↑π ⁻¹' U)
• isIsoOver_regularLocus : IsIsoOver π X.regularLocus
• exists_isSncBoundary_preimage : ∃ (E : R.ClosedSubspace), E.IsSncBoundary ∧ Manifold.IdealSheaf.support E = ↑π ⁻¹' X.singularLocus
• range_eq : Set.range ↑π = closure X.regularLocus

  The image of π is the closure of the simple locus of X.

theorem AnalyticSpace.Hom.isStrongResolutionOntoClosureRegularLocus_iff {K : Type} [RCLike K] {X R : AnalyticSpace K} (π : R ⟶ X) : IsStrongResolutionOntoClosureRegularLocus π ↔ IsStrongResolution π ∧ Set.range ↑π = closure X.regularLocus

Local analytic isomorphisms

def AnalyticSpace.Hom.IsLocalIso {K : Type} [RCLike K] {X' X : AnalyticSpace K} (φ : X' ⟶ X) : Prop

A morphism φ : X' ⟶ X of K-analytic spaces is a local analytic isomorphism when every point of X' has an open neighbourhood U' which φ maps isomorphically onto an open subspace X|_V of X: an isomorphism χ : X'|_{U'} ≅ X|_V with χ ≫ (X|_V → X) = (X'|_{U'} → X') ≫ φ. These are the local analytic isomorphisms of [Wlo09, Theorem 2.0.1 (3)] (Kollár's étale morphisms, the smooth morphisms of relative dimension zero [Kol07, Theorem 45 (5)]): open immersions, isomorphisms, covering maps and the morphism ∐ Uᵢ → X from the disjoint union of an open cover, injective or not.

Equations

• One or more equations did not get rendered due to their size.

structure AnalyticSpace.ResolutionAssignment.LiftsLocalIsomorphisms {K : Type} [RCLike K] {C : Type w} [HasUnderlyingSpace C K] (R : ResolutionAssignment C) : Prop

A resolution assignment R on the inputs C lifts local analytic isomorphisms, in two forms. Every isomorphism φ : X|_U → Y|_V between open subspaces of two inputs lifts to exactly one morphism ψ : R(X)|_{Π_X⁻¹ U} → R(Y)|_{Π_Y⁻¹ V} over φ, ψ ≫ Π_Y|_V = Π_X|_U ≫ φ, where Π_X|_U : R(X)|_{Π_X⁻¹ U} → X|_U is the restriction of Π_X (composition in diagrammatic order), and ψ is an isomorphism. And every local analytic isomorphism φ : X' → X between inputs (Hom.IsLocalIso) lifts to exactly one morphism ψ : R(X') → R(X) over φ, ψ ≫ Π_X = Π_{X'} ≫ φ, and ψ is a local analytic isomorphism. Over every open U' ⊆ X' which φ maps isomorphically onto an open subspace X|_V, the lift of φ restricts to the lift of that isomorphism, by the uniqueness of the latter (LiftsLocalIsomorphisms.lift_restrict). By the uniqueness the lifts respect identities and composition, so R is a functor on the groupoid of isomorphisms between open subspaces of inputs and on the local analytic isomorphisms between inputs.

Relation to the source.

• Translation. The first form stands for clause (5) of [Kol07, Theorem 45], "$R$ commutes with smooth $K$-morphisms", for the smooth morphisms of relative dimension zero that are injective; the second is clause (3) of [Wlo09, Theorem 2.0.1], "for any local analytic isomorphism $\varphi \colon Y' \to Y$ there is a natural lifting $\tilde\varphi \colon \tilde Y' \to \tilde Y$ which is a local analytic isomorphism", and the case of étale morphisms of Kollár's (5); the two are bundled as the two conditions of Kollár's 34.1 are in the algebraic CommutesWithSmoothMorphisms. Composition ≫ is in diagrammatic order: ψ ≫ (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'}$.
• Gap. Smooth morphisms of positive relative dimension are not lifted, and the isomorphism $R(Y) \cong Y \times_X R(X)$ of Kollár's (5) is not stated.

• exists_lift_of_isIso (X Y : C) (U : Set ↑↑(toAnalyticSpace X).toPresheafedSpace) (V : Set ↑↑(toAnalyticSpace Y).toPresheafedSpace) : IsOpen U → IsOpen V → ∀ (φ : (toAnalyticSpace X).restrictSet U ⟶ (toAnalyticSpace Y).restrictSet V), CategoryTheory.IsIso φ → ∃ (ψ : (R.space X).restrictSet (↑(R.map X) ⁻¹' U) ⟶ (R.space Y).restrictSet (↑(R.map Y) ⁻¹' V)), CategoryTheory.IsIso ψ ∧ ∀ (ψ' : (R.space X).restrictSet (↑(R.map X) ⁻¹' U) ⟶ (R.space Y).restrictSet (↑(R.map Y) ⁻¹' V)), CategoryTheory.CategoryStruct.comp ψ' (Hom.restrictSet (R.map Y) V) = CategoryTheory.CategoryStruct.comp (Hom.restrictSet (R.map X) U) φ ↔ ψ' = ψ

  Every isomorphism between open subspaces of two inputs lifts to exactly one morphism of the resolutions over it, an isomorphism.

• exists_lift_of_isLocalIso (X' X : C) (φ : toAnalyticSpace X' ⟶ toAnalyticSpace X) : Hom.IsLocalIso φ → ∃ (ψ : R.space X' ⟶ R.space X), Hom.IsLocalIso ψ ∧ ∀ (ψ' : R.space X' ⟶ R.space X), CategoryTheory.CategoryStruct.comp ψ' (R.map X) = CategoryTheory.CategoryStruct.comp (R.map X') φ ↔ ψ' = ψ

  Every local analytic isomorphism between inputs lifts to exactly one morphism of the resolutions over it, a local analytic isomorphism.

The inputs: reduced spaces

@[reducible, inline]

abbrev AnalyticSpace.ReducedSpace (K : Type) [RCLike K] : Type (u + 1)

The inputs of the resolution theorem: the reduced K-analytic spaces, as a full subcategory of the K-analytic spaces. An object X has X.obj : AnalyticSpace K, its underlying space (toAnalyticSpace X).

Equations

• AnalyticSpace.ReducedSpace K = CategoryTheory.ObjectProperty.FullSubcategory fun (X : AnalyticSpace K) => X.IsReduced