The push-forward relation along the re-modelling

Kollár's push-forward relation up to empty blow-ups (FiniteSuccession.IsPushforwardUpToEmptyAlong, the form of the commutation of a principalization with closed embeddings over the compact sets) carries back from the re-modelled manifolds (IsPushforwardUpToEmptyAlong.transportAlong): if the succession S over an open U of M.transport ψ is the push-forward of the succession R over an open U' of N.transport ψ' along the re-modelled map τT of τ : N → M, then the successions carried back to M and N (transportAlong at the identities of the opens, Hironaka/Resolution/Analytic/ModelTransport/Succession.lean) are related in the same way along τ. The block index is kept, and every embedding is conjugated by the stage identifications of the two transports, which carry the embeddings, the closures of their images, the composite blow-downs, the blow-downs and the supports of the centres — the counterpart for closed embeddings of IsPullbackUpToEmptyAlong.transportAlong for local analytic isomorphisms.

theorem AnalyticManifold.FiniteSuccession.IsPushforwardUpToEmptyAlong.transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} {E₁ : Type u_3} {E₁' : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₁'] [NormedSpace 𝕜 E₁'] {M : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (ψ : E ≃L[𝕜] E₁) (ψ' : E' ≃L[𝕜] E₁') {U : TopologicalSpace.Opens M.carrier} {U' : TopologicalSpace.Opens N.carrier} {S : ((M.transport ψ).restrict (M.transportOpens ψ U)).FiniteSuccession} {R : ((N.transport ψ').restrict (N.transportOpens ψ' U')).FiniteSuccession} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (τT : ContMDiffMap (modelWithCornersSelf 𝕜 E₁') (modelWithCornersSelf 𝕜 E₁) (N.transport ψ').carrier (M.transport ψ).carrier ⊤) (hτ : ∀ (x : N.carrier), τT (N.toTransport ψ' x) = M.toTransport ψ (τ x)) (h : S.IsPushforwardUpToEmptyAlong R τT) : (FiniteSuccession.transportAlong (M.restrictTransportDiffeomorph ψ U) ψ.symm S).IsPushforwardUpToEmptyAlong (FiniteSuccession.transportAlong (N.restrictTransportDiffeomorph ψ' U') ψ'.symm R) τ

Kollár's push-forward relation up to empty blow-ups carries back from the re-modelled manifolds: if the succession S over an open U of M.transport ψ is the push-forward of the succession R over an open U' of N.transport ψ' along the re-modelled map τT of τ, then the successions carried back to M and N (transportAlong at the identities of the opens) are related in the same way along τ. The block index is kept and every embedding is conjugated by the stage identifications of the two transports.