The local resolution over a smaller open, and the relation "isomorphic over N"

Kollár's proof of Theorem 36 compares the local resolutions of a piece for two embeddings NEAR a point [Kol07, Theorem 36, proof]: localResolution_independent_local (LocalResolutionShear.lean) asks for an open N of the piece and an isomorphism of the two local resolutions restricted over N, compatible with the maps to the piece — the relation LocIso N (A, pA) (B, pB) :≡ ∃ ψ : A|pA⁻¹N ≅ B|pB⁻¹N, pB|N ∘ ψ = pA|N (not given a name: the theorems state it in full). This module provides:

• the relation is an equivalence — AnalyticSpace.exists_restrictSet_isIso_trans, exists_restrictSet_isIso_symm — and exists_restrictSet_isIso_of_comp_eq feeds it every global isomorphism over the piece; its open-immersion form exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion (an open immersion A → B over the piece whose range covers pB⁻¹ N restricts to an isomorphism over N; the isoOfRangeEq mechanism with the isomorphism hypothesis weakened to the range condition, for OPEN N — the restriction of a space to a non-open set is by convention the whole space, openOf);
• the morphism homOfPullbackEq of closed subspaces induced by an identity J' = f^* J along an INJECTIVE local analytic isomorphism f is an open immersion with range the points over range f (isOpenImmersion_homOfPullbackEq_of_injective, range_toFun_homOfPullbackEq) — isIso_homOfPullbackEq_of_diffeomorph's mechanism minus surjectivity;
• the preimage of a relatively compact open under the zero extension is relatively compact (isCompact_closure_preimage_padExt);
• restriction to a smaller open: for relatively compact opens W' ≤ W of the ambient, the compatibility field compat of the family (Functor/Family.lean; the restriction of the factorization to a smaller open determines the factorization, [Wlo09, Theorem 2.0.2(5)]) gives the sequence over W' as the pull-back of the sequence over W along the open inclusion with empty centres erased (localResolutionSeq_of_le); the last-stage lift liftOfLe (the lift of [Kol07, Definition 30.1], through stageOfEq, eraseEmptyLast, pullbackLiftLast) is an injective local isomorphism over the inclusion with range the part over W'; the final strict transforms correspond (strictTransformSubspaceSeq_last_liftOfLe); so the induced morphism of closed subspaces is an open immersion localResolutionHomOfLe : Ỹ(W') → Ỹ(W) over the piece (localResolutionToPiece_comp_localResolutionHomOfLe) whose range covers everything over an open N ⊆ embPreimage W', and exists_restrictSet_isIso_localResolution_of_le is the open-immersion form of the relation at it.

Not in the sources beyond Kollár's comparison; bookkeeping (the lift of [Kol07, Definition 30.1] at an open inclusion; the functoriality of quotients).

The relation "isomorphic over N" is an equivalence

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

The relation "(A, pA) and (B, pB) over Z are isomorphic over N compatibly with the maps" is transitive: compose the two isomorphisms of the restrictions.

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

The relation is symmetric: the inverse isomorphism.

The open-immersion form of the restriction lemma

theorem AnalyticSpace.KLocallyRingedSpace.exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion {K : Type} [RCLike K] {A B Z : AnalyticSpace K} (χ : A.toKLocallyRingedSpace ⟶ B.toKLocallyRingedSpace) [hχ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑χ] (pA : A.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (pB : B.toKLocallyRingedSpace ⟶ Z.toKLocallyRingedSpace) (h : CategoryTheory.CategoryStruct.comp χ pB = pA) (N : Set ↑↑Z.toPresheafedSpace) (hNo : IsOpen N) (hN : Hom.toFun pB ⁻¹' N ⊆ Set.range (Hom.toFun χ)) : ∃ (ψ' : 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 OPEN IMMERSION χ : A → B over Z (χ ≫ pB = pA) whose range contains pB⁻¹ N, for an OPEN N, restricts to an isomorphism A|pA⁻¹N ≅ B|pB⁻¹N over Z|N — isoOfRangeEq of the two open immersions A|pA⁻¹N → B and B|pB⁻¹N → B with equal ranges, the compatibility by lift_uniq/lift_fac; the isomorphism hypothesis of exists_restrictSet_isIso_of_comp_eq weakened to the range condition.

theorem AnalyticSpace.exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion {𝕜 : Type} [RCLike 𝕜] {A B Z : AnalyticSpace 𝕜} (χ : A ⟶ B) (hχ : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑χ) (pA : A ⟶ Z) (pB : B ⟶ Z) (h : CategoryTheory.CategoryStruct.comp χ pB = pA) (N : Set ↑↑Z.toPresheafedSpace) (hNo : IsOpen N) (hN : ↑pB ⁻¹' N ⊆ Set.range ↑χ) : ∃ (ψ : A.restrictSet (↑pA ⁻¹' N) ⟶ B.restrictSet (↑pB ⁻¹' N)), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (Hom.restrictSet pB N) = Hom.restrictSet pA N

The relation "isomorphic over N" from an open immersion over the piece whose range covers pB⁻¹ N, N open — the analytic-space form of KLocallyRingedSpace.exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion.

The preimage of a relatively compact open under the zero extension

theorem Hironaka.Manifold.isClosedEmbedding_padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Topology.IsClosedEmbedding (padExt σ G)

The zero extension s : G → padOpens σ G is a closed embedding: a homeomorphism onto the closed slice (padExtDiffeomorph, isClosed_padSlice). Internal.

theorem Hironaka.Manifold.isCompact_closure_preimage_padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (U : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens σ G)).carrier) (hU : IsCompact (closure ↑U)) : IsCompact (closure (padExt σ G ⁻¹' ↑U))

The preimage under the zero extension of a relatively compact open is relatively compact: closure (s⁻¹ U) ⊆ s⁻¹ (closure U), the preimage of a compact set under a closed embedding (Topology.IsClosedEmbedding.isCompact_preimage).

The induced morphism of closed subspaces along an injective local isomorphism

theorem Hironaka.Manifold.isOpenImmersion_homOfPullbackEq_of_injective {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A A' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (f : AnalyticMap A' A) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑f) {J' : A'.IdealSheaf} {J : A.IdealSheaf} (hi : Function.Injective ⇑f) (h : J' = Manifold.IdealSheaf.pullback ⇑f ⋯ J) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(Manifold.IdealSheaf.homOfPullbackEq ⇑f ⋯ h)

The morphism of closed subspaces induced by J' = f^* J along an INJECTIVE local analytic isomorphism f is an open immersion: the base map is the restriction of the open embedding f to the cosupports (cosupport_pullback_of_bijective with germMap_bijective_of_isLocalDiffeomorphAt, Set.restrictPreimage_isOpenEmbedding), the fibre maps are bijective (isIso_map_stalkMap_of_bijective), Mathlib's LocallyRingedSpace.IsOpenImmersion.of_stalk_iso — isIso_homOfPullbackEq_of_diffeomorph's mechanism minus surjectivity.

theorem Hironaka.Manifold.range_toFun_homOfPullbackEq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A A' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (f : AnalyticMap A' A) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑f) {J' : A'.IdealSheaf} {J : A.IdealSheaf} (h : J' = Manifold.IdealSheaf.pullback ⇑f ⋯ J) : Set.range ↑(Manifold.IdealSheaf.homOfPullbackEq ⇑f ⋯ h) = {z : ↑↑J.toAnalyticSpace.toPresheafedSpace | ↑J.toAnalyticSpaceι z ∈ Set.range ⇑f}

The range of the induced morphism along a local analytic isomorphism: the points of Sp(A)/J over the range of f (the cosupport of f^* J is the preimage of the cosupport of J, cosupport_pullback_of_bijective).

The local resolution over a smaller open

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_of_eq_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (L' : BlowUpSequence ψ₀ N) (e : L' = (L.pullback h hh).eraseEmpty) (J' : N.IdealSheaf) (J : M.IdealSheaf) (hJ : J' = Manifold.IdealSheaf.pullback ⇑h ⋯ J) : L'.toSuccession.strictTransformSubspaceSeq J' (Fin.last L'.toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(ContMDiffMap.comp (L.pullbackLiftLast h hh) (ContMDiffMap.comp (L.pullback h hh).eraseEmptyLast.symm.toAnalyticMap (stageOfEq e).toAnalyticMap)) ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length))

strictTransformSubspaceSeq_last_pullback_eraseEmpty' read through a sequence EQUAL to the erased pull-back and an ideal EQUAL to the pulled-back ideal: the final strict transform of J' along L' is the pull-back of the final strict transform of J along L under the lift pullbackLiftLast ∘ eraseEmptyLast⁻¹ ∘ stageOfEq e (the lift of [Kol07, Definition 30.1]; subst on both equalities, stageOfEq rfl the identity). Internal.

theorem Hironaka.Manifold.PieceEmbedding.localResolutionSeq_of_le {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : E.localResolutionSeq bed W' hW' = ((E.localResolutionSeq bed W hW).pullback ((pieceAmbient 𝕜 E.G).restrictLE hle) ⋯).eraseEmpty

The compatibility field compat of the family (Functor/Family.lean) at the piece's triple ([Wlo09, Theorem 2.0.2(5)]): the sequence over W' is the pull-back of the sequence over W along the open inclusion, empty centres erased.

noncomputable def Hironaka.Manifold.PieceEmbedding.liftOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : AnalyticMap ((E.localResolutionSeq bed W' hW').stage (Fin.last (E.localResolutionSeq bed W' hW').length)) ((E.localResolutionSeq bed W hW).stage (Fin.last (E.localResolutionSeq bed W hW).length))

The last-stage lift of the open inclusion W' ↪ W (the lift of [Kol07, Definition 30.1] at an open inclusion): the transport stageOfEq along localResolutionSeq_of_le, then eraseEmptyLast⁻¹, then pullbackLiftLast — an analytic map from the last stage of the sequence over W' to the last stage of the sequence over W.

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.isLocalDiffeomorph_liftOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(E.liftOfLe bed W hW W' hW' hle)

The lift is a local analytic isomorphism (isLocalDiffeomorph_pullbackLiftLast, two diffeomorphisms).

theorem Hironaka.Manifold.PieceEmbedding.injective_liftOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : Function.Injective ⇑(E.liftOfLe bed W hW W' hW' hle)

The lift is injective (injective_pullbackLiftLast, the inclusion injective).

theorem Hironaka.Manifold.PieceEmbedding.stageMap_last_liftOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (q : ((E.localResolutionSeq bed W' hW').stage (Fin.last (E.localResolutionSeq bed W' hW').length)).carrier) : ((E.localResolutionSeq bed W hW).toSuccession.stageMap (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)) ((E.liftOfLe bed W hW W' hW' hle) q) = ((pieceAmbient 𝕜 E.G).restrictLE hle) (((E.localResolutionSeq bed W' hW').toSuccession.stageMap (Fin.last (E.localResolutionSeq bed W' hW').toSuccession.length)) q)

The lift lies over the open inclusion (stageMap_last_pullbackLiftLast, stageMap_last_eraseEmptyLast_symm, stageMap_last_stageOfEq).

theorem Hironaka.Manifold.PieceEmbedding.range_liftOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : Set.range ⇑(E.liftOfLe bed W hW W' hW' hle) = ⇑((E.localResolutionSeq bed W hW).toSuccession.stageMap (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)) ⁻¹' Set.range ⇑((pieceAmbient 𝕜 E.G).restrictLE hle)

The range of the lift is the part of the last stage over W' (range_pullbackLiftLast).

theorem Hironaka.Manifold.PieceEmbedding.strictTransformSubspaceSeq_last_liftOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : (E.localResolutionSeq bed W' hW').toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W') (Fin.last (E.localResolutionSeq bed W' hW').toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(E.liftOfLe bed W hW W' hW' hle) ⋯ ((E.localResolutionSeq bed W hW).toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W) (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length))

The final strict transforms correspond under the lift: strictTransformSubspaceSeq_last_pullback_eraseEmpty' with strictTransformSubspaceSeq_last_stageOfEq and 𝓘|W' = (𝓘|W).comap (W' ↪ W) (pullback_comp).

noncomputable def Hironaka.Manifold.PieceEmbedding.localResolutionHomOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : E.localResolution bed W' hW' ⟶ E.localResolution bed W hW

The local resolution over W' maps into the local resolution over W (Kol07, Theorem 36, proof): the morphism of closed subspaces induced along the lift by strictTransformSubspaceSeq_last_liftOfLe.

Equations

• E.localResolutionHomOfLe bed W hW W' hW' hle = Manifold.IdealSheaf.homOfPullbackEq ⇑(E.liftOfLe bed W hW W' hW' hle) ⋯ ⋯

theorem Hironaka.Manifold.PieceEmbedding.isOpenImmersion_localResolutionHomOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(E.localResolutionHomOfLe bed W hW W' hW' hle)

It is an open immersion (isOpenImmersion_homOfPullbackEq_of_injective at the injective local isomorphism liftOfLe).

theorem Hironaka.Manifold.PieceEmbedding.localResolutionToPiece_comp_localResolutionHomOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) : CategoryTheory.CategoryStruct.comp (E.localResolutionHomOfLe bed W hW W' hW' hle) (E.localResolutionToPiece bed W hW) = E.localResolutionToPiece bed W' hW'

It lies over the piece: Π_W ∘ χ = Π_{W'} — Hom.ext_of_comp_quotientι on the square of the composites through localResolutionMap_comp_ι, stageMap_last_liftOfLe, homOfPullbackEq_comp_toAnalyticSpaceι and inclusion W ∘ restrictLE = inclusion W'.

theorem Hironaka.Manifold.PieceEmbedding.preimage_subset_range_localResolutionHomOfLe {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (N : Set ↑↑(X.restrictSet V).toPresheafedSpace) (hN : N ⊆ E.embPreimage W') : ↑(E.localResolutionToPiece bed W hW) ⁻¹' N ⊆ Set.range ↑(E.localResolutionHomOfLe bed W hW W' hW' hle)

Its range covers the part over N for N ⊆ embPreimage W': a point of Ỹ(W) over N lies over W' (range_toFun_homOfPullbackEq, range_liftOfLe, the ambient point of Π_W q is the composite of q).

theorem Hironaka.Manifold.PieceEmbedding.exists_restrictSet_isIso_localResolution_of_le {𝕜 : 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)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : W' ≤ W) (N : Set ↑↑(X.restrictSet V).toPresheafedSpace) (hNo : IsOpen N) (hN : N ⊆ E.embPreimage W') : ∃ (ψ : (E.localResolution bed W hW).restrictSet (↑(E.localResolutionToPiece bed W hW) ⁻¹' N) ⟶ (E.localResolution bed W' hW').restrictSet (↑(E.localResolutionToPiece bed W' hW') ⁻¹' N)), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (AnalyticSpace.Hom.restrictSet (E.localResolutionToPiece bed W' hW') N) = AnalyticSpace.Hom.restrictSet (E.localResolutionToPiece bed W hW) N

Restriction to a smaller open (the value over W read over W' ⊆ W, Kol07, Theorem 36, proof; the compatibility compat of the family, [Wlo09, Theorem 2.0.2(5)]): for relatively compact opens W' ≤ W of the ambient and an open N of the piece lying over W', the local resolutions over W and over W' are isomorphic over N compatibly with the maps to the piece — exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion at the open immersion localResolutionHomOfLe over the piece whose range covers the part over N, then exists_restrictSet_isIso_symm for the orientation.