A finite succession carried along an analytic isomorphism across the models

A finite succession of monoidal transformations (FiniteSuccession; Hironaka's succession [Hir64, p. 155], Włodarczyk's finite sequence of blow-ups [Wlo09, Theorem 2.0.3 (1)]) over a manifold N modelled on E' is carried to a manifold N₀ modelled on E along an analytic isomorphism g : N₀ ≃ N across the models and a linear isomorphism ψ : E' ≃L[𝕜] E of the models: S.transportAlong g ψ has the same length, its later stages are S's re-modelled along ψ (AnalyticManifold.transport, Hironaka/Resolution/Analytic/ModelTransport/Manifold.lean), its first centre is pulled back along g and its first blow-down is followed by g⁻¹, and from stage 1 on its centres and blow-downs are S's own read on the re-modelled stages — the same-model base change transportBase of Hironaka/Resolution/Analytic/TransportBase.lean with the models freed. Each transported blow-down is a monoidal transformation with the transported centre by AnalyticMap.IsMonoidalTransformation.of_square (SquareChart.lean) on the square of the stage identifications, whose model isomorphism is ψ at stage 0 and the identity of the re-modelled stage afterwards.

• transportAlongStage i : (S.transportAlong g ψ).stage i ≃ S.stage i — g at stage 0, the identity of the re-modelled stage (transportDiffeomorph.symm) at the later stages; the identifications commute with the blow-downs (map_transportAlong: the square at each step) and with the composite blow-downs (stageMap_transportAlong, composite_transportAlong).
• The centres, the weak transforms (clause (ii) of [Hir64, Main Theorem II'(N), p. 156]) and the boundaries (clause (iii)) of the transported succession are the pull-backs of S's along the stage identifications (center_transportAlong, weakTransformSeq_transportAlong, boundarySeq_transportAlong) — by recursion on the stage, weakTransform_of_square and reducedTransform_of_square (Square.lean) on the square at each step; so are the strict transforms of a closed subspace (strictTransformSubspaceSeq_transportAlong; Kollár's restricted sequence [Kol07, Definition 30.2]), by strictTransformSubspace_of_square on each square: the strict transform along a blowing-up commutes with a square of analytic isomorphisms across the models.

Włodarczyk's extension relation along the transport is in Hironaka/Resolution/Analytic/ModelTransport/SuccessionExtension.lean; the transported families in Family.lean.

The strict transform of a closed subspace along a square

theorem Manifold.strictTransformSubspace_of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M M' : AnalyticManifold 𝕜 E} {N N' : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (g' : Diffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) N'.carrier M'.carrier ⊤) (ψ : E ≃L[𝕜] E') {n n' c c' : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {ψ₁ : E' ≃L[𝕜] Fin n' → 𝕜} {Y : Set M.carrier} {Y' : Set N.carrier} {π : M'.carrier → M.carrier} {π' : N'.carrier → N.carrier} (hY : IsClosedSubmanifold ψ₀ Y c) (h : IsBlowUp ψ₀ Y c π) (hY' : IsClosedSubmanifold ψ₁ Y' c') (h' : IsBlowUp ψ₁ Y' c' π') (e : Y' = ⇑g ⁻¹' Y) (hsq : ∀ (x : N'.carrier), π (g' x) = g (π' x)) (I : M.IdealSheaf) : AnalyticManifold.IdealSheaf.pullbackDiffeomorph g' (strictTransformSubspace hY h I) = strictTransformSubspace hY' h' (AnalyticManifold.IdealSheaf.pullbackDiffeomorph g I)

The strict transform of a closed subspace along a square of analytic isomorphisms across the models (the counterpart of IdealSheaf.weakTransform_of_square for strictTransformSubspace): for blowings-up π : M' → M along Y and π' : N' → N along g⁻¹(Y) with π ∘ g' = g ∘ π', the strict transform of g^* I is the pull-back along g' of the strict transform of I. Both sides are the saturations of the total transforms by the exceptional ideals (strictTransformSubspace_eq_ofStalks); the total transforms and the exceptional ideals correspond under g' (IsClosedSubmanifold.idealSheaf_pullbackDiffeomorph), and the stalk isomorphism of g' carries the colon ideals (Ideal.map_colon_pow_equiv).

The transported succession

@[reducible, inline]

abbrev AnalyticManifold.FiniteSuccession.transportAlongLater {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : AnalyticManifold 𝕜 E'} (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (j : Fin S.length) : AnalyticManifold 𝕜 E

The later stages of the transported succession: S's, re-modelled along ψ.

Equations

• AnalyticManifold.FiniteSuccession.transportAlongLater ψ S j = (S.later j).transport ψ

noncomputable def AnalyticManifold.FiniteSuccession.transportAlongCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin S.length) : (N₀.finStages (transportAlongLater ψ S) i.castSucc).IdealSheaf

The centres of the transported succession: the first pulled back along g, the others S's read on the re-modelled stages.

Equations

• AnalyticManifold.FiniteSuccession.transportAlongCenter g ψ S ⟨0, h⟩ = AnalyticManifold.IdealSheaf.pullbackDiffeomorph g (S.center ⟨0, h⟩)
• AnalyticManifold.FiniteSuccession.transportAlongCenter g ψ S ⟨k.succ, h⟩ = AnalyticManifold.IdealSheaf.transport ψ (S.center ⟨k + 1, h⟩)

def AnalyticManifold.FiniteSuccession.transportAlongMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin S.length) : AnalyticMap (N₀.finStages (transportAlongLater ψ S) i.succ) (N₀.finStages (transportAlongLater ψ S) i.castSucc)

The blow-downs of the transported succession: the first followed by g⁻¹, the others S's own on the re-modelled stages (analytic by the typed identities of Hironaka/Resolution/Analytic/ModelTransport/Manifold.lean).

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticManifold.FiniteSuccession.transportAlong_isMonoidal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin S.length) : (transportAlongMap g ψ S i).IsMonoidalTransformation (transportAlongCenter g ψ S i)

Each transported blow-down is a monoidal transformation with the transported centre: AnalyticMap.IsMonoidalTransformation.of_square on the square of the stage identifications — at stage 0 the model isomorphism is ψ and the square is σ_1 = g ∘ (g⁻¹ ∘ σ_1); at a later stage both isomorphisms are the identity of the re-modelled stage.

noncomputable def AnalyticManifold.FiniteSuccession.transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) : N₀.FiniteSuccession

The succession S over N carried to N₀ along g with the later stages re-modelled on E along ψ: stage 0 is N₀, the first centre is pulled back along g, the first blow-down is followed by g⁻¹, the later data are S's own read on the re-modelled stages (the base change transportBase with the models freed).

Equations

• One or more equations did not get rendered due to their size.

The stage identifications

def AnalyticManifold.FiniteSuccession.transportAlongStageAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : ℕ) (h : i < S.length + 1) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (N₀.finStages (transportAlongLater ψ S) ⟨i, h⟩).carrier (N.finStages S.later ⟨i, h⟩).carrier ⊤

The stage identification, by recursion on the index (as stageMapAux): g at stage 0, the identity of the re-modelled stage afterwards.

Equations

• AnalyticManifold.FiniteSuccession.transportAlongStageAux g ψ S 0 x_2 = g
• AnalyticManifold.FiniteSuccession.transportAlongStageAux g ψ S k.succ h = ((S.later ⟨k, ⋯⟩).transportDiffeomorph ψ).symm

def AnalyticManifold.FiniteSuccession.transportAlongStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin (S.length + 1)) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') ((transportAlong g ψ S).stage i).carrier (S.stage i).carrier ⊤

The identification of the stages of the transported succession with those of S: g at stage 0, the identity of the re-modelled stage at the later ones.

Equations

• AnalyticManifold.FiniteSuccession.transportAlongStage g ψ S i = AnalyticManifold.FiniteSuccession.transportAlongStageAux g ψ S ↑i ⋯

theorem AnalyticManifold.FiniteSuccession.transportAlong_length {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) : (transportAlong g ψ S).length = S.length

The transported succession has the length of S.

theorem AnalyticManifold.FiniteSuccession.coe_transportAlongStage_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) : ⇑(transportAlongStage g ψ S 0) = ⇑g

At stage 0 the identification is g.

theorem AnalyticManifold.FiniteSuccession.coe_transportAlongStage_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (k : ℕ) (h : k + 1 < S.length + 1) : ⇑(transportAlongStage g ψ S ⟨k + 1, h⟩) = id

At a later stage the identification is the identity on points.

theorem AnalyticManifold.FiniteSuccession.map_transportAlongStageAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (k : ℕ) (h : k + 1 < S.length + 1) (p : (N₀.finStages (transportAlongLater ψ S) ⟨k + 1, h⟩).carrier) : (S.map ⟨k, ⋯⟩) ((transportAlongStageAux g ψ S (k + 1) h) p) = (transportAlongStageAux g ψ S k ⋯) (((transportAlong g ψ S).map ⟨k, ⋯⟩) p)

The square at each step, on the auxiliary indices: σ_{k+1} ∘ (stage k+1) = (stage k) ∘ σ'_{k+1}; at k = 0 it is g (g⁻¹ y) = y, afterwards definitional.

theorem AnalyticManifold.FiniteSuccession.map_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin S.length) (p : ((transportAlong g ψ S).stage i.succ).carrier) : (S.map i) ((transportAlongStage g ψ S i.succ) p) = (transportAlongStage g ψ S i.castSucc) (((transportAlong g ψ S).map i) p)

The stage identifications commute with the blow-downs: the square σ_{i+1} ∘ e_{i+1} = e_i ∘ σ'_{i+1} at each step.

theorem AnalyticManifold.FiniteSuccession.stageMapAux_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : ℕ) (h : i < S.length + 1) (p : (N₀.finStages (transportAlongLater ψ S) ⟨i, h⟩).carrier) : (S.stageMapAux i h) ((transportAlongStageAux g ψ S i h) p) = g (((transportAlong g ψ S).stageMapAux i h) p)

The composite blow-downs commute with the identifications, on the auxiliary indices: by recursion, the square at each step.

theorem AnalyticManifold.FiniteSuccession.stageMap_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin (S.length + 1)) (p : ((transportAlong g ψ S).stage i).carrier) : (S.stageMap i) ((transportAlongStage g ψ S i) p) = g (((transportAlong g ψ S).stageMap i) p)

The composite blow-downs commute with the identifications: σ^i ∘ e_i = g ∘ σ'^i (Włodarczyk's σ^i, [Wlo09, Theorem 2.0.3 (2)]).

The centres, the weak transforms and the boundaries

theorem AnalyticManifold.FiniteSuccession.center_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (i : Fin S.length) : (transportAlong g ψ S).center i = IdealSheaf.pullbackDiffeomorph (transportAlongStage g ψ S i.castSucc) (S.center i)

The centres of the transported succession are the pull-backs of S's along the stage identifications.

theorem AnalyticManifold.FiniteSuccession.center_transportAlongAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (k : ℕ) (h : k + 1 < S.length + 1) : (transportAlong g ψ S).center ⟨k, ⋯⟩ = IdealSheaf.pullbackDiffeomorph (transportAlongStageAux g ψ S k ⋯) (S.center ⟨k, ⋯⟩)

The centre identity on the auxiliary indices, in the syntactic form of the recursions below.

theorem AnalyticManifold.FiniteSuccession.weakTransformSeqAux_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (J : N.IdealSheaf) (i : ℕ) (h : i < S.length + 1) : (transportAlong g ψ S).weakTransformSeqAux (IdealSheaf.pullbackDiffeomorph g J) i h = IdealSheaf.pullbackDiffeomorph (transportAlongStageAux g ψ S i h) (S.weakTransformSeqAux J i h)

The weak transforms along the transported succession, on the auxiliary indices: by recursion, weakTransform_of_square on the square at each step.

theorem AnalyticManifold.FiniteSuccession.weakTransformSeq_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (J : N.IdealSheaf) (i : Fin (S.length + 1)) : (transportAlong g ψ S).weakTransformSeq (IdealSheaf.pullbackDiffeomorph g J) i = IdealSheaf.pullbackDiffeomorph (transportAlongStage g ψ S i) (S.weakTransformSeq J i)

The weak transforms (clause (ii) of [Hir64, Main Theorem II'(N), p. 156]) along the transported succession, started with g^* J, are the pull-backs of S's along the stage identifications.

theorem AnalyticManifold.FiniteSuccession.boundarySeqAux_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (E₀ : N.IdealSheaf) (i : ℕ) (h : i < S.length + 1) : (transportAlong g ψ S).boundarySeqAux (IdealSheaf.pullbackDiffeomorph g E₀) i h = IdealSheaf.pullbackDiffeomorph (transportAlongStageAux g ψ S i h) (S.boundarySeqAux E₀ i h)

The boundaries along the transported succession, on the auxiliary indices: by recursion, reducedTransform_of_square on the square at each step.

theorem AnalyticManifold.FiniteSuccession.boundarySeq_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (E₀ : N.IdealSheaf) (i : Fin (S.length + 1)) : (transportAlong g ψ S).boundarySeq (IdealSheaf.pullbackDiffeomorph g E₀) i = IdealSheaf.pullbackDiffeomorph (transportAlongStage g ψ S i) (S.boundarySeq E₀ i)

The boundaries (clause (iii) of [Hir64, Main Theorem II'(N), p. 156]) along the transported succession, started with g^* E₀, are the pull-backs of S's along the stage identifications.

theorem AnalyticManifold.FiniteSuccession.strictTransformSubspaceSeqAux_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (J : N.IdealSheaf) (i : ℕ) (h : i < S.length + 1) : (transportAlong g ψ S).strictTransformSubspaceSeqAux (IdealSheaf.pullbackDiffeomorph g J) i h = IdealSheaf.pullbackDiffeomorph (transportAlongStageAux g ψ S i h) (S.strictTransformSubspaceSeqAux J i h)

The strict transforms along the transported succession, on the auxiliary indices: by recursion, strictTransformSubspace_of_square on the square at each step.

theorem AnalyticManifold.FiniteSuccession.strictTransformSubspaceSeq_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (J : N.IdealSheaf) (i : Fin (S.length + 1)) : (transportAlong g ψ S).strictTransformSubspaceSeq (IdealSheaf.pullbackDiffeomorph g J) i = IdealSheaf.pullbackDiffeomorph (transportAlongStage g ψ S i) (S.strictTransformSubspaceSeq J i)

The strict transforms of a closed subspace along the transported succession, started with g^* J, are the pull-backs of S's along the stage identifications (Kollár's restricted sequence [Kol07, Definition 30.2]; Włodarczyk's strict transforms Y_i Wlo09, Theorem 2.0.2 (2)).

theorem AnalyticManifold.FiniteSuccession.composite_transportAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N₀ : AnalyticManifold 𝕜 E} {N : AnalyticManifold 𝕜 E'} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') N₀.carrier N.carrier ⊤) (ψ : E' ≃L[𝕜] E) (S : N.FiniteSuccession) (p : (transportAlong g ψ S).last.carrier) : S.composite ((transportAlongStage g ψ S (Fin.last S.length)) p) = g ((transportAlong g ψ S).composite p)

The composite blow-down of the transported succession is g⁻¹ ∘ σ^r through the identification of the end results (Włodarczyk's σ^r [Wlo09, Theorem 2.0.3]; Hironaka's canonical modification [Hir64, p. 155]).