The parts of a piece's local resolution over a base open, read on the ambient

Two bookkeeping identities for the assembly of the mixed-pair transition of the common datum (CoproductMixedTransition.lean):

• a point of a piece's local resolution lies over the base open domOpens Q (in X) iff its ambient point — the last stage's composite blow-down read through the closed inclusion — lies in the ambient open Q (toFun_toSpaceMap_eq, pieceOverIncl_mem_domOpens_iff, localResolutionMap_comp_ι);
• along the open immersion localResolutionHomOn (LocalResolutionOn.lean) of the piece's local resolution over W' into the local resolution of (T, W) along an open embedding g of admissible inputs, the part of the source over the base open domOpens Q (Q ≤ W') maps ONTO the part of the target over the ambient open g(Q) (range_toFun_localResolutionHomOn, stageMap_last_liftOn).

Both are used by isoOfRangeEq in the assembly: the two padded pieces' parts over one base open P are identified with the local resolution of the common admissible input over W₁' through the common run's local resolution. hbed is the only hypothesis. Not in the sources; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.toFun_toSpaceMap_mem_domOpens_iff {𝕜 : 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)) (Q : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (y : ↑↑(E.localResolution bed W hW).toPresheafedSpace) : AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW) y ∈ E.domOpens Q ↔ ↑(((E.localResolutionSeq bed W hW).toSuccession.stageMap (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)) (↑((E.localResolutionSeq bed W hW).toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W) (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).toAnalyticSpaceι y)) ∈ Q

A point of the local resolution lies over the base open of Q iff its ambient point lies in Q — toSpaceMap = pieceOverIncl ∘ Π (toFun_toSpaceMap_eq), pieceOverIncl_mem_domOpens_iff, and the square ι_W ∘ Π = composite ∘ ι_Y (localResolutionMap_comp_ι).

theorem Hironaka.Manifold.PieceEmbedding.range_ofRestrict_comp_localResolutionHomOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (g : AnalyticMap (pieceAmbient 𝕜 E.G) M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : E.ambientTriple.IsPullbackOf T g) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (Q : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hQ : Q ≤ W') : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (CategoryTheory.CategoryStruct.comp ((E.localResolution bed W' hW').ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W' hW'), continuous_toFun := ⋯ }) (E.domOpens Q))) (bed.localResolutionHomOn T hT W hW E.ambientTriple ⋯ g hg hpb W' hW' hle hbed))) = {y : ↑↑(bed.lastIdealOn T hT W hW).toAnalyticSpace.toPresheafedSpace | ↑(((bed.seqOn T hT W hW).toSuccession.stageMap (Fin.last (bed.seqOn T hT W hW).toSuccession.length)) (↑(bed.lastIdealOn T hT W hW).toAnalyticSpaceι y)) ∈ ⇑g '' ↑Q}

The part of the piece's local resolution over the base open domOpens Q maps under localResolutionHomOn ONTO the part of the target's local resolution over the ambient open g(Q) (Q ≤ W'): the lift covers g (stageMap_last_liftOn), the range of the immersion is the part over g(W') (range_toFun_localResolutionHomOn), and g is injective.