The closed subspace along an analytic map, and the restriction of an isomorphism

The independence of the local resolution of a piece from its embedding [Kol07, Theorem 36, proof] compares two local resolutions as analytic 𝕜-spaces: each is the closed subspace of the last stage of a blow-up sequence cut out by the final ideal-theoretic strict transform (IdealSheaf.toAnalyticSpace, the closed subspace of Sp of a manifold), and the comparison is a chain of isomorphisms of closed subspaces, each induced by an identity of ideal sheaves along a manifold map — the functoriality of the germ quotient (quotientMap) along Sp(f). This module provides that layer:

• IdealSheaf.homOfPullbackEq (PieceIndependence.lean, with the compatibility compat_ofManifoldHom_of_eq): the morphism of closed subspaces over Sp(f) when J' = f^* J, for ANY analytic map f between standard-model manifolds (two models allowed) — the generalisation of padSliceHom (PadIdeal.lean), with restrictedIdealHom its instance at an open inclusion; on points it is f (toFun_homOfPullbackEq_val), it lies over Sp(f) (homOfPullbackEq_comp_toAnalyticSpaceι), and along a DIFFEOMORPHISM it is an isomorphism (isIso_homOfPullbackEq_of_diffeomorph: the base map is a homeomorphism of cosupports and the fibre maps are bijective, the mechanism of isIso_padSliceHom — Mathlib's LocallyRingedSpace.IsOpenImmersion.of_stalk_iso and to_iso).
• isIso_homOfPullbackEq_inclusionMap: the weak commutation with closed embeddings, j^* B(X, I_X) = B(Y, I_Y) [Kol07, 34.4], read on the closed subspaces — along a closed embedding S ↪ M with 𝓘_S ≤ J, the closed subspace of S cut out by J|_S IS the closed subspace of M cut out by J: the cosupport of J lies in S, and the stalk maps are onto with kernel 𝓘_{S,p} ≤ J_p (bijective_fiberMap_homOfPullbackEq_inclusionMap). Used at the last stage of the push-forward chain of a padded embedding.
• PieceEmbedding.embInv: the inverse Sp(G)/𝓘_Y ≅ X|V of a piece embedding, named (localResolutionToPiece inlines it, localResolutionToPiece_eq).
• QuotientSpace.compat_comp, KLocallyRingedSpace.quotientMap_comp: the functoriality of the germ quotient is functorial (Hom.ext_of_comp_quotientι, quotientMap_comp_quotientι).
• AnalyticSpace.exists_restrictSet_isIso_of_comp_eq: an isomorphism over Z restricts, for every N ⊆ Z, to an isomorphism of the restrictions (restrictSet, Hom.restrictSet) over N, compatible with the restricted projections: isoOfRangeEq of the two open immersions into B (the ranges agree because an isomorphism is a homeomorphism, in both branches of the openOf convention), and the composite by the uniqueness of lifts through the open immersion Z|N → Z (Hom.ext_of_comp_ofRestrict). The conclusion is the shape in which the independence of the local resolution is stated (localResolution_independent_local).

Closed subspaces and restrictions of analytic spaces are those of [Hir64, Ch. 0, §1, pp. 119–120]. Not in the sources; bookkeeping on quotientMap, ofManifoldHom and restrictSet.

Functoriality of the germ-family quotient

theorem AnalyticSpace.QuotientSpace.compat_comp {X'' X' X : AlgebraicGeometry.LocallyRingedSpace} (φ' : X'' ⟶ X') (φ : X' ⟶ X) (J'' : Manifold.IdealSheaf X''.𝒪) (J' : Manifold.IdealSheaf X'.𝒪) (J : Manifold.IdealSheaf X.𝒪) (h' : Compat φ' J'' J') (h : Compat φ J' J) : Compat (CategoryTheory.CategoryStruct.comp φ' φ) J'' J

Compatibility composes: if φ' carries 𝒥' into 𝒥'' and φ carries 𝒥 into 𝒥', the composite carries 𝒥 into 𝒥'' (the stalk map of a composite is the composite of the stalk maps).

theorem AnalyticSpace.KLocallyRingedSpace.quotientMap_comp {K : Type} [RCLike K] {X'' X' X : KLocallyRingedSpace K} (ψ' : X'' ⟶ X') (ψ : X' ⟶ X) (J'' : Manifold.IdealSheaf X''.𝒪) (J' : Manifold.IdealSheaf X'.𝒪) (J : Manifold.IdealSheaf X.𝒪) (h' : QuotientSpace.Compat (↑ψ') J'' J') (h : QuotientSpace.Compat (↑ψ) J' J) (h'' : QuotientSpace.Compat (↑(CategoryTheory.CategoryStruct.comp ψ' ψ)) J'' J) : CategoryTheory.CategoryStruct.comp (quotientMap ψ' J'' J' h') (quotientMap ψ J' J h) = quotientMap (CategoryTheory.CategoryStruct.comp ψ' ψ) J'' J h''

The functoriality of the closed subspace is functorial: the induced morphisms compose (Hom.ext_of_comp_quotientι and quotientMap_comp_quotientι).

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

theorem Hironaka.Manifold.toFun_homOfPullbackEq_val {𝕜 : 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' = Manifold.IdealSheaf.pullback f hf J) (z : ↑↑J'.toAnalyticSpace.toPresheafedSpace) : ↑(↑(Manifold.IdealSheaf.homOfPullbackEq f hf h) z) = f ↑z

On points the morphism of closed subspaces is f.

theorem Hironaka.Manifold.homOfPullbackEq_comp_toAnalyticSpaceι {𝕜 : 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' = Manifold.IdealSheaf.pullback f hf J) : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq f hf h) J.toAnalyticSpaceι = CategoryTheory.CategoryStruct.comp J'.toAnalyticSpaceι (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom f hf; this)

The morphism of closed subspaces lies over Sp(f): ι_J ∘ homOfPullbackEq = Sp(f) ∘ ι_{J'} (quotientMap_comp_quotientι).

theorem Hironaka.Manifold.stalkMap_ofManifoldHom_hom {𝕜 : 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) (x : A'.carrier) : CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(AnalyticSpace.KLocallyRingedSpace.ofManifoldHom f hf)) x) = Manifold.germMap f hf x

The stalk map of Sp(f) is the germ map (stalkMap_ofManifoldHom_eq_germMap, bundled).

theorem Hironaka.Manifold.cosupport_pullback_of_bijective {𝕜 : 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} (hbij : ∀ (z : A'.carrier), Function.Bijective ⇑(Manifold.germMap f hf z)) : (Manifold.IdealSheaf.pullback f hf J).support = f ⁻¹' Manifold.IdealSheaf.support J

The cosupport of a pull-back along a map whose germ maps are bijective is the preimage of the cosupport (Ideal.comap_map_of_bijective).

theorem Hironaka.Manifold.isIso_homOfPullbackEq_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {k n : ℕ} {A : AnalyticManifold 𝕜 (Fin k → 𝕜)} {A' : AnalyticManifold 𝕜 (Fin n → 𝕜)} {J' : A'.IdealSheaf} {J : A.IdealSheaf} (g : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) A'.carrier A.carrier ⊤) (h : J' = Manifold.IdealSheaf.pullback ⇑g ⋯ J) : CategoryTheory.IsIso (Manifold.IdealSheaf.homOfPullbackEq ⇑g ⋯ h)

Along a diffeomorphism (any two standard models) the morphism of closed subspaces is an isomorphism: the base map is the homeomorphism of cosupports induced by g, the fibre maps are bijective because the germ maps of g are ring isomorphisms (germMap_bijective_of_diffeomorph), so it is an open immersion onto the whole target (the mechanism of isIso_padSliceHom).

The closed subspace along a closed embedding

theorem Hironaka.Manifold.ker_germMap_inclusionMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S s) (p : hS.toAnalyticManifold.carrier) : RingHom.ker (Manifold.germMap ⇑hS.inclusionMap ⋯ p) = hS.idealSheaf.stalkIdeal (hS.inclusionMap p)

The kernel of the germ map of the inclusion of a closed submanifold at p is the stalk of 𝓘_S at p (restrictStalk, stalkIdeal_idealSheaf_of_mem).

theorem Hironaka.Manifold.cosupport_subset_of_idealSheaf_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S s) {J : M.IdealSheaf} (hle : hS.idealSheaf ≤ J) : Manifold.IdealSheaf.support J ⊆ S

With 𝓘_S ≤ J, the cosupport of J lies in S (off S the stalk of 𝓘_S is the unit ideal).

theorem Hironaka.Manifold.cosupport_pullback_inclusionMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S s) {J : M.IdealSheaf} (hle : hS.idealSheaf ≤ J) : (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J).support = ⇑hS.inclusionMap ⁻¹' Manifold.IdealSheaf.support J

With 𝓘_S ≤ J, the cosupport of J|_S is the preimage of the cosupport of J (the germ maps of the inclusion are onto with kernel 𝓘_{S,p} ≤ J_p).

theorem Hironaka.Manifold.bijective_fiberMap_homOfPullbackEq_inclusionMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S s) {J : M.IdealSheaf} (hle : hS.idealSheaf ≤ J) (z : ↑(AnalyticSpace.QuotientSpace.support (AnalyticSpace.KLocallyRingedSpace.ofManifold 𝕜 (Fin (n - s) → 𝕜) hS.toAnalyticManifold.carrier).toLocallyRingedSpace (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J))) : Function.Bijective ⇑(AnalyticSpace.QuotientSpace.fiberMap (↑(AnalyticSpace.KLocallyRingedSpace.ofManifoldHom ⇑hS.inclusionMap ⋯)) (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) J ⋯ z)

With 𝓘_S ≤ J, the fibre maps of the closed-subspace morphism along the inclusion are bijective: the germ maps of the inclusion are onto with kernel 𝓘_{S,p} ≤ J_p.

theorem Hironaka.Manifold.isIso_homOfPullbackEq_inclusionMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) S s) {J : M.IdealSheaf} (hle : hS.idealSheaf ≤ J) {J_S : hS.toAnalyticManifold.IdealSheaf} (h : J_S = Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) : CategoryTheory.IsIso (Manifold.IdealSheaf.homOfPullbackEq ⇑hS.inclusionMap ⋯ h)

Along a closed embedding S ↪ M with 𝓘_S ≤ J, the closed subspace of S cut out by J|_S is the closed subspace of M cut out by J: the morphism of closed subspaces over Sp(S ↪ M) is an isomorphism (the cosupport of J lies in S, the fibre maps are bijective). The weak commutation with closed embeddings j^* B(X, I_X) = B(Y, I_Y) [Kol07, 34.4], read on the subspaces; used at the last stage of the push-forward chain of a padded embedding (idealSheaf_range_pushforwardIncl_le_strictTransformSubspaceSeq).

The inverse of a piece embedding, named

noncomputable def Hironaka.Manifold.PieceEmbedding.embInv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : E.ideal.toAnalyticSpace ⟶ X.restrictSet V

The inverse Sp(G)/𝓘_Y ≅ X|V of the piece embedding, named (localResolutionToPiece inlines it as inv E.emb).

Equations

• E.embInv = CategoryTheory.inv E.emb

theorem Hironaka.Manifold.PieceEmbedding.embInv_comp_emb {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : CategoryTheory.CategoryStruct.comp E.emb E.embInv = CategoryTheory.CategoryStruct.id (X.restrictSet V)

embInv ∘ emb = id.

theorem Hironaka.Manifold.PieceEmbedding.emb_comp_embInv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) : CategoryTheory.CategoryStruct.comp E.embInv E.emb = CategoryTheory.CategoryStruct.id E.ideal.toAnalyticSpace

emb ∘ embInv = id.

theorem Hironaka.Manifold.PieceEmbedding.localResolutionToPiece_eq {𝕜 : 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.localResolutionToPiece bed W hW = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (E.localResolutionMap bed W hW) (E.restrictedIdealHom W)) E.embInv

The local resolution map over the piece, through embInv (definitional).

Restriction of an isomorphism over a map to the preimages of a set

theorem AnalyticSpace.Hom.restrictSet_comp_ofRestrict {K : Type} [RCLike K] {X Y : AnalyticSpace K} (f : X ⟶ Y) (V : Set ↑↑Y.toPresheafedSpace) : CategoryTheory.CategoryStruct.comp (restrictSet f V) (Y.ofRestrict (Y.openOf V)) = CategoryTheory.CategoryStruct.comp (X.ofRestrict (X.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' V))) f

The restriction of a morphism lies over it (Hom.restrictSet is the lift through the open immersion, IsOpenImmersion.lift_fac).

theorem AnalyticSpace.KLocallyRingedSpace.exists_restrictSet_isIso_of_comp_eq {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (ψ : A.toKLocallyRingedSpace ⟶ B.toKLocallyRingedSpace) [CategoryTheory.IsIso ψ] (pA : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (pB : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (h : CategoryTheory.CategoryStruct.comp ψ pB = pA) (N : Set ↑↑Z.toPresheafedSpace) : ∃ (ψ' : A.restrictOpen (A.openOf (Hom.toFun pA ⁻¹' N)) ⟶ B.restrictOpen (B.openOf (Hom.toFun pB ⁻¹' N))), CategoryTheory.IsIso ψ' ∧ CategoryTheory.CategoryStruct.comp ψ' (Hom.restrictSet pB N) = Hom.restrictSet pA N

An isomorphism ψ : A ≅ B over Z restricts to an isomorphism of the open restrictions of the convention openOf, compatible with the restricted projections (the K-level form): isoOfRangeEq of the two open immersions into B, whose ranges agree because ψ is a homeomorphism (so Π_A⁻¹N is open iff Π_B⁻¹N is, and the openOf branches agree), and the uniqueness of lifts through Z|N → Z.

theorem AnalyticSpace.exists_restrictSet_isIso_of_comp_eq {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (ψ : A ⟶ B) (hψ : CategoryTheory.IsIso ψ) (pA : A ⟶ Z) (pB : B ⟶ Z) (h : CategoryTheory.CategoryStruct.comp ψ pB = pA) (N : Set ↑↑Z.toPresheafedSpace) : ∃ (ψ' : A.restrictSet (↑pA ⁻¹' N) ⟶ B.restrictSet (↑pB ⁻¹' N)), CategoryTheory.IsIso ψ' ∧ CategoryTheory.CategoryStruct.comp ψ' (Hom.restrictSet pB N) = Hom.restrictSet pA N

An isomorphism ψ : A ≅ B over Z (Π_B ∘ ψ = Π_A) restricts, for every N ⊆ Z, to an isomorphism of the restrictions (restrictSet, Hom.restrictSet) over N, compatible with the restricted projections — the shape in which the independence of the local resolution is stated (localResolution_independent_local); the K-level content is KLocallyRingedSpace.exists_restrictSet_isIso_of_comp_eq.