The exceptional members under restriction to a smaller open

Statement. Restricting a piece's run to a smaller relatively compact open W' ⊆ W deletes the blow-ups whose centres miss W' (the functor's CommutesWithOpenEmbeddings: the run over W' is the cleaned pull-back ((run over W).pullback incl).eraseEmpty; the compatibility of [Kol07, 34.1] and [Wlo09, Theorem 2.0.2(5)]). The theorem BlowUpSequence.exists_orderEmb_totalTransformSeqFrom_last_pullback_eraseEmpty says what this does to the BOUNDARY FAMILY at the last stage: along the lift λ := h_r ∘ eraseEmptyLast⁻¹ of a local isomorphism h there is an order embedding ε of the cleaned run's index type into the original run's with λ⁻¹(H_{ε i}) = H'_i for every member i and λ⁻¹(H_b) = ∅ outside the range of ε — the members whose creation steps were deleted have empty trace over W' (the empty blow-ups arising from restriction, [Kol07, Warning 20]: these are ONE source of empty traces, not the only one). PieceEmbedding.exists_orderEmb_totalTransformSeq_last_liftOfLe is its instance at a piece, along the lift liftOfLe of the open inclusion W' ↪ W.

Why. The restriction to a smaller open is the first and last leg — (γ) in the notation of LocalResolutionShear.lean — of the transition of localResolution_independent_local, (γ)·(α)⁻¹·(β)·(α)·(γ)⁻¹, and the only leg where the correspondence of the boundary families is a proper injection.

Conventions. The list-level theorem is stated for an arbitrary start family F (totalTransformSeqFrom); the exceptional family is the instance F := HypersurfaceFamily.empty M (totalTransformSeqFrom_empty, definitional) with (empty M).comap h = empty N (HypersurfaceFamily.empty_comap). The lift is spelled as the lemmas it rests on spell it: the composite of Diffeomorph.toAnalyticMap eraseEmptyLast.symm and pullbackLiftLast, coerced to functions.

Sources. The lift of a local isomorphism to the blow-ups, [Kol07, Definition 30.1]; the empty blow-up convention, [Kol07, 32] and [Kol07, 34.1]; [Wlo09, Theorem 2.0.2(5)]. The proofs compose totalTransformSeqFrom_last_pullbackLiftLast (OrderReduction/ConcatPullback.lean) with eraseEmptyIdx/hyp_eraseEmptyIdx/hyp_eq_empty_of_notMem_range_eraseEmptyIdx (Functor/EraseEmptyBoundary.lean); not in the sources.

theorem AnalyticManifold.BlowUpSequence.exists_orderEmb_totalTransformSeqFrom_last_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) (F : Manifold.HypersurfaceFamily M.carrier) (hF : ∀ (j : F.ι), IsClosed (F.hyp j)) : ∃ (ε : ((L.pullback h hh).eraseEmpty.toSuccession.totalTransformSeqFrom (Manifold.HypersurfaceFamily.comap (⇑h) F) (Fin.last (L.pullback h hh).eraseEmpty.toSuccession.length)).ι ↪o (L.toSuccession.totalTransformSeqFrom F (Fin.last L.toSuccession.length)).ι), (∀ (i : ((L.pullback h hh).eraseEmpty.toSuccession.totalTransformSeqFrom (Manifold.HypersurfaceFamily.comap (⇑h) F) (Fin.last (L.pullback h hh).eraseEmpty.toSuccession.length)).ι), ⇑(L.pullbackLiftLast h hh) ∘ ⇑(L.pullback h hh).eraseEmptyLast.symm.toAnalyticMap ⁻¹' (L.toSuccession.totalTransformSeqFrom F (Fin.last L.toSuccession.length)).hyp (ε i) = ((L.pullback h hh).eraseEmpty.toSuccession.totalTransformSeqFrom (Manifold.HypersurfaceFamily.comap (⇑h) F) (Fin.last (L.pullback h hh).eraseEmpty.toSuccession.length)).hyp i) ∧ ∀ b ∉ Set.range ⇑ε, ⇑(L.pullbackLiftLast h hh) ∘ ⇑(L.pullback h hh).eraseEmptyLast.symm.toAnalyticMap ⁻¹' (L.toSuccession.totalTransformSeqFrom F (Fin.last L.toSuccession.length)).hyp b = ∅

The boundary family of the CLEANED pull-back (h^* L).eraseEmpty at its last stage against the boundary family of L ([Kol07, Definition 30.1]; the empty blow-up convention [Kol07, 32], [Kol07, 34.1]), along the lift λ := h_r ∘ eraseEmptyLast⁻¹ of the local isomorphism h — an order embedding ε of the cleaned list's index type into L's with λ⁻¹(H^L_{ε i}) = H^{cleaned}_i for every i, and λ⁻¹(H^L_b) = ∅ for every b outside the range of ε. From totalTransformSeqFrom_last_pullbackLiftLast and eraseEmptyIdx with hyp_eraseEmptyIdx, hyp_eq_empty_of_notMem_range_eraseEmptyIdx.

theorem Manifold.HypersurfaceFamily.exists_orderIso_of_eq {A : Type u} {F₁ F₂ : HypersurfaceFamily A} (h : F₁ = F₂) : ∃ (o : F₁.ι ≃o F₂.ι), ∀ (j : F₁.ι), F₁.hyp j = F₂.hyp (o j)

The transport of a hypersurface family along an equality: an order isomorphism of the index types matching the members.

theorem AnalyticManifold.BlowUpSequence.totalTransformSeqFrom_last_stageOfEq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n' : ℕ} {ψ₀ : E ≃L[𝕜] Fin n' → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : BlowUpSequence ψ₀ M} (e : L₁ = L₂) (G : Manifold.HypersurfaceFamily M.carrier) : L₂.toSuccession.totalTransformSeqFrom G (Fin.last L₂.toSuccession.length) = Manifold.HypersurfaceFamily.comap (⇑(stageOfEq e).symm.toAnalyticMap) (L₁.toSuccession.totalTransformSeqFrom G (Fin.last L₁.toSuccession.length))

The boundary family at the last stage of an equal list, read through stageOfEq.

theorem Hironaka.Manifold.PieceEmbedding.exists_orderEmb_totalTransformSeq_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.totalTransformSeq (Fin.last (E.localResolutionSeq bed W' hW').toSuccession.length)).ι ↪o ((E.localResolutionSeq bed W hW).toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).ι), (∀ (i : ((E.localResolutionSeq bed W' hW').toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W' hW').toSuccession.length)).ι), ⇑(E.liftOfLe bed W hW W' hW' hle) ⁻¹' ((E.localResolutionSeq bed W hW).toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).hyp (ε i) = ((E.localResolutionSeq bed W' hW').toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W' hW').toSuccession.length)).hyp i) ∧ ∀ b ∉ Set.range ⇑ε, ⇑(E.liftOfLe bed W hW W' hW' hle) ⁻¹' ((E.localResolutionSeq bed W hW).toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).hyp b = ∅

The manifold level at the piece: along the lift liftOfLe of the open inclusion W' ↪ W, the last-stage boundary family over W' corresponds to the one over W — eraseEmptyIdx transported along localResolutionSeq_of_le and empty_comap.