The ideal-theoretic strict transforms along the push-forward of a blow-up sequence

Kollár pushes a blow-up sequence T of a closed submanifold S ⊆ X forward to a sequence j_* T of X whose centres are the carried centres Z_i^X = (j_i)_* Z_i^S, and declares that "for all practical purposes Z_i^X = Z_i^S" [Kol07, Definition 30.3]; the identification behind it is that S_{i+1} := Bl_{Z_i ∩ S_i} S_i is the birational (strict) transform of S_i in X_{i+1} [Kol07, Definition 30.2] (strictTransform_submanifold_eq_blowUp, BlowUp/Transform/StrictSmooth.lean). The comparison of the local resolutions of a piece for two embeddings needs the IDEAL-level content of the sentence for a closed subspace Y ⊆ S given by an ideal sheaf I ⊇ 𝓘_S of X: the strict transforms strictTransformSubspace of I along j_* T stay inside the carried S_i and restrict to the strict transforms of I|_S along T itself. This module proves it. Labels used below: (A) the containment 𝓘_{S'} ≤ Yt, (A′) its consequence off S', (S) and (S′) the saturation identities, (C) the branch coincidence, (B) the restriction identity, (Q) the diffeomorphism square.

The one-step core (section PushforwardStep)

For one blowing-up σ : X' → X along Y ⊆ S with S' := strictTransformSet σ Y S (a closed submanifold) and the restricted blow-down σ|_{S'} : S' → S (a blowing-up of the bundled S along Y, isBlowUp_restrictMap), write ρ_p : 𝒪_{X',p} → 𝒪_{S',p} for the restriction of germs at p ∈ S' — surjective (germMap_inclusionMap_surjective) with kernel 𝓘_{S',p} (stalkIdeal_idealSheaf_of_mem).

• idealSheaf_strictTransform_le_strictTransformSubspace (A): 𝓘_{S'} ≤ Yt, the strict transform of I lies inside S' — from the inclusion 𝓘_{S'} ≤ saturation(σ^*𝓘_S) (idealSheaf_strictTransform_stalkIdeal_le_saturationStalk, the adapted-chart computation σ^*𝓘_S = 𝓘_{S'} · 𝓘_E) and the monotonicity of the saturation in the ideal; trivial in the ⊤ branch. Its stalk form 𝓘_{S',p} ≤ Sat_X(I)_p is the INPUT of the colon step below: the kernel of ρ_p lies in the saturation.
• saturationStalk_restrictMap_eq_map (S): Sat_S(I|_S)_p = ρ_p(Sat_X(I)_p). The exceptional stalk is principal, 𝓘_{E,p} = (u) (exists_stalkIdeal_totalTransform_self_eq_span_singleton); k = 0 is the pull-back identity σ|_{S'}^*(I|_S) = (σ^*I)|_{S'}; for k ≥ 1 a germ g with u^k g ∈ σ^*I restricts into (σ^*I|_{S'} : ρ(u)^k), and conversely a lift g of h ∈ (σ^*I|_{S'} : ρ(u)^k) has u^k g ∈ σ^*I + 𝓘_{S'} ⊆ Sat_X(I), so g ∈ Sat_X(I) (the saturation is saturated: u^m x ∈ Sat ⇒ x ∈ Sat).
• comap_saturationStalk_restrictMap (S′): Sat_X(I)_p = ρ_p⁻¹(Sat_S(I|_S)_p) (the kernel lies in Sat_X), and saturationStalk_eq_top_of_notMem_strictTransform_of_le (A′): off S' the saturation is the unit ideal (𝓘_{S',p} = ⊤ ≤ Sat_X(I)_p).
• hasLocalGenerators_saturationStalk_restrictMap_iff (C), the BRANCH COINCIDENCE of the if in the definition of strictTransformSubspace: Sat_X(I) has local generators iff Sat_S(I|_S) has. Generators RESTRICT (hasLocalGenerators_pullback on ofStalks, ρ(ρ⁻¹J) = J) and LIFT: near p ∈ S' the S'-generators' germs lift along the surjective ρ_p to germs of X', represented by sections agreeing with the generators near p (TopCat.Presheaf.germ_eq); together with local generators of 𝓘_{S'} (which are ⊤ at the nearby points off S') they generate ρ_q⁻¹(Sat_S) = Sat_X at every nearby q; off S' the single section 1 generates on the open S'ᶜ. No finite-type input is needed: the result holds over every RCLike field.
• strictTransformSubspace_pullback_inclusionMap (B), UNCONDITIONAL: (strict transform of I along σ)|_{S'} = strict transform of I|_S along σ|_{S'} — in the then branches by (S), in the else branches by ⊤ pulling back to ⊤, the branches coinciding by (C).

The diffeomorphism square (section DiffeoSquare) — (Q)

T's stage i+1 is blown up along the GIVEN T.map i, the core along the restricted blow-down; the unique diffeomorphism PushforwardStage.blowUpStep.iso : T_{i+1} ≃ S_{i+1} lies over e_i : T_i ≃ S_i (restrictMap_blowUpStep_iso). strictTransformSubspace_comap_of_diffeomorph_square carries the strict transform across any such square of blow-up models of the same centre (saturationStalk_comap_of_diffeomorph_square at the sheaf level: bijective germ maps, the exceptional ideal sheaf by comap_idealSheaf_of_isLocalDiffeomorph and idealSheaf_congr, the branches by hasLocalGenerators_pullback / HasLocalGenerators.of_map_germMap_of_surjective).

The chain (namespace AnalyticManifold.FiniteSuccession)

isClosedSubmanifold_range_pushforwardIncl types the carried S_i = j_i(T_i) on the stage; (A) idealSheaf_range_pushforwardIncl_le_strictTransformSubspaceSeq, (B) strictTransformSubspaceSeq_pushforward_pullback_incl and (C) hasLocalGenerators_saturationStalk_pushforward_iff follow by ONE induction on the stage (strictTransformSubspaceSeq_pushforward_aux: (A) ∧ (B) at stage i; the step is the core at P := pushforwardAux i with I := Yt^X_i, its hypothesis 𝓘_{S_i} ≤ Yt^X_i the (A) of the previous stage, the branch coincidence (C) of the step supplying both then/else cases, and the square (Q) carrying the result from the restricted blow-down to T.map i; stage 0 is J := I|_S, pushforwardIncl_zero). The witnesses of the push-forward at a step are its CHOSEN chart and codimension on the cosupport of the carried centre; strictTransformSubspace_congr bridges them to pushforwardCenterOfSub (support_pushforwardCenterOf).

Sources: [Kol07, Definitions 30.2–30.3]; the saturation is that of [BM97, §3, Proposition 3.13]. The proofs are bookkeeping of the printed steps; not in the sources.

(Q) The diffeomorphism square of two blow-up models of the same centre

theorem Hironaka.Manifold.saturationStalk_comap_of_diffeomorph_square {𝕜 : Type} [RCLike 𝕜] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ψ : F ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ M₁' M₂' : AnalyticManifold 𝕜 F} {Y₁ : Set M₁.carrier} {Y₂ : Set M₂.carrier} {c : ℕ} {π₁ : M₁'.carrier → M₁.carrier} {π₂ : M₂'.carrier → M₂.carrier} (hY₁ : Manifold.IsClosedSubmanifold ψ Y₁ c) (h₁ : Manifold.IsBlowUp ψ Y₁ c π₁) (hY₂ : Manifold.IsClosedSubmanifold ψ Y₂ c) (h₂ : Manifold.IsBlowUp ψ Y₂ c π₂) (g : Diffeomorph (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 F) M₁.carrier M₂.carrier ⊤) (hg : ⇑g '' Y₁ = Y₂) (g' : Diffeomorph (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 F) M₁'.carrier M₂'.carrier ⊤) (hsq : ∀ (p : M₁'.carrier), π₂ (g' p) = g (π₁ p)) (I₂ : M₂.IdealSheaf) (p : M₁'.carrier) : Manifold.saturationStalk hY₁ h₁ (Manifold.IdealSheaf.pullback ⇑g.toAnalyticMap ⋯ I₂) p = Ideal.map (Manifold.germMap ⇑g'.toAnalyticMap ⋯ p) (Manifold.saturationStalk hY₂ h₂ I₂ (g'.toAnalyticMap p))

The saturation stalks across a DIFFEOMORPHISM square (the saturation half of (Q)): two blowings-up π₁ : M₁' → M₁ along Y₁, π₂ : M₂' → M₂ along Y₂ = g(Y₁), and a diffeomorphism g' of the blow-ups over g — the saturation stalks of g^*I₂ along π₁ are the images of the saturation stalks of I₂ along π₂ under the bijective germ maps of g'.

theorem Hironaka.Manifold.hasLocalGenerators_saturationStalk_comap_of_diffeomorph_square_iff {𝕜 : Type} [RCLike 𝕜] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ψ : F ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ M₁' M₂' : AnalyticManifold 𝕜 F} {Y₁ : Set M₁.carrier} {Y₂ : Set M₂.carrier} {c : ℕ} {π₁ : M₁'.carrier → M₁.carrier} {π₂ : M₂'.carrier → M₂.carrier} (hY₁ : Manifold.IsClosedSubmanifold ψ Y₁ c) (h₁ : Manifold.IsBlowUp ψ Y₁ c π₁) (hY₂ : Manifold.IsClosedSubmanifold ψ Y₂ c) (h₂ : Manifold.IsBlowUp ψ Y₂ c π₂) (g : Diffeomorph (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 F) M₁.carrier M₂.carrier ⊤) (hg : ⇑g '' Y₁ = Y₂) (g' : Diffeomorph (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 F) M₁'.carrier M₂'.carrier ⊤) (hsq : ∀ (p : M₁'.carrier), π₂ (g' p) = g (π₁ p)) (I₂ : M₂.IdealSheaf) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk hY₁ h₁ (Manifold.IdealSheaf.pullback ⇑g.toAnalyticMap ⋯ I₂)) ↔ Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk hY₂ h₂ I₂)

The two saturations take the same branch of the if in strictTransformSubspace (g' is a surjective local isomorphism) — the branch half of (Q).

theorem Hironaka.Manifold.strictTransformSubspace_comap_of_diffeomorph_square {𝕜 : Type} [RCLike 𝕜] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {ψ : F ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ M₁' M₂' : AnalyticManifold 𝕜 F} {Y₁ : Set M₁.carrier} {Y₂ : Set M₂.carrier} {c : ℕ} {π₁ : M₁'.carrier → M₁.carrier} {π₂ : M₂'.carrier → M₂.carrier} (hY₁ : Manifold.IsClosedSubmanifold ψ Y₁ c) (h₁ : Manifold.IsBlowUp ψ Y₁ c π₁) (hY₂ : Manifold.IsClosedSubmanifold ψ Y₂ c) (h₂ : Manifold.IsBlowUp ψ Y₂ c π₂) (g : Diffeomorph (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 F) M₁.carrier M₂.carrier ⊤) (hg : ⇑g '' Y₁ = Y₂) (g' : Diffeomorph (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 F) M₁'.carrier M₂'.carrier ⊤) (hsq : ∀ (p : M₁'.carrier), π₂ (g' p) = g (π₁ p)) (I₂ : M₂.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑g'.toAnalyticMap ⋯ (Manifold.strictTransformSubspace hY₂ h₂ I₂) = Manifold.strictTransformSubspace hY₁ h₁ (Manifold.IdealSheaf.pullback ⇑g.toAnalyticMap ⋯ I₂)

(Q) The strict transform transports along a diffeomorphism square of blow-up models: g'^* (strict transform of I₂ along π₂) = strict transform of g^*I₂ along π₁ — branch by branch, UNCONDITIONAL. Used at each step of the chain to pass from the restricted blow-down S_{i+1} → S_i (the core's model) to the given T.map i through the unique diffeomorphism PushforwardStage.blowUpStep.iso (restrictMap_blowUpStep_iso).

The core: one blowing-up of M along Y ⊆ S, restricted to the strict transform S'

theorem Hironaka.Manifold.idealSheaf_strictTransform_stalkIdeal_le_saturationStalk_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) (p : M') : ⋯.idealSheaf.stalkIdeal p ≤ Manifold.saturationStalk hY h I p

The stalk form of (A): the ideal of the strict transform S' lies in the saturation of σ^*I at every point — the inclusion 𝓘_{S'} ≤ saturation(σ^*𝓘_S) (the adapted-chart computation) and the monotonicity of the saturation in the ideal.

theorem Hironaka.Manifold.idealSheaf_strictTransform_le_strictTransformSubspace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) : ⋯.idealSheaf ≤ Manifold.strictTransformSubspace hY h I

(A) core ("Z_i^X = Z_i^S" of [Kol07, Definition 30.3] made explicit: the strict transform of a subspace of S stays in the strict transform S' of S): 𝓘_{S'} ≤ the strict transform of I — from 𝓘_{S'} = saturation of σ^*𝓘_S ≤ saturation of σ^*I ([Kol07, Definition 30.2], strictTransform_submanifold_eq_blowUp); trivial in the ⊤ branch.

theorem Hironaka.Manifold.saturationStalk_eq_top_of_notMem_strictTransform_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) {p : M'} (hp : p ∉ Manifold.strictTransformSet π Y S) : Manifold.saturationStalk hY h I p = ⊤

(A′) core: off the strict transform S' the saturation of σ^*I is the unit ideal (the ideal of S' is the unit ideal there and lies in the saturation).

theorem Hironaka.Manifold.mem_saturationStalk_of_pow_mul_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {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} {Y : Set M} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {p : M'} {u : ↑((Manifold.structureSheaf 𝕜 E M').presheaf.stalk p)} (hu : (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal p = Ideal.span {u}) {m : ℕ} {x : ↑((Manifold.structureSheaf 𝕜 E M').presheaf.stalk p)} (hx : x * u ^ m ∈ Manifold.saturationStalk hY h I p) : x ∈ Manifold.saturationStalk hY h I p

The saturation is saturated: if u^m x lies in ⋃_k (σ^*I : (u)^k), u generating the exceptional stalk, so does x (the union is directed).

theorem Hironaka.Manifold.saturationStalk_restrictMap_eq_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) (p : ⋯.toAnalyticManifold.carrier) : Manifold.saturationStalk ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) p = Ideal.map (Manifold.germMap ⇑⋯.inclusionMap ⋯ p) (Manifold.saturationStalk hY h I (⋯.inclusionMap p))

(S) core: at a point p ∈ S' the saturation of σ|_{S'}^*(I|_S) by the exceptional divisor of S' → S is the IMAGE of the saturation of σ^*I under the surjective restriction 𝒪_{M',p} → 𝒪_{S',p} (germMap_inclusionMap_surjective): k = 0 is the pull-back identity, k ≥ 1 the colon step (σ^*I : 𝓘_E^k) ↦ (σ^*I|_{S'} : 𝓘_{E_S}^k) with (A) at the step — 𝓘_{S'} ≤ Sat_X(I) from 𝓘_{S'} · 𝓘_E = σ^*𝓘_S ≤ σ^*I — as the input that lets the kernel drop out.

theorem Hironaka.Manifold.comap_saturationStalk_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) (p : ⋯.toAnalyticManifold.carrier) : Ideal.comap (Manifold.germMap ⇑⋯.inclusionMap ⋯ p) (Manifold.saturationStalk ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) p) = Manifold.saturationStalk hY h I (⋯.inclusionMap p)

(S′) core: the saturation of σ^*I at p ∈ S' is the PREIMAGE of the saturation on S' (it contains the kernel 𝓘_{S'} by (A)).

theorem Hironaka.Manifold.hasLocalGenerators_saturationStalk_restrictMap_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk hY h I) ↔ Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I))

(C) core, the BRANCH COINCIDENCE of the if in strictTransformSubspace: the saturation of σ^*I on M' has local generators iff the saturation of σ|_{S'}^*(I|_S) on S' has — generators LIFT (the S'-generators' local representatives along the closed embedding, together with the adapted coordinates generating 𝓘_{S'}, which also give ⊤ at the nearby points off S') and RESTRICT (the restriction is surjective on stalks, ρ(ρ⁻¹ J) = J). No finite-type input is needed.

theorem Hironaka.Manifold.strictTransformSubspace_pullback_inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hYS : Y ⊆ S) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hI : hS.idealSheaf ≤ I) : Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ (Manifold.strictTransformSubspace hY h I) = Manifold.strictTransformSubspace ⋯ ⋯ (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I)

(B) core, UNCONDITIONAL ([Kol07, Definitions 30.2–30.3]): the strict transform of I ⊇ 𝓘_S under σ = Bl_Y M → M, restricted to the strict transform S' = Bl_Y S, is the strict transform of I|_S under the restricted blowing-up σ|_{S'} : S' → S — in the then branches by (S), in the else branches by ⊤ pulling back to ⊤, the branches coinciding by (C).

Along the push-forward j_* T of a sequence of the bundled S

theorem AnalyticManifold.FiniteSuccession.isClosedSubmanifold_range_pushforwardIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin (T.length + 1)) : Manifold.IsClosedSubmanifold ψ (Set.range ⇑(pushforwardIncl hS T i)) s

The carried S_i = j_i(T_i) ⊆ X_i as a closed submanifold of the stage X_i of the push-forward, typed on the stage (the pushforwardAux witness, read through range_incl).

theorem AnalyticManifold.FiniteSuccession.strictTransformSubspaceSeq_pushforward_step {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (j : ℕ) (hj : j < T.length) (P : Manifold.PushforwardStage ψ s (T.stage ⟨j, hj⟩.castSucc)) (Yt : P.space.IdealSheaf) (hle : ⋯.idealSheaf ≤ Yt) (hIH : Manifold.IdealSheaf.pullback ⇑P.incl ⋯ Yt = T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) ⟨j, hj⟩.castSucc) : Manifold.IdealSheaf.pullback ⇑(Manifold.IsBlowUp.diffeomorph ⋯ ⋯ ⋯).toAnalyticMap ⋯ (Manifold.IdealSheaf.pullback ⇑⋯.inclusionMap ⋯ (Manifold.strictTransformSubspace ⋯ ⋯ Yt)) = T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) ⟨j, hj⟩.succ ∧ ⋯.idealSheaf ≤ Manifold.strictTransformSubspace ⋯ ⋯ Yt

One step of the chain, on a stage datum P at the given stage T_j (PushforwardStage; the induction instantiates P := pushforwardAux j): from the strict transform Yt of I on P.space containing 𝓘_{S_j} and restricting to the T-chain's Y_j, the same two facts on P.blowUpStep — the core (A)/(B) at P and the diffeomorphism square (Q) from the restricted blow-down to the given T.map j.

theorem AnalyticManifold.FiniteSuccession.hasLocalGenerators_saturationStalk_pushforward_step {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (j : ℕ) (hj : j < T.length) (P : Manifold.PushforwardStage ψ s (T.stage ⟨j, hj⟩.castSucc)) (Yt : P.space.IdealSheaf) (hle : ⋯.idealSheaf ≤ Yt) (hIH : Manifold.IdealSheaf.pullback ⇑P.incl ⋯ Yt = T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) ⟨j, hj⟩.castSucc) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ Yt) ↔ Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) ⟨j, hj⟩.castSucc))

One step of the branch coincidence along the chain, on a stage datum P at T_j: the core (C) at P, the restricted blow-down's witnesses read as isBlowUp_restrictMap_imageVal's, and the square (Q) to the given T.map j.

theorem AnalyticManifold.FiniteSuccession.strictTransformSubspaceSeq_pushforward_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (hI : hS.idealSheaf ≤ I) (i : ℕ) (hi : i < T.length + 1) : Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T ⟨i, hi⟩) ⋯ ((pushforward hS T).strictTransformSubspaceSeq I ⟨i, hi⟩) = T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) ⟨i, hi⟩ ∧ ⋯.idealSheaf ≤ (pushforward hS T).strictTransformSubspaceSeq I ⟨i, hi⟩

The chain, ℕ-indexed: (B) ∧ (A) at every stage, by ONE induction on the stage ((B) at i + 1 needs (A) at i as the core's hypothesis and (B) at i for the identification of the inputs).

theorem AnalyticManifold.FiniteSuccession.idealSheaf_range_pushforwardIncl_le_strictTransformSubspaceSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (hI : hS.idealSheaf ≤ I) (i : Fin (T.length + 1)) : ⋯.idealSheaf ≤ (pushforward hS T).strictTransformSubspaceSeq I i

(A) Along the push-forward j_* T [Kol07, Definition 30.3] the strict transform of I ⊇ 𝓘_S stays inside the carried S_i: 𝓘_{S_i} ≤ Ỹ^X_i at every stage (stage 0 is the hypothesis).

theorem AnalyticManifold.FiniteSuccession.strictTransformSubspaceSeq_pushforward_pullback_incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (hI : hS.idealSheaf ≤ I) (i : Fin (T.length + 1)) : Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T i) ⋯ ((pushforward hS T).strictTransformSubspaceSeq I i) = T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) i

(B) UNCONDITIONAL ("for all practical purposes Z_i^X = Z_i^S", [Kol07, Definition 30.3]): the strict transform of I along the push-forward, restricted to the carried S_i through j_i : T_i ↪ X_i, is the strict transform of I|_S along T itself — one induction on the stage with (C) (both chains take the same branch at each step; stage 0 is J := I|_S).

theorem AnalyticManifold.FiniteSuccession.hasLocalGenerators_saturationStalk_pushforward_iff_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (hI : hS.idealSheaf ≤ I) (j : ℕ) (hj : j < T.length) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((pushforward hS T).strictTransformSubspaceSeq I ⟨j, hj⟩.castSucc)) ↔ Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) ⟨j, hj⟩.castSucc))

The branch coincidence along the chains, ℕ-indexed (the Fin form below): at step j the saturation of the X-chain has local generators iff the saturation of the S-chain has.

theorem AnalyticManifold.FiniteSuccession.hasLocalGenerators_saturationStalk_pushforward_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (I : M.IdealSheaf) (hI : hS.idealSheaf ≤ I) (i : Fin T.length) : Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((pushforward hS T).strictTransformSubspaceSeq I i.castSucc)) ↔ Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (T.strictTransformSubspaceSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) i.castSucc))

(C) The BRANCH COINCIDENCE along the chains: at every step the saturation of the X-chain has local generators iff the saturation of the S-chain has (the core (C) at the step, the two chains' inputs identified by (B) at the previous stage).