The ideal-theoretic strict transforms along pull-backs and along the deletion of empty blow-ups

The independence of the local resolution of a piece from the chosen embedding [Kol07, Theorem 36, proof] compares the final ideal-theoretic strict transforms (FiniteSuccession.strictTransformSubspaceSeq) along the values of the embedded desingularization functor for two embeddings. The comparison transports them along the sequences that the functoriality clause of IsEmbeddedDesing (CommutesWithLocalIsos, the commutation with smooth morphisms of [Kol07, 34.1]) produces: the pull-back along a local analytic isomorphism g restricted onto its image, with the empty blow-ups deleted. This module proves the ideal-level counterparts of the corresponding transports of the set-level strict transforms and of the weak transforms:

• (A) saturationStalk_congr, strictTransformSubspace_congr: the strict transform strictTransformSubspace depends on the witnesses hY : IsClosedSubmanifold ψ Y c, h : IsBlowUp ψ Y c π only through the SET Y and the blow-down π (the ideal sheaf of a closed submanifold depends only on the set, IsClosedSubmanifold.idealSheaf_congr). A succession's witnesses isClosedSubmanifold_center i carry the chosen chart and codimension of its monoidality witness, so the constructor form of the recursion (cons_strictTransformSubspaceSeqAux_succ) is not rfl as it is for the weak transform (whose centre argument is the ideal sheaf itself); (A) bridges the two.
• (B) The pull-back of a blow-up sequence along a smooth morphism [Kol07, Definition 30.1] at the ideal level: along the lift liftStep of a SURJECTIVE local analytic isomorphism h : N → M to the blowings-up, the strict transform pulls back to the strict transform of the pull-back (strictTransformSubspace_comap_liftStep), then along a whole list (BlowUpSequence.pullback) in the ℕ-indexed, Fin-indexed and last-stage forms (strictTransformSubspaceSeqAux_pullback, strictTransformSubspaceSeq_pullback, strictTransformSubspaceSeq_last_pullbackLiftLast). The saturation stalks correspond under the bijective germ maps of the lift (saturationStalk_comap_liftStep: Ideal.map_colon_pow_of_bijective, totalTransform_comap_liftStep, exceptionalIdealSheaf_comap_liftStep); the two saturations take the same branch of the case distinction in strictTransformSubspace (hasLocalGenerators_saturationStalk_comap_liftStep_iff: local generators pull back, hasLocalGenerators_pullback, and descend along a surjective local isomorphism, HasLocalGenerators.of_map_germMap_of_surjective). The surjectivity of h is a hypothesis of the formalization forced by that sheaf-wide case distinction — a non-surjective h sees the branch on N while M may take the other branch off the image; the sources' statement is pointwise, and the map produced by the functoriality clause (restrictMap g U' (imageOpens g hg U')) is surjective.
• (C) Deleting the empty blow-ups [Kol07, 34.1]: the final strict transform along the cleaned list L.eraseEmpty is the pull-back along the isomorphism eraseEmptyLast⁻¹ of the last stages of the one along L (strictTransformSubspaceSeq_last_eraseEmpty, the counterpart of weakTransformSeq_last_eraseEmpty): an empty blowing-up is an isomorphism whose exceptional ideal sheaf is the unit ideal, so its strict transform is the pull-back (strictTransformSubspace_blowUpπ_of_eq_empty); the two saturations are then isomorphic sheaves and take one branch.
• (D) strictTransformSubspaceSeq_last_pullback_eraseEmpty: (B) at the last stage composed with (C), the exact right-hand side that the functoriality clause produces.
• (B′) The surjectivity of h in (B) and (D) was needed only for the coincidence of the branches; since every saturation has local generators (saturationStalk_hasLocalGenerators, SaturationFiniteType.lean), the condition of the case distinction is a theorem for every centre, blow-up and ideal sheaf (strictTransformSubspace_eq_ofStalks), so the identities hold along ANY local analytic isomorphism, the open inclusions of Kollár's proof included. The unconditional forms strictTransformSubspace_comap_liftStep', strictTransformSubspaceSeqAux_pullback', strictTransformSubspaceSeq_pullback', strictTransformSubspaceSeq_last_pullbackLiftLast', strictTransformSubspaceSeq_last_pullback_eraseEmpty' stand beside the surjective ones.

The strict transform of a closed subspace is the saturation of its total transform by the exceptional divisor [BM97, §3, Proposition 3.13]. Not in the sources; bookkeeping on the pull-back and deletion transports of the Functor modules and on the saturation stalks.

(A) The strict transform depends on its witnesses only through the set

theorem Hironaka.Manifold.saturationStalk_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {n n' c c' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {Y Y' : Set M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hY' : Manifold.IsClosedSubmanifold ψ' Y' c') (h' : Manifold.IsBlowUp ψ' Y' c' π) (e : Y = Y') (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : Manifold.saturationStalk hY h I = Manifold.saturationStalk hY' h' I

(A) The saturation stalks depend on the witnesses only through the centre set and the blow-down: the total transform depends only on π, the exceptional ideal sheaf only on the set (IsClosedSubmanifold.idealSheaf_congr).

theorem Hironaka.Manifold.strictTransformSubspace_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {n n' c c' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {Y Y' : Set M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hY' : Manifold.IsClosedSubmanifold ψ' Y' c') (h' : Manifold.IsBlowUp ψ' Y' c' π) (e : Y = Y') (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : Manifold.strictTransformSubspace hY h I = Manifold.strictTransformSubspace hY' h' I

(A) The strict transform strictTransformSubspace depends on the witnesses only through the centre set and the blow-down.

(B′) The strict transform always takes its ofStalks branch

theorem Hironaka.Manifold.strictTransformSubspace_eq_ofStalks {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : Manifold.strictTransformSubspace hY h I = Manifold.IdealSheaf.ofStalks (Manifold.structureSheaf 𝕜 E M') (Manifold.saturationStalk hY h I) ⋯

(B′) The strict transform strictTransformSubspace ALWAYS takes its ofStalks branch: the condition of its case distinction, that the saturation stalks have local generators, is a theorem for every centre, blow-up and ideal sheaf (saturationStalk_hasLocalGenerators).

(B) One step: the strict transform along the lift of a local isomorphism

theorem Hironaka.Manifold.saturationStalk_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (J : M.IdealSheaf) (q : (Manifold.blowUp ψ ⋯).carrier) : Manifold.saturationStalk ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J) q = Ideal.map (Manifold.germMap ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ q) (Manifold.saturationStalk hY ⋯ J ((AnalyticManifold.BlowUpSequence.liftStep h hh hY) q))

(B) at the stalks: the saturation stalks of the pulled-back ideal sheaf along the pulled-back blowing-up [Kol07, Definition 30.1] are the images of the saturation stalks under the bijective germ maps of the lift liftStep — colons by powers transport along a ring isomorphism (Ideal.map_colon_pow_of_bijective), the total transform and the exceptional ideal sheaf pull back (totalTransform_comap_liftStep, exceptionalIdealSheaf_comap_liftStep). No surjectivity is needed here.

theorem Hironaka.Manifold.hasLocalGenerators_saturationStalk_comap_liftStep_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (hs : Function.Surjective ⇑h) (J : M.IdealSheaf) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J)) ↔ Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk hY ⋯ J)

(B) For a SURJECTIVE h the two saturations take the same branch of the case distinction in strictTransformSubspace: local generators pull back along the lift (hasLocalGenerators_pullback) and descend along the surjective local isomorphism liftStep (HasLocalGenerators.of_map_germMap_of_surjective).

theorem Hironaka.Manifold.strictTransformSubspace_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (hs : Function.Surjective ⇑h) (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (Manifold.strictTransformSubspace hY ⋯ J) = Manifold.strictTransformSubspace ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J)

(B) The pull-back of a blow-up sequence [Kol07, Definition 30.1] at the ideal level, one step: along the lift of a SURJECTIVE local analytic isomorphism the strict transform pulls back to the strict transform of the pull-back — in the then branches by the stalk identity saturationStalk_comap_liftStep, in the else branches by ⊤ pulling back to ⊤, the branches coinciding by hasLocalGenerators_saturationStalk_comap_liftStep_iff.

theorem Hironaka.Manifold.strictTransformSubspace_comap_liftStep' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY) ⋯ (Manifold.strictTransformSubspace hY ⋯ J) = Manifold.strictTransformSubspace ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J)

(B′) strictTransformSubspace_comap_liftStep WITHOUT surjectivity: both sides take the ofStalks branch (strictTransformSubspace_eq_ofStalks), and the stalk identity saturationStalk_comap_liftStep never needed surjectivity.

theorem Hironaka.Manifold.strictTransformSubspace_comap_of_square {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (hs : Function.Surjective ⇑h) {S : Set N.carrier} (hS : Manifold.IsClosedSubmanifold ψ S c) (e : S = ⇑h ⁻¹' Y) (G : AnalyticMap (Manifold.blowUp ψ hS) (Manifold.blowUp ψ hY)) (hcomm : ∀ (q : (Manifold.blowUp ψ hS).carrier), (Manifold.blowUpπ ψ hY) (G q) = h ((Manifold.blowUpπ ψ hS) q)) (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑G ⋯ (Manifold.strictTransformSubspace hY ⋯ J) = Manifold.strictTransformSubspace hS ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ J)

(B) for any analytic G between the blowings-up lying over h with S = h⁻¹(Y): such a G is the lift (heq_liftStep_of_forall); the counterpart of weakTransform_comap_of_square.

The constructor form of the recursion of the ideal-theoretic strict transforms

theorem AnalyticManifold.FiniteSuccession.cons_strictTransformSubspaceSeqAux_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) (k : ℕ) (h : k + 1 < (cons ψ hY rest).length + 1) : (cons ψ hY rest).strictTransformSubspaceSeqAux J (k + 1) h = rest.strictTransformSubspaceSeqAux (Manifold.strictTransformSubspace hY ⋯ J) k ⋯

The recursion of the ideal-theoretic strict transforms on the constructor form, at the level of the ℕ-indexed auxiliary recursion (the counterpart of cons_weakTransformSeqAux_succ); the witnesses of the cons — the chosen chart and codimension of the monoidality witness of the first step, on the cosupport of hY.idealSheaf — are bridged to hY itself by strictTransformSubspace_congr.

(B) Along a list: the strict transforms of the pull-back by a surjective local

isomorphism

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeqAux_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Function.Surjective ⇑h → ∀ (J : M.IdealSheaf) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1), (L.pullback h hh).toSuccession.strictTransformSubspaceSeqAux (Manifold.IdealSheaf.pullback ⇑h ⋯ J) i hi' = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftAux h hh i hi hi') ⋯ (L.toSuccession.strictTransformSubspaceSeqAux J i hi)

(B) along a list [Kol07, Definition 30.1]: the ideal-theoretic strict transforms along h^* L, for a SURJECTIVE h, are the pull-backs along the lifts of the strict transforms along L (strictTransformSubspace_comap_liftStep at each step; the counterpart of boundarySeqAux_pullback).

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (J : M.IdealSheaf) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) ⟨↑i, ⋯⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLift h hh i) ⋯ (L.toSuccession.strictTransformSubspaceSeq J i)

(B), Fin-indexed (the counterpart of boundarySeq_pullback).

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeqAux_pullback' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1) : (L.pullback h hh).toSuccession.strictTransformSubspaceSeqAux (Manifold.IdealSheaf.pullback ⇑h ⋯ J) i hi' = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftAux h hh i hi hi') ⋯ (L.toSuccession.strictTransformSubspaceSeqAux J i hi)

(B′) strictTransformSubspaceSeqAux_pullback WITHOUT surjectivity.

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_pullback' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) ⟨↑i, ⋯⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLift h hh i) ⋯ (L.toSuccession.strictTransformSubspaceSeq J i)

(B′) strictTransformSubspaceSeq_pullback WITHOUT surjectivity.

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_pullbackLiftLast' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) : (L.pullback h hh).toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftLast h hh) ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length))

(B′) strictTransformSubspaceSeq_last_pullbackLiftLast WITHOUT surjectivity: (B) at the last stage along ANY local analytic isomorphism — the open inclusions of [Kol07, Theorem 36, proof] included.

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_pullbackLiftLast {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Function.Surjective ⇑h → ∀ (J : M.IdealSheaf), (L.pullback h hh).toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftLast h hh) ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length))

(B) at the last stage, along the bundled last-stage lift pullbackLiftLast (the counterpart of strictTransformSeq_last_pullbackLiftLast).

(C) Along the deletion of the empty blow-ups

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspace_blowUpπ_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) (J : M.IdealSheaf) : Manifold.strictTransformSubspace hY ⋯ J = Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hY) ⋯ J

(C), one step: the strict transform along the blowing-up of an EMPTY centre is the pull-back — the exceptional ideal sheaf is the unit ideal (idealSheaf_eq_top_of_eq_empty), so every colon is the total transform's stalk, which has local generators; the counterpart of weakTransform_blowUpπ_of_eq_empty.

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_stageOfEq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : BlowUpSequence ψ₀ M} (e : L₁ = L₂) (I : M.IdealSheaf) : L₂.toSuccession.strictTransformSubspaceSeq I (Fin.last L₂.toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(stageOfEq e).symm.toAnalyticMap ⋯ (L₁.toSuccession.strictTransformSubspaceSeq I (Fin.last L₁.toSuccession.length))

(C) transport along an equality of lists (the counterpart of weakTransformSeq_last_stageOfEq).

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) (Z : BlowUpSequence ψ₀ M) (J : N.IdealSheaf) : (map φ Z).toSuccession.strictTransformSubspaceSeq J (Fin.last (map φ Z).toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(mapLast φ Z).symm.toAnalyticMap ⋯ (Z.toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑φ.toAnalyticMap ⋯ J) (Fin.last Z.toSuccession.length))

(C) transport along a diffeomorphism and its lift to the last stages: the strict transform at the last stage of the transported list Z.map φ is the pull-back along (mapLast φ)⁻¹ of the strict transform of φ^* J at the last stage of Z (strictTransformSubspace_comap_of_square at each step; the counterpart of weakTransformSeq_last_map).

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (I : M.IdealSheaf) : L.eraseEmpty.toSuccession.strictTransformSubspaceSeq I (Fin.last L.eraseEmpty.toSuccession.length) = Manifold.IdealSheaf.pullback ⇑L.eraseEmptyLast.symm.toAnalyticMap ⋯ (L.toSuccession.strictTransformSubspaceSeq I (Fin.last L.toSuccession.length))

(C) Deleting the empty blow-ups [Kol07, 34.1], the ideal-level counterpart of strictTransformSeq_last_eraseEmpty and weakTransformSeq_last_eraseEmpty: the strict transform of I at the last stage of the cleaned list is the pull-back along eraseEmptyLast⁻¹ of the one at the last stage of the list — a kept step contributes the same strict transform on both sides, a deleted step the pull-back along the empty blowing-up (strictTransformSubspace_blowUpπ_of_eq_empty), which the transport of the cleaned tail along Bl_∅ M ≃ M absorbs (strictTransformSubspaceSeq_last_map).

(D) = (B) + (C): the shape the functoriality clause CommutesWithLocalIsos produces

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) (J : M.IdealSheaf) : (L.pullback h hh).eraseEmpty.toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).eraseEmpty.toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(L.pullback h hh).eraseEmptyLast.symm.toAnalyticMap ⋯ (Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftLast h hh) ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length)))

(D) The final strict transform along (h^* L).eraseEmpty — the right-hand side of the functoriality clause of IsEmbeddedDesing — is the pull-back of the final strict transform along L, through the last-stage lift and eraseEmptyLast⁻¹; h SURJECTIVE (the clause's restrictMap g U' (imageOpens g hg U') is).

theorem AnalyticManifold.BlowUpSequence.strictTransformSubspaceSeq_last_pullback_eraseEmpty' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) : (L.pullback h hh).eraseEmpty.toSuccession.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).eraseEmpty.toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(L.pullback h hh).eraseEmptyLast.symm.toAnalyticMap ⋯ (Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftLast h hh) ⋯ (L.toSuccession.strictTransformSubspaceSeq J (Fin.last L.toSuccession.length)))

(D′) strictTransformSubspaceSeq_last_pullback_eraseEmpty WITHOUT surjectivity: the value of the functoriality clause at ANY local analytic isomorphism — an OPEN INCLUSION W' ↪ W in particular — has its final strict transform pulled back from the one over the source, through the last-stage lift and eraseEmptyLast⁻¹.