Local embedding data of a relatively compact piece of an analytic space

The resolution of an analytic space is assembled from local embeddings into affine space. Kollár chooses an embedding of the variety into a smooth variety ([Kol07, Corollary 22, proof] and [Kol07, Theorem 36, proof]) and glues the resolutions of the members of an affine cover [Kol07, Proposition 37, proof]; Włodarczyk covers the analytic space by neighbourhoods V locally isomorphic to closed analytic subsets of open balls U ⊂ ℂⁿ, shrunk to V_i ⊆ W_i ⊆ U_i with compact closures [Wlo09, §4, (3)⇒(4)], and makes the ambient dimensions agree by adding coordinates [Wlo09, §7.1]. An analytic space is by definition locally isomorphic to a local analytic space in Kⁿ [Hir64, Ch. 0, §1, pp. 119–120]. This module defines the data of such local embeddings, in the vocabulary of the structure AmbientBlowUpFactorization with which the resolution theorem for analytic spaces (exists_functorial_resolution) is stated.

• pieceAmbient G: the open G ⊆ 𝕜ⁿ as the disjoint-union manifold sigmaOpens with ONE summand — the universe lift used throughout (a manifold with carrier ↥G lives in Type, the analytic spaces in Type u; AnalyticSpace.Hom takes both spaces at one universe). Its points are ⟨(), x⟩.
• PieceEmbedding 𝕜 n X V: a closed embedding of the open subspace X|V into an open G ⊆ 𝕜ⁿ — the ideal sheaf 𝓘_Y on pieceAmbient G, nonzero at every stalk and reduced, with an isomorphism of analytic 𝕜-spaces X|V ≅ Sp(G)/𝓘_Y (the fields emb, emb_isIso of AmbientBlowUpFactorization); n is a parameter, so that two embeddings of one piece into 𝕜ⁿ and 𝕜ᵐ can be compared.
• PieceEmbedding.ambientTriple E: the analytic triple (G, 𝓘_Y, ∅), the input of the embedded desingularization functor for the piece (to desingularize Y one resolves the marked ideal (I_Y, 1) with empty divisor, [Wlo09, §6, Remark (3) after Step 2b]).
• LocalEmbeddingData 𝕜 X U: finitely many open pieces Uᵢ ⊆ X with relatively compact inner opens Vᵢ, closure Vᵢ ⊆ Uᵢ, covering U, one ambient dimension n, and a PieceEmbedding 𝕜 n X Uᵢ per piece; LocalEmbeddingData.subset_iUnion_piece (the corresponding field of AmbientBlowUpFactorization) is derived.

That every relatively compact open of a reduced analytic 𝕜-space carries such data is exists_localEmbeddingData_of_padTools (PieceModel.lean) at the padding tools padTools of PieceModelPad.lean.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.pieceAmbient (𝕜 : Type) [RCLike 𝕜] {n : ℕ} (G : TopologicalSpace.Opens (Fin n → 𝕜)) : AnalyticManifold 𝕜 (Fin n → 𝕜)

The one-piece ambient: the open G ⊆ 𝕜ⁿ as the disjoint-union manifold sigmaOpens with a single summand, so that it lives in the universe of the analytic spaces it embeds (AnalyticSpace.Hom takes both spaces at one universe; the carrier ↥G alone is in Type). Its points are ⟨(), x⟩. The ambient manifold of an AmbientBlowUpFactorization is the disjoint union of the ambients of the members of a finite open cover, as in the gluing argument of [Kol07, Proposition 37, proof].

Equations

• Hironaka.Manifold.pieceAmbient 𝕜 G = AnalyticManifold.sigmaOpens fun (x : PUnit.{?u.1 + 1}) => G

structure Hironaka.Manifold.PieceEmbedding (𝕜 : Type) [RCLike 𝕜] (n : ℕ) (X : AnalyticSpace 𝕜) (V : Set ↑↑X.toPresheafedSpace) : Type u

A closed embedding of the open subspace X|V into an open G ⊆ 𝕜ⁿ, the local model of an analytic space ([Hir64, Ch. 0, §1, pp. 119–120]; the embedding into a smooth variety of [Kol07, Corollary 22, proof] and [Kol07, Theorem 36, proof]; the neighbourhood isomorphic to a closed analytic subset of a ball of [Wlo09, §4, (3)⇒(4)]): the ideal sheaf 𝓘_Y of the closed subspace Y ⊆ G on the one-piece ambient, nonzero at every stalk (as after adding a coordinate, [Wlo09, §7.1]) and reduced (the defining ideal of a reduced subspace), with an isomorphism of analytic 𝕜-spaces X|V ≅ Sp(G)/𝓘_Y (the fields emb, emb_isIso of AmbientBlowUpFactorization). The ambient dimension n is a parameter, so that two embeddings of one piece into 𝕜ⁿ and 𝕜ᵐ can be compared.

• G : TopologicalSpace.Opens (Fin n → 𝕜)

  The open subset G ⊆ 𝕜ⁿ.

• ideal : (pieceAmbient 𝕜 self.G).IdealSheaf

  The ideal sheaf 𝓘_Y of the closed subspace Y ⊆ G (locally finitely generated).

• isNonzeroEverywhere : Manifold.IdealSheaf.IsNonzeroEverywhere self.ideal

  𝓘_Y is nonzero at every stalk.

• isReduced : self.ideal.IsReduced

  𝓘_Y is reduced: the defining ideal sheaf of a reduced closed subspace has radical stalks.

• emb : X.restrictSet V ⟶ self.ideal.toAnalyticSpace

  The closed embedding: X|V is isomorphic to Sp(G)/𝓘_Y …

• emb_isIso : CategoryTheory.IsIso self.emb

  … as analytic 𝕜-spaces.

def Hironaka.Manifold.PieceEmbedding.ambientTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (pieceAmbient 𝕜 E.G)

The analytic triple (G, 𝓘_Y, ∅) of the piece: the input of the embedded desingularization functor for the piece (to desingularize Y one resolves the marked ideal (I_Y, 1) with empty divisor, [Wlo09, §6, Remark (3) after Step 2b]); its divisor is empty (HypersurfaceFamily.empty, index PEmpty, simple normal crossings by isSnc_empty).

Equations

• E.ambientTriple = { I := E.ideal, isNonzeroEverywhere := ⋯, F := Manifold.HypersurfaceFamily.empty (Hironaka.Manifold.pieceAmbient 𝕜 E.G).carrier, isSnc := ⋯ }

theorem Hironaka.Manifold.PieceEmbedding.ambientTriple_F {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : E.ambientTriple.F = Manifold.HypersurfaceFamily.empty (pieceAmbient 𝕜 E.G).carrier

The divisor of the piece's triple is empty.

theorem Hironaka.Manifold.PieceEmbedding.ambientTriple_I {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : E.ambientTriple.I = E.ideal

The ideal sheaf of the piece's triple is 𝓘_Y.

structure Hironaka.Manifold.LocalEmbeddingData (𝕜 : Type) [RCLike 𝕜] (X : AnalyticSpace 𝕜) (U : Set ↑↑X.toPresheafedSpace) : Type (u + 1)

The local embedding data of an open U ⊆ X: finitely many open pieces Uᵢ with relatively compact inner opens Vᵢ, closure Vᵢ ⊆ Uᵢ, covering U; one ambient dimension n; and a closed embedding of each X|Uᵢ into an open of 𝕜ⁿ (PieceEmbedding). The fields n, ι, finite, piece, isOpen_piece are the first block of AmbientBlowUpFactorization; the shrinking is Włodarczyk's cover V_i ⊆ W_i ⊆ U_i with compact closures [Wlo09, §4, (3)⇒(4)], the common n his addition of coordinates [Wlo09, §7.1], and the finite affine cover the one glued in [Kol07, Proposition 37, proof].

• n : ℕ

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

• ι : Type u

  The finite index set of the pieces.

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

  The open subspaces Uᵢ ⊆ X carrying the local models …

• isOpen_piece (i : self.ι) : IsOpen (self.piece i)
• inner : self.ι → Set ↑↑X.toPresheafedSpace

  … and the inner opens Vᵢ, relatively compact in X with closure Vᵢ ⊆ Uᵢ (Włodarczyk's V_i ⊆ W_i ⊆ U_i with compact closures [Wlo09, §4, (3)⇒(4)]), …

• isOpen_inner (i : self.ι) : IsOpen (self.inner i)
• isCompact_closure_inner (i : self.ι) : IsCompact (closure (self.inner i))
• closure_inner_subset (i : self.ι) : closure (self.inner i) ⊆ self.piece i
• subset_iUnion_inner : U ⊆ ⋃ (i : self.ι), self.inner i

  … covering U.

• embedding (i : self.ι) : PieceEmbedding 𝕜 self.n X (self.piece i)

  The closed embedding of each piece into an open of 𝕜ⁿ.

theorem Hironaka.Manifold.LocalEmbeddingData.subset_iUnion_piece {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) : U ⊆ ⋃ (i : D.ι), D.piece i

The pieces cover U (the field subset_iUnion_piece of AmbientBlowUpFactorization), from the inner opens.