The resolution family commutes with local analytic isomorphisms

The value of the resolution family resolveFam bo (the rounds of the order-reduction functors bo d at decreasing maximal order, Hironaka/Resolution/Analytic/Wlo09/Rounds.lean) on a pulled-back triple is the pull-back of the value, with the empty blow-ups erased: for a local analytic isomorphism g : N → M, a triple T' on N carrying the pull-back data of a triple T on M and a relatively compact open U' ⊆ N, the value of T' on U' is the pull-back of the value of T on the image g(U') along g|_{U'} : U' → g(U'), its empty blow-ups erased (resolveSeqOn_pullback). This is the behaviour of a blow-up sequence functor under smooth morphisms [Kol07, 34.1], and Włodarczyk's commutation of the canonical principalization with local analytic isomorphisms [Wlo09, Theorem 3.5.1 (2)] for the locally finite principalization [Wlo09, Theorem 2.0.3]; the compatibility of the family under restriction (resolveSeqOn_compat, Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean) is the case of an open inclusion.

The proof reads the canonical chain c of g(U') on M (canonicalResolveChain) and builds an admissible chain c' for U' on N of the same length: the iterated shrinks of closure U' inside g⁻¹(c.W 0) (shrinkChain), on whose outermost open the order of the pulled-back ideal is at most the length, the order being invariant under local analytic isomorphisms (IdealSheaf.ord_pullback_of_isLocalDiffeomorphAt). The value of T' on U' is its value along c' (canonicity, resolveSeqOnAlong_chain_indep), and the transport theorem of the rounds (eraseEmpty_resolveFrom_congr, Hironaka/Resolution/Analytic/Wlo09/Transport.lean) along the restriction of g to the outermost opens, with the reading maps the inclusions of U' and g(U'), identifies the two erased lists.

theorem Hironaka.Manifold.resolveSeqOn_pullback {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hpb : T'.IsPullbackOf T g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : resolveSeqOn bo T' U' hU' = ((resolveSeqOn bo T (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

The value of the resolution family commutes with local analytic isomorphisms ([Kol07, 34.1]; [Wlo09, Theorem 3.5.1 (2)]): for a local analytic isomorphism g : N → M and a triple T' on N carrying the pull-back data of T, the value of T' on a relatively compact open U' is the pull-back of the value of T on g(U') along g|_{U'}, with the empty blow-ups erased. The canonical chain of g(U') and the shrinks of closure U' inside the preimage of its innermost open are two chains of the same length related by g, and the transport theorem of the rounds identifies their values (eraseEmpty_resolveFrom_congr).