Pieces from local models: the existence of local embedding data

Every point of an analytic K-space has a neighbourhood K-isomorphic to a local analytic K-space (S(𝓘), 𝒜_G/𝓘), G ⊆ Kⁿ open [Hir64, Ch. 0, §1, pp. 119–120] (exists_kIso_localModel); for a relatively compact open U finitely many such models cover the compact closure U. This module turns those models into the LocalEmbeddingData of PieceEmbedding.lean:

• the bridge modelBridge G' : (G', 𝒜_{G'}) ≅ Sp(pieceAmbient 𝕜 (downOpens G')) — the model open G' ⊆ Kn 𝕜 n (the universe-lifted Kⁿ) read as an open of Fin n → 𝕜, and the one-piece Σ-ambient identified with it by two inverse analytic maps (ofManifoldIso, ofManifold_restrictOpen_iso; ContMDiff.sigmaDesc, contMDiff_sigmaMk_comp_iff);
• the transport of the model's ideal 𝓘 = (f₁, …, f_k) along the bridge (transportIdeal, quotient_kIso): modelPieceIdeal G' f with Sp(A)/𝓘 ≅ (S(𝓘), 𝒜/𝓘), hence the piece's model isomorphism X|_V ≅ Sp(A)/𝓘 (modelPieceEmbIso), and its reducedness on a reduced X (the closed subspace is X|_V, whose stalks are reduced; ClosedSubspace.isReduced_iff);
• the shrinking of a finite cover of closure U to inner opens with compact closures (exists_inner_opens_of_isCompact_closure; the space is locally compact Hausdorff);
• the padding to one common dimension n' := max n_V + 1 (Włodarczyk's common ambient dimension [Wlo09, §7.1]; Kollár's freedom to enlarge the affine space of an embedding [Kol07, Theorem 36, proof]), through the interface PadTools, whose fields are the padding constructions of PadIdeal.lean (instantiated in PieceModelPad.lean); the padding is what makes the ideal of a model with k = 0 equations nonzero at every stalk, as PieceEmbedding.isNonzeroEverywhere requires;
• the assembly exists_localEmbeddingData_of_padTools: the pointwise models at the points of the compact closure U, a finite subcover, the shrinking, the padded pieces.

No new mathematics: Hironaka's definition of an analytic space, the local models, and Włodarczyk's padding. Kollár's requirement dim 𝔸 ≥ dim X + 2 on the embedding [Kol07, Corollary 22, proof] is not needed: the argument follows Włodarczyk, whose local models are minimal embeddings into open subsets of ℂⁿ [Wlo09, §4, (3)⇒(4)], with the freedom to use any closed embedding coming from the commutation of the resolution with embeddings of ambient manifolds [Wlo09, §7.1].

theorem Hironaka.Manifold.contMDiff_subtypeVal_comp_iff_of_opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u_3} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_4} [TopologicalSpace N] [ChartedSpace E' N] {m : WithTop ℕ∞} {U : TopologicalSpace.Opens N} (g : M → ↥U) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') m (Subtype.val ∘ g) ↔ ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') m g

Mathlib's ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff for ContMDiff, with the two manifolds in independent universes (contMDiff_subtypeVal_comp_iff' fixes one universe for both; here the opens of Fin n → 𝕜 live in Type and those of Kn 𝕜 n in Type u).

def Hironaka.Manifold.downOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : TopologicalSpace.Opens (Fin n → 𝕜)

An open G' ⊆ Kn 𝕜 n of the universe-lifted model of Kⁿ, read as an open of Fin n → 𝕜.

Equations

• Hironaka.Manifold.downOpens G' = { carrier := ULift.up ⁻¹' ↑G', is_open' := ⋯ }

def Hironaka.Manifold.toLiftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : (pieceAmbient 𝕜 (downOpens G')).carrier → ↥G'

The points of the one-piece ambient of downOpens G' mapped onto G'.

Equations

• Hironaka.Manifold.toLiftOpens G' p = ⟨{ down := ↑p.snd }, ⋯⟩

def Hironaka.Manifold.ofLiftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : ↥G' → (pieceAmbient 𝕜 (downOpens G')).carrier

The inverse of toLiftOpens.

Equations

• Hironaka.Manifold.ofLiftOpens G' y = ⟨PUnit.unit, ⟨(↑y).down, ⋯⟩⟩

theorem Hironaka.Manifold.contMDiff_toLiftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (AnalyticSpace.Kn 𝕜 n)) ⊤ (toLiftOpens G')

toLiftOpens is analytic (ContMDiff.sigmaDesc on the one-point Σ, and the lifted coordinates).

theorem Hironaka.Manifold.contMDiff_ofLiftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : ContMDiff (modelWithCornersSelf 𝕜 (AnalyticSpace.Kn 𝕜 n)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (ofLiftOpens G')

ofLiftOpens is analytic (contMDiff_sigmaMk_comp_iff).

noncomputable def Hironaka.Manifold.pieceAmbientLiftIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : (AnalyticSpace.KLocallyRingedSpace.ofManifold 𝕜 (Fin n → 𝕜) (pieceAmbient 𝕜 (downOpens G')).carrier).KIso (AnalyticSpace.KLocallyRingedSpace.ofManifold 𝕜 (AnalyticSpace.Kn 𝕜 n) ↥G')

Sp(pieceAmbient (downOpens G')) ≅ Sp(G'): the one-piece ambient is the open itself, as 𝕜-local-ringed spaces.

Equations

• Hironaka.Manifold.pieceAmbientLiftIso G' = AnalyticSpace.KLocallyRingedSpace.ofManifoldIso (Hironaka.Manifold.toLiftOpens G') (Hironaka.Manifold.ofLiftOpens G') ⋯ ⋯ ⋯ ⋯

noncomputable def Hironaka.Manifold.modelBridge {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : (AnalyticSpace.analyticSpaceOfOpen 𝕜 n G').KIso (AnalyticSpace.toSpace (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (pieceAmbient 𝕜 (downOpens G'))).toKLocallyRingedSpace

The bridge from the model open (G', 𝒜_{G'}) of Hironaka's local analytic spaces [Hir64, Ch. 0, §1, p. 119] to the space of the one-piece ambient manifold of downOpens G' (ofManifold_restrictOpen_iso).

Equations

• Hironaka.Manifold.modelBridge G' = AnalyticSpace.KLocallyRingedSpace.ofManifold_restrictOpen_iso G' ≪≫ CategoryTheory.Iso.symm (Hironaka.Manifold.pieceAmbientLiftIso G')

The model ideal transported to the one-piece ambient

noncomputable def Hironaka.Manifold.modelPieceIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 n G') : (pieceAmbient 𝕜 (downOpens G')).IdealSheaf

The ideal 𝓘 = (f₁, …, f_k) of a local model (S(𝓘), 𝒜_{G'}/𝓘) Hir64, Ch. 0, §1, p. 119, transported along the bridge to an ideal sheaf on the one-piece ambient manifold (transportIdeal).

Equations

• Hironaka.Manifold.modelPieceIdeal G' f = AnalyticSpace.KLocallyRingedSpace.transportIdeal (CategoryTheory.Iso.symm (Hironaka.Manifold.modelBridge G')) (AnalyticSpace.modelIdeal 𝕜 n G' f)

noncomputable def Hironaka.Manifold.modelPieceIdealIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 n G') : (modelPieceIdeal G' f).toAnalyticSpace.KIso (AnalyticSpace.localModel 𝕜 n G' f)

Sp(A)/𝓘 ≅ (S(𝓘), 𝒜_{G'}/𝓘) (quotient_kIso): the closed subspace of the one-piece ambient cut out by the transported ideal is the local model.

Equations

• Hironaka.Manifold.modelPieceIdealIso G' f = AnalyticSpace.KLocallyRingedSpace.quotient_kIso (CategoryTheory.Iso.symm (Hironaka.Manifold.modelBridge G')) (AnalyticSpace.modelIdeal 𝕜 n G' f)

def Hironaka.Manifold.analyticIsoOfKIso {𝕜 : Type} [RCLike 𝕜] {A B : AnalyticSpace 𝕜} (e : A.KIso B.toKLocallyRingedSpace) : A ≅ B

A K-isomorphism of the underlying K-local-ringed spaces, as an isomorphism of analytic K-spaces (the category's morphisms are those K-morphisms).

Equations

• Hironaka.Manifold.analyticIsoOfKIso e = { hom := e.hom, inv := e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def Hironaka.Manifold.modelPieceEmbIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 n G') (e : (X.restrictOpen V).KIso (AnalyticSpace.localModel 𝕜 n G' f)) : X.restrictSet ↑V ≅ (modelPieceIdeal G' f).toAnalyticSpace

The model isomorphism X|_V ≅ Sp(A)/𝓘 of a piece, from the local model isomorphism X|_V ≅ (S(𝓘), 𝒜/𝓘) of exists_kIso_localModel [Hir64, Ch. 0, §1, pp. 119–120], as an isomorphism of analytic spaces.

Equations

• Hironaka.Manifold.modelPieceEmbIso G' f e = CategoryTheory.eqToIso ⋯ ≪≫ Hironaka.Manifold.analyticIsoOfKIso (e ≪≫ CategoryTheory.Iso.symm (Hironaka.Manifold.modelPieceIdealIso G' f))

noncomputable def Hironaka.Manifold.modelPieceEmb {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 n G') (e : (X.restrictOpen V).KIso (AnalyticSpace.localModel 𝕜 n G' f)) : X.restrictSet ↑V ⟶ (modelPieceIdeal G' f).toAnalyticSpace

The model isomorphism as the emb field of a PieceEmbedding.

Equations

• Hironaka.Manifold.modelPieceEmb G' f e = (Hironaka.Manifold.modelPieceEmbIso G' f e).hom

theorem Hironaka.Manifold.modelPieceEmb_isIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 n G') (e : (X.restrictOpen V).KIso (AnalyticSpace.localModel 𝕜 n G' f)) : CategoryTheory.IsIso (modelPieceEmb G' f e)

The emb_isIso field of the PieceEmbedding built from a local model.

theorem Hironaka.Manifold.isReduced_modelPieceIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} (hX : X.IsReduced) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 n G') (e : (X.restrictOpen V).KIso (AnalyticSpace.localModel 𝕜 n G' f)) : (modelPieceIdeal G' f).IsReduced

On a reduced space the transported model ideal is reduced: its closed subspace is X|_V, whose stalks are reduced (ClosedSubspace.isReduced_iff, isReduced_stalk_of_kIso, isReduced_stalk_restrictOpen_iff; a space is reduced when its local rings have no nilpotent elements, [Hir64, Introduction]).

The shrinking of a finite cover

theorem Hironaka.Manifold.exists_inner_opens_of_isCompact_closure {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] {U : Set X} (hU : IsCompact (closure U)) {ι : Type u_2} [Finite ι] (V : ι → Set X) (hV : ∀ (i : ι), IsOpen (V i)) (hcov : closure U ⊆ ⋃ (i : ι), V i) : ∃ (W : ι → Set X), (∀ (i : ι), IsOpen (W i)) ∧ (∀ (i : ι), IsCompact (closure (W i))) ∧ (∀ (i : ι), closure (W i) ⊆ V i) ∧ U ⊆ ⋃ (i : ι), W i

Shrinking a finite open cover of a relatively compact set to inner opens with compact closures inside the cover's members, still covering the set (Mathlib's IsCompact.finite_compact_cover followed by exists_open_between_and_isCompact_closure; the space is locally compact Hausdorff). These are the inner opens V_i ⊆ W_i ⊆ U_i with compact closures of [Wlo09, §4, (3)⇒(4)].

The assembly: local embedding data from the local models, padded

structure Hironaka.Manifold.PadTools (𝕜 : Type) [RCLike 𝕜] : Type u

The padding tools the existence proof uses, as an interface: for m ≤ n' the padded ambient G × 𝕜^{n'-m} and the padded ideal 𝓘 + (z_{m+1}, …, z_{n'}), the transport of reducedness, the nonvanishing at every stalk for m < n', and the slice isomorphism of closed subspaces Sp/𝓘_pad ≅ Sp/𝓘 (Włodarczyk's passage to a common ambient dimension [Wlo09, §7.1]). The fields are the constructions of PadIdeal.lean, instantiated in PieceModelPad.lean.

• padOpens {m n' : ℕ} : m ≤ n' → TopologicalSpace.Opens (Fin m → 𝕜) → TopologicalSpace.Opens (Fin n' → 𝕜)
• padIdeal {m n' : ℕ} (h : m ≤ n') {G : TopologicalSpace.Opens (Fin m → 𝕜)} : (pieceAmbient 𝕜 G).IdealSheaf → (pieceAmbient 𝕜 (self.padOpens h G)).IdealSheaf
• isReduced {m n' : ℕ} (h : m ≤ n') {G : TopologicalSpace.Opens (Fin m → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : J.IsReduced → (self.padIdeal h J).IsReduced
• isNonzeroEverywhere {m n' : ℕ} (h : m ≤ n') : m < n' → ∀ {G : TopologicalSpace.Opens (Fin m → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf), Manifold.IdealSheaf.IsNonzeroEverywhere (self.padIdeal h J)
• iso {m n' : ℕ} (h : m ≤ n') {G : TopologicalSpace.Opens (Fin m → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : (self.padIdeal h J).toAnalyticSpace ≅ J.toAnalyticSpace

noncomputable def Hironaka.Manifold.pieceOfModel {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} (T : PadTools 𝕜) {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {m : ℕ} (G' : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 m)) {k : ℕ} (f : Fin k → AnalyticSpace.AnalyticFun 𝕜 m G') (e : (X.restrictOpen V).KIso (AnalyticSpace.localModel 𝕜 m G' f)) (hX : X.IsReduced) {n' : ℕ} (h : m < n') : PieceEmbedding 𝕜 n' X ↑V

The PieceEmbedding of a local model of X|_V in K^m, padded to the common dimension n' > m by z ↦ (z, 0) with the equations z_{m+1}, …, z_{n'} added [Wlo09, §7.1]; the padding supplies the nonvanishing of the ideal at every stalk.

Equations

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

theorem Hironaka.Manifold.exists_localEmbeddingData_of_padTools {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} (T : PadTools 𝕜) (hX : X.IsReduced) (U : Set ↑↑X.toPresheafedSpace) (hUc : IsCompact (closure U)) : Nonempty (LocalEmbeddingData 𝕜 X U)

Given the padding tools, every relatively compact open U of a reduced analytic space has local embedding data: finitely many pieces (the local models [Hir64, Ch. 0, §1, pp. 119–120] at the points of the compact closure U), inner opens with compact closures covering U, and one common dimension n' := max n_V + 1 (the local embeddings of [Wlo09, §4, (3)⇒(4)] and [Kol07, Corollary 22, proof], padded as in [Wlo09, §7.1]).