The run's exceptional members and their restriction along an open embedding of inputs

The empty blow-up convention [Kol07, 32] and the commutation with smooth morphisms [Kol07, 34.1], read on the family functor: for ANY open embedding g : N → M of admissible inputs (T' = g⁻¹T, DomBEDan on both sides) and relatively compact opens W' ⊆ N, W ⊆ M with g(W') ⊆ W, the functor's value on T' over W' is the value on T over W pulled back and cleaned of its empty blow-ups (BEDanFamStar.seqOn_eq_of_isAnalyticOpenEmbedding, LocalResolutionOn.lean) — so the last-stage boundary members of the run on T' are the members of the run on T of the stages that survive over W', read through the lift liftOn of the last stages (pullbackLiftLast after the inverse of eraseEmptyLast and the cast stageOfEq), and the members of the deleted stages are EMPTY over W'. For the run's members as CLOSED SUBSPACES of its local resolution (runMembers, for any admissible input, and its coproduct instance sigmaMembers, both in CoproductExceptionalFamily.lean) this module proves the identity along the open immersion localResolutionHomOn of the local resolutions:

• an ORDER EMBEDDING lab of the stage set of the run on T' into that of the run on T — the BoundaryCorr correspondence of Functor/EraseEmptyBoundary.lean composed along eraseEmptyLast and stageOfEq, then totalTransformSeqFrom_last_pullbackLiftLast along pullbackLiftLast;
• the inverse image along localResolutionHomOn of the member of label lab k IS the member k of the run on T' — the square homOfPullbackEq_comp_toAnalyticSpaceι (the closed inclusions commute with the lift), the bridge comap_ofManifoldHom_eq_pullback and comap_idealSheaf_of_isLocalDiffeomorph (the ideal sheaf of a preimage hypersurface);
• the inverse image of every member OFF the range of lab is the unit ideal ⊤ (the empty subspace; the deleted blow-ups have empty centres over W').

The summand inclusions of a datum's coproduct ambient into the COMMON datum of two adjacent levels of the exhaustion use it (the label maps of the common run, CoproductSumData.lean); at the summand inclusion sigmaMk i of a piece's ambient into a datum's coproduct ambient it says that within one datum the pieces share the single run's stage set as their LABEL SET. hbed : bed.IsEmbeddedDesing is the only hypothesis. Not in the sources beyond the convention cited; bookkeeping.

theorem AnalyticManifold.BlowUpSequence.stageOfEq_symm_symm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {L₁ L₂ : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (e : L₁ = L₂) : ⇑(stageOfEq ⋯).symm = ⇑(stageOfEq e)

The cast stageOfEq along e.symm, inverted, is the cast along e (both are the identity).

theorem Hironaka.Manifold.comap_top_closedSubspace {𝕜 : Type} [RCLike 𝕜] {Y Z : AnalyticSpace 𝕜} (f : Y ⟶ Z) : ⊤.comap f = ⊤

The inverse image of the unit ideal — the empty subspace — is the unit ideal.

theorem Hironaka.Manifold.BEDanFamStar.exists_orderEmbedding_hyp_runFamily_eq_preimage_liftOn {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) : ∃ (lab : (bed.runFamily T' hT' W' hW').ι ↪o (bed.runFamily T hT W hW).ι), (∀ (k : (bed.runFamily T' hT' W' hW').ι), (bed.runFamily T' hT' W' hW').hyp k = ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) ⁻¹' (bed.runFamily T hT W hW).hyp (lab k)) ∧ ∀ σ ∉ Set.range ⇑lab, ⇑(bed.liftOn T hT W hW T' hT' g hg hpb W' hW' hle hbed) ⁻¹' (bed.runFamily T hT W hW).hyp σ = ∅

The boundary members of the run on T' are the preimages along the lift of the members of the run on T ([Kol07, 32], [Kol07, 34.1]), through an ORDER EMBEDDING of the stage sets, the members off its range pulling back to ∅ — the BoundaryCorr correspondence composed along eraseEmptyLast (boundaryCorr_eraseEmpty_self) and the cast (boundaryCorr_of_eq), read through totalTransformSeqFrom_last_pullbackLiftLast.

theorem Hironaka.Manifold.BEDanFamStar.comap_localResolutionHomOn_runMembers {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) (σ : (bed.runFamily T hT W hW).ι) : AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed)) (bed.runMembers T hT W hW hbed σ) = AnalyticSpace.ClosedSubspace.comap ⋯.idealSheaf (bed.lastIdealOn T' hT' W' hW').toAnalyticSpaceι

The inverse image of a member of the run on T along localResolutionHomOn is the trace of the preimage hypersurface along the lift — the square homOfPullbackEq_comp_toAnalyticSpaceι, the bridge comap_ofManifoldHom_eq_pullback and comap_idealSheaf_of_isLocalDiffeomorph.

theorem Hironaka.Manifold.BEDanFamStar.exists_orderEmbedding_comap_localResolutionHomOn_runMembers {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (g : AnalyticMap N M) (hg : Manifold.IsAnalyticOpenEmbedding g) (hpb : T'.IsPullbackOf T g) (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (hle : ⇑g '' ↑W' ⊆ ↑W) : ∃ (lab : (bed.runFamily T' hT' W' hW').ι ↪o (bed.runFamily T hT W hW).ι), (∀ (k : (bed.runFamily T' hT' W' hW').ι), AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed)) (bed.runMembers T hT W hW hbed (lab k)) = bed.runMembers T' hT' W' hW' hbed k) ∧ ∀ σ ∉ Set.range ⇑lab, AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT W hW T' hT' g hg hpb W' hW' hle hbed)) (bed.runMembers T hT W hW hbed σ) = ⊤

The restriction identity of the exceptional members along an open embedding of admissible inputs ([Kol07, 34.1]) — an order embedding lab of the stage set of the run on T' into that of the run on T such that the member of label lab k pulls back along localResolutionHomOn to the member k of the run on T', and every member off the range of lab pulls back to the unit ideal ⊤. The summand inclusions of the common datum of two adjacent levels of the exhaustion are the instances that give the label maps of the common run (CoproductSumData.lean).

theorem Hironaka.Manifold.BEDanFamStar.preimage_liftOn_runFamily_eq_of_pullback_eq {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (g₁ g₂ : AnalyticMap N M) (hg₁ : Manifold.IsAnalyticOpenEmbedding g₁) (hg₂ : Manifold.IsAnalyticOpenEmbedding g₂) (hpb₁ : T'.IsPullbackOf T g₁) (hpb₂ : T'.IsPullbackOf T g₂) (hle₁ : ⇑g₁ '' ↑W' ⊆ ↑W) (hle₂ : ⇑g₂ '' ↑W' ⊆ ↑W) (hrun : (bed.seqOn T hT W hW).pullback (AnalyticMap.restrictMap g₁ W' W hle₁) ⋯ = (bed.seqOn T hT W hW).pullback (AnalyticMap.restrictMap g₂ W' W hle₂) ⋯) (σ : (bed.runFamily T hT W hW).ι) : ⇑(bed.liftOn T hT W hW T' hT' g₁ hg₁ hpb₁ W' hW' hle₁ hbed) ⁻¹' (bed.runFamily T hT W hW).hyp σ = ⇑(bed.liftOn T hT W hW T' hT' g₂ hg₂ hpb₂ W' hW' hle₂ hbed) ⁻¹' (bed.runFamily T hT W hW).hyp σ

The fixed-run synchronisation at the level of the boundary families ((37.2) in [Kol07, Proposition 37, proof]) — two open embeddings g₁, g₂ of one admissible input into (T, W) with EQUAL pulled-back runs pull every member of the run's boundary family back along their lifts to the same set: both lifts read the same totalTransformSeqFrom of the same list (totalTransformSeqFrom_last_pullbackLiftLast twice, preimage_eq_of_comap_eq).

theorem Hironaka.Manifold.BEDanFamStar.comap_localResolutionHomOn_runMembers_eq_of_pullback_eq {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT' : DomBEDan 𝕜 T') (W' : TopologicalSpace.Opens N.carrier) (hW' : IsCompact (closure ↑W')) (g₁ g₂ : AnalyticMap N M) (hg₁ : Manifold.IsAnalyticOpenEmbedding g₁) (hg₂ : Manifold.IsAnalyticOpenEmbedding g₂) (hpb₁ : T'.IsPullbackOf T g₁) (hpb₂ : T'.IsPullbackOf T g₂) (hle₁ : ⇑g₁ '' ↑W' ⊆ ↑W) (hle₂ : ⇑g₂ '' ↑W' ⊆ ↑W) (hrun : (bed.seqOn T hT W hW).pullback (AnalyticMap.restrictMap g₁ W' W hle₁) ⋯ = (bed.seqOn T hT W hW).pullback (AnalyticMap.restrictMap g₂ W' W hle₂) ⋯) (σ : (bed.runFamily T hT W hW).ι) : AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT W hW T' hT' g₁ hg₁ hpb₁ W' hW' hle₁ hbed)) (bed.runMembers T hT W hW hbed σ) = AnalyticSpace.QuotientSpace.comap (↑(bed.localResolutionHomOn T hT W hW T' hT' g₂ hg₂ hpb₂ W' hW' hle₂ hbed)) (bed.runMembers T hT W hW hbed σ)

The fixed-run synchronisation ((37.2) in [Kol07, Proposition 37, proof]) — two open embeddings g₁, g₂ of one admissible input (T', W') into (T, W) with EQUAL pulled-back runs (the conclusion of seqOn_pullback_eq_of_pullback_eq, ExceptionalFamilyGlue.lean) pull every member of the run on T back along the two open immersions of local resolutions to the SAME closed subspace: the stage-σ member on one side IS the stage-σ member on the other — no label is chosen, the label is a stage of the one run.