Padded embeddings, shears, the transport of an embedding along an isomorphism, and the local

resolution map over the piece

Two closed embeddings i₁ : X ↪ 𝕜ⁿ, i₂ : X ↪ 𝕜ᵐ become equivalent under an analytic automorphism of 𝕜ⁿ⁺ᵐ after the coordinate inclusions: extend i₁, i₂ (locally) to j₁, j₂, shear by (x, y) ↦ (x, y + j₂(x)), shear by (x, y) ↦ (x + j₁(y), y), compose [Kol07, Lemma 39]; Włodarczyk's Lemma 4.8.1 is the same statement, with two explicit automorphisms of the doubled affine space [Wlo05, Lemma 4.8.1]. The ambient dimension may be increased at any time by 𝕜ⁿ ↪ 𝕜ⁿ⁺ᵐ [Kol07, Theorem 36, proof], as in Włodarczyk's passage to a common ambient dimension [Wlo09, §7.1]. The algebraic counterparts are shearX, shearY, prodEmb and coordInclFst of Hironaka/Resolution/Algebraic/Kol07/Thm36/AffineSpace.lean. This module constructs the analytic terms:

• The paddings. PieceEmbedding.padAlong E σ pads a piece embedding along an embedding of coordinates σ : Fin n ↪ Fin n' with the tools of PadIdeal.lean: the ambient padOpens σ E.G, the ideal padIdeal σ E.ideal, the embedding X|V ≅ Sp(G)/𝓘 ≅ Sp(padOpens σ G)/padIdeal σ 𝓘 (the slice isomorphism inverted). padLeft E m (σ := Fin.castAddEmb m, the coordinate inclusion x ↦ (x, 0)) and padRight E m (σ := Fin.natAddEmb m, y ↦ (0, y)) are the two paddings of Lemma 39. isNonzeroEverywhere_padIdeal_of_isNonzeroEverywhere is the nonvanishing of the padded ideal for an ARBITRARY σ (the padding of a nonzero ideal is nonzero, no padding coordinate needed), so that the paddings are total in m.
• The shears. shearSnd O j hj, shearFst O j hj: the analytic automorphisms (x, y) ↦ (x, y + j(x)) of O × 𝕜ᵐ and (x, y) ↦ (x + j(y), y) of 𝕜ⁿ × O, for j analytic on the open O — Mathlib's PartialDiffeomorph of the model space 𝕜ⁿ⁺ᵐ with source and target the cylinder over O (the two automorphisms of [Kol07, Lemma 39, proof]; the local extensions j₁, j₂ are supplied where the two embeddings are compared, from the sheaf of germ families).
• The transport. PieceEmbedding.transportAlongIso E h hh: a piece embedding of Y|U composed with an isomorphism X|V ≅ Y|U is a piece embedding of X|V with the SAME ambient and ideal — the analytic form, for an isomorphism of open subspaces, of the compatible embeddings of [Kol07, Lemma 41] (the projection argument of that lemma is not needed).
• The composite. PieceEmbedding.localResolutionToPiece E bed W hW: the local resolution map Π : Ỹ → Sp(W)/𝓘|W (PieceResolution.lean) followed by the restriction-of-a-quotient map Sp(W)/𝓘|W → Sp(G)/𝓘 (the functoriality of the closed subspace along Sp(W ↪ G)) and the inverse of the embedding X|V ≅ Sp(G)/𝓘 — the map Ỹ_Z → Y_Z of Włodarczyk's canonical desingularization [Wlo09, §4, (3)⇒(4)], landing in the piece X|V, with image the open embPreimage E W of the points of X|V whose ambient point lies over W (ambientPoint).

Conventions: the one-piece ambient pieceAmbient 𝕜 G; the linear chart of 𝕜ⁿ is the identity (ContinuousLinearEquiv.refl). The map localResolutionToPiece lands in the piece itself rather than in the open subspace X | embPreimage E W, so that its compositions with the transitions between pieces take place in one space; the open subspace is reached by restricting along the open set embPreimage E W (Hom.restrictSet). Not in the sources beyond the items cited; bookkeeping.

The padding of a nonzero ideal is nonzero, for every σ

theorem Hironaka.Manifold.isNonzeroEverywhere_padIdeal_of_isNonzeroEverywhere {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) : Manifold.IdealSheaf.IsNonzeroEverywhere (padIdeal σ J)

The padding of an ideal nonzero at every stalk is nonzero at every stalk, for every embedding of coordinates σ — off the slice the padded ideal is the unit ideal, on the slice (p^*J + 𝓘_S)_{s w} = (s^*)⁻¹ J_w contains p^* J_w, and s^* ∘ p^* = id.

The shears (x, y) ↦ (x, y + j x) and (x, y) ↦ (x + j y, y)

theorem Hironaka.Manifold.contDiff_append_zero_left {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} : ContDiff 𝕜 ⊤ fun (b : Fin m → 𝕜) => Fin.append 0 b

The block inclusion b ↦ (0, b) of 𝕜ᵐ into 𝕜ⁿ⁺ᵐ is analytic.

theorem Hironaka.Manifold.contDiff_append_zero_right {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} : ContDiff 𝕜 ⊤ fun (a : Fin n → 𝕜) => Fin.append a 0

The block inclusion a ↦ (a, 0) of 𝕜ⁿ into 𝕜ⁿ⁺ᵐ is analytic.

theorem Hironaka.Manifold.contDiff_comp_castAdd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} : ContDiff 𝕜 ⊤ fun (z : Fin (n + m) → 𝕜) => z ∘ Fin.castAdd m

The projection z ↦ z ∘ castAdd m onto the first block is analytic.

theorem Hironaka.Manifold.contDiff_comp_natAdd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} : ContDiff 𝕜 ⊤ fun (z : Fin (n + m) → 𝕜) => z ∘ Fin.natAdd n

The projection z ↦ z ∘ natAdd n onto the second block is analytic.

theorem Hironaka.Manifold.append_zero_left_comp_castAdd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (b : Fin m → 𝕜) : Fin.append 0 b ∘ Fin.castAdd m = 0

The first block of (0, b) is 0.

theorem Hironaka.Manifold.append_zero_right_comp_natAdd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (a : Fin n → 𝕜) : Fin.append a 0 ∘ Fin.natAdd n = 0

The second block of (a, 0) is 0.

def Hironaka.Manifold.shearSnd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O : TopologicalSpace.Opens (Fin n → 𝕜)) (j : (Fin n → 𝕜) → Fin m → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (Fin (n + m) → 𝕜) (Fin (n + m) → 𝕜) ⊤

The shear (x, y) ↦ (x, y + j(x)), an analytic automorphism of the cylinder O × 𝕜ᵐ ⊆ 𝕜ⁿ⁺ᵐ over an open O ⊆ 𝕜ⁿ on which j is analytic; its inverse is the shear by −j. It carries the coordinate inclusion x ↦ (x, 0) to the graph x ↦ (x, j(x)): the first automorphism of [Kol07, Lemma 39, proof] (compare the automorphisms of [Wlo05, Lemma 4.8.1]).

Equations

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

def Hironaka.Manifold.shearFst {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O : TopologicalSpace.Opens (Fin m → 𝕜)) (j : (Fin m → 𝕜) → Fin n → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (Fin (n + m) → 𝕜) (Fin (n + m) → 𝕜) ⊤

The shear (x, y) ↦ (x + j(y), y), an analytic automorphism of the cylinder 𝕜ⁿ × O ⊆ 𝕜ⁿ⁺ᵐ over an open O ⊆ 𝕜ᵐ on which j is analytic; its inverse is the shear by −j. It carries the coordinate inclusion y ↦ (0, y) to the graph y ↦ (j(y), y): the second automorphism of [Kol07, Lemma 39, proof] (compare the automorphisms of [Wlo05, Lemma 4.8.1]).

Equations

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

theorem Hironaka.Manifold.shearSnd_apply {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O : TopologicalSpace.Opens (Fin n → 𝕜)) (j : (Fin n → 𝕜) → Fin m → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O) (z : Fin (n + m) → 𝕜) : ↑(shearSnd O j hj).toPartialEquiv z = z + Fin.append 0 (j (z ∘ Fin.castAdd m))

The value of the shear (x, y) ↦ (x, y + j(x)) (rfl).

theorem Hironaka.Manifold.shearFst_apply {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O : TopologicalSpace.Opens (Fin m → 𝕜)) (j : (Fin m → 𝕜) → Fin n → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O) (z : Fin (n + m) → 𝕜) : ↑(shearFst O j hj).toPartialEquiv z = z + Fin.append (j (z ∘ Fin.natAdd n)) 0

The value of the shear (x, y) ↦ (x + j(y), y) (rfl).

The closed subspace along an analytic map with J' = f^* J

theorem Hironaka.Manifold.compat_ofManifoldHom_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (f : M.carrier → N.carrier) (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ⊤ f) {J' : M.IdealSheaf} {J : N.IdealSheaf} (h : J' = Manifold.IdealSheaf.pullback f hf J) : AnalyticSpace.QuotientSpace.Compat (↑(AnalyticSpace.KLocallyRingedSpace.ofManifoldHom f hf)) J' J

The compatibility Compat for Sp(f) when the source ideal IS the pull-back of the target one (comap_ofManifoldHom_eq_pullback, compat_comap). Any two models.

noncomputable def Manifold.IdealSheaf.homOfPullbackEq {𝕜 : Type} [RCLike 𝕜] {k n : ℕ} {A : AnalyticManifold 𝕜 (Fin k → 𝕜)} {A' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (f : A'.carrier → A.carrier) (hf : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ⊤ f) {J' : A'.IdealSheaf} {J : A.IdealSheaf} (h : J' = pullback f hf J) : J'.toAnalyticSpace ⟶ J.toAnalyticSpace

The morphism of closed subspaces over Sp(f) when J' = f^* J: quotientMap along Sp(f), for any analytic map between standard-model manifolds (two models allowed: 𝕜ⁿ → 𝕜ᵏ); restrictedIdealHom is its instance at an open inclusion.

Equations

• Manifold.IdealSheaf.homOfPullbackEq f hf h = AnalyticSpace.KLocallyRingedSpace.quotientMap (AnalyticSpace.KLocallyRingedSpace.ofManifoldHom f hf) J' J ⋯

The padded embeddings

noncomputable def Hironaka.Manifold.PieceEmbedding.padAlong {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {n' : ℕ} (σ : Fin n ↪ Fin n') : PieceEmbedding 𝕜 n' X V

The piece embedding padded along an embedding of coordinates σ : Fin n ↪ Fin n' — the ambient padOpens σ G, the ideal padIdeal σ 𝓘, the embedding X|V ≅ Sp(G)/𝓘 ≅ Sp(padOpens σ G)/padIdeal σ 𝓘 through the slice isomorphism of PadIdeal.lean (the enlargement of the ambient space in [Kol07, Theorem 36, proof]; the common ambient dimension of [Wlo09, §7.1]).

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.padAlong_G {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {n' : ℕ} (σ : Fin n ↪ Fin n') : (E.padAlong σ).G = padOpens σ E.G

The ambient of the padded embedding is the padded open (rfl).

theorem Hironaka.Manifold.PieceEmbedding.padAlong_ideal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {n' : ℕ} (σ : Fin n ↪ Fin n') : (E.padAlong σ).ideal = padIdeal σ E.ideal

The ideal of the padded embedding is the padded ideal (rfl).

noncomputable def Hironaka.Manifold.PieceEmbedding.padLeft {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (m : ℕ) : PieceEmbedding 𝕜 (n + m) X V

The left padding E.padLeft m : PieceEmbedding 𝕜 (n + m) X V — the coordinate inclusion x ↦ (x, 0) after E (the embedding i'_1 of [Kol07, Lemma 39]).

Equations

• E.padLeft m = E.padAlong (Fin.castAddEmb m)

noncomputable def Hironaka.Manifold.PieceEmbedding.padRight {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (m : ℕ) : PieceEmbedding 𝕜 (m + n) X V

The right padding E.padRight m : PieceEmbedding 𝕜 (m + n) X V — the coordinate inclusion y ↦ (0, y) after E (the embedding i'_2 of [Kol07, Lemma 39]).

Equations

• E.padRight m = E.padAlong (Fin.natAddEmb m)

theorem Hironaka.Manifold.PieceEmbedding.padLeft_G {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (m : ℕ) : (E.padLeft m).G = padOpens (Fin.castAddEmb m) E.G

The ambient of the left padding, G × 𝕜ᵐ as padOpens (castAddEmb m) G (rfl).

theorem Hironaka.Manifold.PieceEmbedding.padRight_G {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (m : ℕ) : (E.padRight m).G = padOpens (Fin.natAddEmb m) E.G

The ambient of the right padding, 𝕜ᵐ × G as padOpens (natAddEmb m) G (rfl).

The ambient point of an embedded point, and the points over an open

noncomputable def Hironaka.Manifold.PieceEmbedding.ambientPoint {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : (pieceAmbient 𝕜 E.G).carrier

The ambient point i(y) ∈ G of a point y of the piece X|V: the image of y under the embedding followed by the closed-subspace inclusion Sp(G)/𝓘 → Sp(G).

Equations

• E.ambientPoint y = ↑E.ideal.toAnalyticSpaceι (↑E.emb y)

def Hironaka.Manifold.PieceEmbedding.embPreimage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : Set ↑↑(X.restrictSet V).toPresheafedSpace

The points of the piece over W — the points of X|V whose ambient point lies in the open W ⊆ G, the open subset of the piece over which the local resolution over W lives (the part of the germ Y_Z over W, [Wlo09, §4, (3)⇒(4)]); the image of localResolutionToPiece.

Equations

• E.embPreimage W = {y : ↑↑(X.restrictSet V).toPresheafedSpace | E.ambientPoint y ∈ W}

theorem Hironaka.Manifold.PieceEmbedding.isOpen_embPreimage {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : IsOpen (E.embPreimage W)

The points over W form an open subset of the piece.

The transport of a piece embedding along an isomorphism of open subspaces

noncomputable def Hironaka.Manifold.PieceEmbedding.transportAlongIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {Y : AnalyticSpace 𝕜} {U : Set ↑↑Y.toPresheafedSpace} (E : PieceEmbedding 𝕜 n Y U) (h : X.restrictSet V ⟶ Y.restrictSet U) (hh : CategoryTheory.IsIso h) : PieceEmbedding 𝕜 n X V

The transport of a piece embedding along an isomorphism h : X|V ≅ Y|U: the same ambient G, the same ideal 𝓘, the embedding E.emb ∘ h. The analytic form, for an isomorphism of open subspaces, of the compatible embeddings of [Kol07, Lemma 41]: the ambient and the ideal are unchanged.

Equations

• E.transportAlongIso h hh = { G := E.G, ideal := E.ideal, isNonzeroEverywhere := ⋯, isReduced := ⋯, emb := CategoryTheory.CategoryStruct.comp h E.emb, emb_isIso := ⋯ }

theorem Hironaka.Manifold.PieceEmbedding.transportAlongIso_G {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {Y : AnalyticSpace 𝕜} {U : Set ↑↑Y.toPresheafedSpace} (E : PieceEmbedding 𝕜 n Y U) (h : X.restrictSet V ⟶ Y.restrictSet U) (hh : CategoryTheory.IsIso h) : (E.transportAlongIso h hh).G = E.G

The transport keeps the ambient open (rfl).

theorem Hironaka.Manifold.PieceEmbedding.transportAlongIso_ideal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {Y : AnalyticSpace 𝕜} {U : Set ↑↑Y.toPresheafedSpace} (E : PieceEmbedding 𝕜 n Y U) (h : X.restrictSet V ⟶ Y.restrictSet U) (hh : CategoryTheory.IsIso h) : (E.transportAlongIso h hh).ideal = E.ideal

The transport keeps the ideal sheaf (rfl).

theorem Hironaka.Manifold.PieceEmbedding.transportAlongIso_emb {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {Y : AnalyticSpace 𝕜} {U : Set ↑↑Y.toPresheafedSpace} (E : PieceEmbedding 𝕜 n Y U) (h : X.restrictSet V ⟶ Y.restrictSet U) (hh : CategoryTheory.IsIso h) : (E.transportAlongIso h hh).emb = CategoryTheory.CategoryStruct.comp h E.emb

The transport's embedding is the composite E.emb ∘ h (rfl).

theorem Hironaka.Manifold.PieceEmbedding.ambientPoint_transportAlongIso {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {Y : AnalyticSpace 𝕜} {U : Set ↑↑Y.toPresheafedSpace} (E : PieceEmbedding 𝕜 n Y U) (h : X.restrictSet V ⟶ Y.restrictSet U) (hh : CategoryTheory.IsIso h) (x : ↑↑(X.restrictSet V).toPresheafedSpace) : (E.transportAlongIso h hh).ambientPoint x = E.ambientPoint (↑h x)

The ambient points correspond along h (rfl).

The local resolution map over the piece

noncomputable def Hironaka.Manifold.PieceEmbedding.restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : (E.restrictedIdeal W).toAnalyticSpace ⟶ E.ideal.toAnalyticSpace

The restriction-of-a-quotient map Sp(W)/𝓘|W ⟶ Sp(G)/𝓘 along Sp(W ↪ G): the morphism of closed subspaces homOfPullbackEq at the open inclusion (the ideal 𝓘|W is the pullback of 𝓘 along the inclusion by definition, restrictOpens).

Equations

• E.restrictedIdealHom W = Manifold.IdealSheaf.homOfPullbackEq ⇑((Hironaka.Manifold.pieceAmbient 𝕜 E.G).inclusion W) ⋯ ⋯

noncomputable def Hironaka.Manifold.PieceEmbedding.localResolutionToPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) : E.localResolution bed W hW ⟶ X.restrictSet V

The local resolution map over the piece Ỹ → X|V — the local resolution map Π : Ỹ → Sp(W)/𝓘|W of PieceResolution.lean, followed by the restriction-of-a-quotient map Sp(W)/𝓘|W → Sp(G)/𝓘 and the inverse of the embedding X|V ≅ Sp(G)/𝓘: Włodarczyk's Ỹ_Z → Y_Z [Wlo09, §4, (3)⇒(4)], Kollár's resolution g : g⁻¹(X) → X [Kol07, Corollary 22, proof], which need not be a composite of smooth blow-ups [Kol07, Warning 23]. Its image lies in the open embPreimage E W of the piece (range_localResolutionToPiece_subset; over ℂ it is the closure of the simple points of Y ∩ W, as in the clause range Π = closure X.regularLocus of the resolution theorem — not all of the open over ℝ).

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.toFun_toAnalyticSpaceι_restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (w : ↑↑(E.restrictedIdeal W).toAnalyticSpace.toPresheafedSpace) : ↑E.ideal.toAnalyticSpaceι (↑(E.restrictedIdealHom W) w) = ↑(↑(E.restrictedIdeal W).toAnalyticSpaceι w)

The restriction-of-a-quotient map lies over Sp(W ↪ G): ι ∘ restrictedIdealHom = Sp(val) ∘ ι' on points.

theorem Hironaka.Manifold.PieceEmbedding.range_localResolutionToPiece_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) : Set.range ↑(E.localResolutionToPiece bed W hW) ⊆ E.embPreimage W

The image of the local resolution map over the piece lies in the open embPreimage E W: every point of Ỹ maps to a point of the piece whose ambient point is in W.