The embedded desingularization and closed embeddings of ambient manifolds, on the model

The push-forward relation of [Wlo09, Theorem 2.0.2 (4)], "commutes with … embeddings of ambient varieties", for the embedded desingularization embeddedDesingFam on the standard models: for a closed embedding τ : N → M of manifolds modelled on 𝕜^{n−s} and 𝕜ⁿ whose image is a closed submanifold of codimension s, identified with the bundled submanifold by e over τ, a reduced 𝓘_Y on M containing the ideal sheaf of τ(N) and J = τ^* 𝓘_Y with nonzero stalks, the succession of the family of Y ⊆ M over U_K is the push-forward along τ of the succession of the family of Y ⊆ N over U_{K'} whenever τ(U_{K'}) ⊆ U_K (isPushforwardUpToEmptyAlong_embeddedDesingFam; the gluing is isPushforwardUpToEmptyAlong_toExtensionCompatibleFamily_of_dom of Hironaka/Resolution/Analytic/Wlo09/FamilyPushforward.lean, from the per-open commutation of the concrete functor, BEDanFamStar.closedEmbedding).

The families of the theorem are those of the ideal sheaves made the unit ideal on the connected components where they vanish (unitOnZeroStalks). Since J has nonzero stalks, 𝓘_Y has nonzero stalks along τ(N), so the modified ideal sheaf pulls back along τ to J (unitOnZeroStalks_pullback_eq) and J is unchanged (unitOnZeroStalks_eq_self); the modified ideal sheaf still contains the ideal sheaf of τ(N) (le_unitOnZeroStalks). The class of the functor is the reduced ideal sheaves with nonzero stalks, and the pull-back to a closed submanifold of a reduced ideal sheaf containing its ideal sheaf is reduced (isReduced_pullback_inclusionMap: the germ map of the inclusion is surjective with kernel the stalk of the submanifold's ideal sheaf, and the image of a radical ideal containing the kernel is radical); so J is reduced (isReduced_pullback_of_diffeomorph_toAnalyticManifold).

The variants for a nonempty N on any 𝕜^m (…_of_diffeomorph, the identification e forcing m = n − s) and for an empty N on any model (…_of_isEmpty) are the forms the assignment on arbitrary models uses (Hironaka/Resolution/Analytic/Wlo09/EmbeddedDesingularization.lean).

Ideal sheaves made the unit ideal on their zero components, along maps

theorem AnalyticManifold.IdealSheaf.le_unitOnZeroStalks {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) : I ≤ I.unitOnZeroStalks

An ideal sheaf lies in itself made the unit ideal on its zero components.

theorem AnalyticManifold.IdealSheaf.unitOnZeroStalks_eq_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : I.unitOnZeroStalks = I

An ideal sheaf with nonzero stalks is unchanged by making it the unit ideal on its zero components.

theorem AnalyticManifold.IdealSheaf.unitOnZeroStalks_pullback_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : AnalyticManifold 𝕜 E'} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (h : (Manifold.IdealSheaf.pullback ⇑τ ⋯ I).IsNonzeroEverywhere) : Manifold.IdealSheaf.pullback ⇑τ ⋯ I.unitOnZeroStalks = Manifold.IdealSheaf.pullback ⇑τ ⋯ I

The pull-back along τ of an ideal sheaf made the unit ideal on its zero components is the pull-back of the ideal sheaf, when the latter has nonzero stalks: the stalks of the ideal sheaf at the image points are nonzero.

theorem AnalyticManifold.IdealSheaf.isReduced_pullback_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S s) (hI : I.IsReduced) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) : IsReduced (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I)

The pull-back to a closed submanifold of a reduced ideal sheaf containing the submanifold's ideal sheaf is reduced: the germ map of the inclusion is surjective (germMap_inclusionMap_surjective) with kernel the stalk of the submanifold's ideal sheaf (ker_germMap_inclusionMap'), and the image under a surjection of a radical ideal containing the kernel is radical (Ideal.map_radical_of_surjective).

The reducedness of the pull-back along a closed embedding

theorem Hironaka.Manifold.isReduced_pullback_of_diffeomorph_toAnalyticManifold {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) {s : ℕ} {N : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) : AnalyticManifold.IdealSheaf.IsReduced (Manifold.IdealSheaf.pullback ⇑τ ⋯ I)

The pull-back along τ of a reduced ideal sheaf containing the ideal sheaf of τ(N) is reduced, for N identified with the bundled submanifold τ(N) by e over τ: it is the pull-back along e of the reduced pull-back to the bundled submanifold (isReduced_pullback_inclusionMap).

theorem Hironaka.Manifold.isReduced_pullback_of_diffeomorph_toAnalyticManifold' {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) {m s : ℕ} {N : AnalyticManifold 𝕜 (Fin m → 𝕜)} [Nonempty N.carrier] (τ : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) : AnalyticManifold.IdealSheaf.IsReduced (Manifold.IdealSheaf.pullback ⇑τ ⋯ I)

isReduced_pullback_of_diffeomorph_toAnalyticManifold for a nonempty N modelled on any 𝕜^m (dim_eq_of_diffeomorph).

The push-forward relation on the standard models

theorem Hironaka.Manifold.isPushforwardUpToEmptyAlong_embeddedDesingFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) {s : ℕ} {N : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (J : N.IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) (hJI : J = Manifold.IdealSheaf.pullback ⇑τ ⋯ I) (hJr : J.IsReduced) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) (hK : ⇑τ '' ↑((embeddedDesingFam N J hJr).nhd K') ⊆ ↑((embeddedDesingFam M I hI).nhd K)) : ((embeddedDesingFam M I hI).seq K).IsPushforwardUpToEmptyAlong ((embeddedDesingFam N J hJr).seq K') τ

The embedded desingularization on the standard models commutes with closed embeddings, over every pair of compacts ([Wlo09, Theorem 2.0.2 (4)], "embeddings of ambient varieties", read as [Kol07, 34.3]): for a closed embedding τ : N → M with image a closed submanifold of codimension s, identified with the bundled submanifold by e over τ, a reduced 𝓘_Y containing the ideal sheaf of τ(N) and J = τ^* 𝓘_Y with nonzero stalks, the succession of the family of Y ⊆ M over U_K is the push-forward along τ of that of Y ⊆ N over U_{K'}, up to blow-ups whose centres lie outside the part over τ(U_{K'}), whenever τ(U_{K'}) ⊆ U_K. The families are those of the ideal sheaves made the unit ideal on their zero components, which J is already and which pull back to each other along τ; the gluing is isPushforwardUpToEmptyAlong_toExtensionCompatibleFamily_of_dom from the per-open commutation BEDanFamStar.closedEmbedding of the concrete functor.

theorem Hironaka.Manifold.isPushforwardUpToEmptyAlong_embeddedDesingFam_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) {m s : ℕ} {N : AnalyticManifold 𝕜 (Fin m → 𝕜)} [Nonempty N.carrier] (τ : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (J : N.IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) (hJI : J = Manifold.IdealSheaf.pullback ⇑τ ⋯ I) (hJr : J.IsReduced) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) (hK : ⇑τ '' ↑((embeddedDesingFam N J hJr).nhd K') ⊆ ↑((embeddedDesingFam M I hI).nhd K)) : ((embeddedDesingFam M I hI).seq K).IsPushforwardUpToEmptyAlong ((embeddedDesingFam N J hJr).seq K') τ

isPushforwardUpToEmptyAlong_embeddedDesingFam for a nonempty N modelled on any 𝕜^m: the identification e of N with the bundled submanifold of codimension s forces m = n − s (dim_eq_of_diffeomorph).

theorem Hironaka.Manifold.isPushforwardUpToEmptyAlong_embeddedDesingFam_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : I.IsReduced) {s : ℕ} {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [FiniteDimensional 𝕜 E'] {N : AnalyticManifold 𝕜 E'} [IsEmpty N.carrier] (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (F : N.ExtensionCompatibleFamily) (hF : ∀ (K' : TopologicalSpace.Compacts N.carrier), (F.seq K').NoEmptyCenters) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) : ((embeddedDesingFam M I hI).seq K).IsPushforwardUpToEmptyAlong (F.seq K') τ

isPushforwardUpToEmptyAlong_embeddedDesingFam for an empty N modelled on any space: both successions are empty (isPushforwardUpToEmptyAlong_seqOn_of_isEmpty_of_dom).