The coordinate slice of a padding is the piece: the slice diffeomorphism

Kollár's proof of Theorem 36 passes from an embedding X ↪ 𝔸ⁿ to its padding X ↪ 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ (the embedding i'_1 of [Kol07, Lemma 39]) and back through the weak commutation with closed embeddings [Kol07, 34.4]: the resolution of the padded ideal on the padded ambient is the push-forward of the resolution on the coordinate slice S = {z_j = 0, j ∉ range σ} ([Kol07, Theorem 36, proof]; the common ambient dimension of [Wlo09, §7.1]). On the slice, read as a bundled submanifold with its induced charts (IsClosedSubmanifold.toAnalyticManifold, modelled on 𝕜^{n' − (n' − n)}), the padded ideal restricts to the original ideal: this module proves that identification.

• padExtDiffeomorph σ G: the zero extension padExt corestricted to the slice, as a DIFFEOMORPHISM of the piece onto the bundled slice — across the two models 𝕜ⁿ and 𝕜^{n' − (n' − n)} (IsClosedSubmanifold.contMDiff_codRestrict for the analyticity into the induced charts; inverse the coordinate projection after the inclusion); inclusionMap_padExtDiffeomorph, padExtDiffeomorph_symm_apply its point formulas.
• pullback_padExt_padIdeal: s^*(p^* J + 𝓘_S) = J — the padded ideal pulled back along the zero extension is the ideal (stalkIdeal_padIdeal_padExt with the surjectivity of the germ maps of s, padExtStalk_padCoordProjStalk).
• pullback_inclusionMap_padIdeal: the padded ideal restricted to the slice (the pull-back along the inclusion) is J transported along the inverse of the slice diffeomorphism — both sides pull back along the diffeomorphism to J, and pulling back along a diffeomorphism is injective (IdealSheaf.pullback_symm_pullback).
• idealSheaf_padSlice_le_padIdeal: 𝓘_S ≤ p^* J + 𝓘_S.

Not in the sources; bookkeeping on the padding of PadIdeal.lean and the bundled submanifolds of Bundle.lean.

noncomputable def Hironaka.Manifold.padExtDiffeomorph {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n' - (n' - n)) → 𝕜)) (pieceAmbient 𝕜 G).carrier ⋯.toAnalyticManifold.carrier ⊤

The zero extension as a diffeomorphism of the piece onto the coordinate slice S = {z_j = 0, j ∉ range σ} with its induced structure (IsClosedSubmanifold.toAnalyticManifold, modelled on 𝕜^{n' − (n' − n)}) — ACROSS MODELS (Fin n → 𝕜 against Fin (n' − (n' − n)) → 𝕜); inverse the coordinate projection after the inclusion. The identification of Y with its copy in U × 𝕜ᵐ of [Wlo09, §7.1], and of X ↪ 𝔸ⁿ with X ↪ 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ in [Kol07, Theorem 36, proof].

Equations

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

theorem Hironaka.Manifold.inclusionMap_padExtDiffeomorph {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : ⋯.inclusionMap ((padExtDiffeomorph σ G) w) = padExt σ G w

The slice diffeomorphism followed by the inclusion is the zero extension.

theorem Hironaka.Manifold.padExtDiffeomorph_symm_apply {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (p : ⋯.toAnalyticManifold.carrier) : (padExtDiffeomorph σ G).symm p = padCoordProj σ G (⋯.inclusionMap p)

The inverse of the slice diffeomorphism is the coordinate projection.

theorem Hironaka.Manifold.pullback_padExt_padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (J : (pieceAmbient 𝕜 G).IdealSheaf) : Manifold.IdealSheaf.pullback (padExt σ G) ⋯ (padIdeal σ J) = J

The padded ideal pulled back along the zero extension is the ideal: at w, s^*(p^* J + 𝓘_S)_{s w} = s^* (s^*)⁻¹ J_w = J_w (stalkIdeal_padIdeal_padExt; the germ map of s is onto, p ∘ s = id).

theorem Hironaka.Manifold.pullback_inclusionMap_padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (J : (pieceAmbient 𝕜 G).IdealSheaf) : Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ (padIdeal σ J) = Manifold.IdealSheaf.pullback ⇑(padExtDiffeomorph σ G).symm ⋯ J

The slice ideal is the piece ideal transported: the padded ideal restricted to the slice (the pull-back along the inclusion) is the pull-back of J along the inverse of the slice diffeomorphism. Both sides pull back along padExtDiffeomorph to J (pullback_padExt_padIdeal, IdealSheaf.pullback_symm_pullback), and pulling back along a diffeomorphism is injective.

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

The ideal sheaf of the slice lies in the padded ideal (padIdeal is the sum p^*J + 𝓘_S).