Pull-backs of blow-up sequences up to empty blow-ups

The vocabulary predicate FiniteSuccession.IsPullbackUpToEmptyAlong R S g (Włodarczyk's "the induced sequence g^*(S) is an extension of R" [Wlo09, Theorem 3.5.1 (2)]) is read off the pull-back of a blow-up sequence along a local analytic isomorphism (BlowUpSequence.pullback, the sequence of the fibre products [Wlo09, Proposition 3.4.1]):

• BlowUpSequence.isPullbackUpToEmptyAlong_of_isExtensionOf: if the pull-back of L along h : U' → U is an extension of R ([Wlo09, Definition 3.2.6]) and h is the restriction of g : N → M, then R is the pull-back of L along g up to empty blow-ups. The lift of a stage R_{j_k} to L_k is the stage lift of the pull-back (pullbackLift) after the inverse of the identification of the extension; the clauses come from the stage lifts (stageMap_pullbackLift, map_pullbackLift) and the centres of the pull-back (center_pullback).
• BlowUpSequence.isPullbackUpToEmptyAlong_eraseEmpty_pullback: the pull-back with its empty blow-ups erased ([Kol07, 32]) is such an R (isExtensionOf_toSuccession_eraseEmpty).
• CompatibleFamily.isPullbackUpToEmptyAlong_seqOn: for two compatible families whose values on U' and on its image g(U') are related by the commutation equation of a family functor (AnalyticFamilyFunctor.CommutesWithLocalIsos, Kollár's [Kol07, 34.1] read per open), the value on U' is the pull-back along g up to empty blow-ups of the value on every relatively compact open U ⊇ g(U'): the compatibility of the family along g(U') ⊆ U (CompatibleFamily.compat), eraseEmpty_pullback_eraseEmpty and pullback_comp.

theorem AnalyticManifold.BlowUpSequence.isPullbackUpToEmptyAlong_of_isExtensionOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} {U' : TopologicalSpace.Opens N.carrier} (L : BlowUpSequence ψ₀ (M.restrict U)) (h : AnalyticMap (N.restrict U') (M.restrict U)) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (g : AnalyticMap N M) (hgh : ∀ (p : (N.restrict U').carrier), (M.inclusion U) (h p) = g ((N.inclusion U') p)) {R : (N.restrict U').FiniteSuccession} (hR : (L.pullback h hh).toSuccession.IsExtensionOf R) : R.IsPullbackUpToEmptyAlong L.toSuccession g

An extension of the pull-back is a pull-back up to empty blow-ups: if the pull-back of the sequence L over U ⊆ M along the local analytic isomorphism h : U' → U is an extension of R ([Wlo09, Definition 3.2.6]) and h is the restriction of g : N → M, then R is the pull-back of L along g up to blow-ups with empty centre ([Wlo09, Theorem 3.5.1 (2)]): the lift of the stage R_{j_k} is the stage lift of the pull-back after the inverse of the identification of the extension.

theorem AnalyticManifold.BlowUpSequence.isPullbackUpToEmptyAlong_eraseEmpty_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} {U' : TopologicalSpace.Opens N.carrier} (L : BlowUpSequence ψ₀ (M.restrict U)) (h : AnalyticMap (N.restrict U') (M.restrict U)) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (g : AnalyticMap N M) (hgh : ∀ (p : (N.restrict U').carrier), (M.inclusion U) (h p) = g ((N.inclusion U') p)) : (L.pullback h hh).eraseEmpty.toSuccession.IsPullbackUpToEmptyAlong L.toSuccession g

The pull-back with its empty blow-ups erased ([Kol07, 32]) is the pull-back up to empty blow-ups: isPullbackUpToEmptyAlong_of_isExtensionOf at the extension isExtensionOf_toSuccession_eraseEmpty.

theorem Hironaka.Manifold.CompatibleFamily.isPullbackUpToEmptyAlong_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} {T' : Manifold.AnalyticTriple ψ₀ N} (C : CompatibleFamily T) (C' : CompatibleFamily T') (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) (hC : C'.seqOn U' hU' = ((C.seqOn (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hgU : ⇑g '' ↑U' ⊆ ↑U) : (C'.seqOn U' hU').toSuccession.IsPullbackUpToEmptyAlong (C.seqOn U hU).toSuccession g

The value on U' is the pull-back along g of the value on any U ⊇ g(U'), up to empty blow-ups ([Wlo09, Theorem 3.5.1 (2)]), for two compatible families related on U' and its image g(U') by the commutation equation of [Kol07, 34.1]: the compatibility of the family along g(U') ⊆ U rewrites the value on g(U') as the erased pull-back of the value on U, the two erasures and pull-backs combine (eraseEmpty_pullback_eraseEmpty, pullback_comp), and isPullbackUpToEmptyAlong_eraseEmpty_pullback reads the result.