The Jacobian stalk of the glued blow-down on a piece

The blow-down σ : M̃ → M of the principalization theorem is glued from the blow-downs of the pieces of a compact exhaustion: Włodarczyk glues the Ũ_i = prin⁻¹(U_i) over a cover by relatively compact opens into a manifold M̃ with a proper bimeromorphic prin : M̃ → M [Wlo09, §4.1]; Kollár passes from neighbourhoods of compact sets to "any analytic space that is an increasing union of its compact subsets" [Kol07, 44]. Here σ is CompatibleFamily.limitBlowDown, the direct limit of the pieces' composites Π^{(m)} : M'_m → M_m ⊆ M along the analytic open embeddings ι_m = toLimitMap m : M'_m → M̃. At a point q of the piece m, the Jacobian stalk of σ at ι_m q, transported along the bijective germ map of ι_m, is the Jacobian stalk of the piece's composite σ^{(m)} at q (CompatibleFamily.jacobianStalk_limitBlowDown_toLimitMap): σ ∘ ι_m = Π^{(m)} = inclusion ∘ σ^{(m)} (limitDesc_comp_toLimitMap, the definition of blowDownOn), and the chain rule (Hironaka/Manifold/Jacobian/Comp.lean) keeps the piece's stalk because ι_m and the inclusion M_m ⊆ M are local analytic isomorphisms (isAnalyticOpenEmbedding_toLimitMap, isLocalDiffeomorph_inclusion; their Jacobian stalks are ⊤). With the Jacobian ledger of each piece (Hironaka/Resolution/Analytic/BM97/LedgerSequence.lean) this gives the ledger of σ at every point of M̃ (every point lies in some piece, toLimit_surjective), which the Jacobian clause of the principalization theorem reads pointwise (Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean).

theorem Hironaka.Manifold.CompatibleFamily.jacobianStalk_limitBlowDown_toLimitMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} (C : CompatibleFamily T) (Kex : CompactExhaustion M.carrier) (hemb : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂), Manifold.IsAnalyticOpenEmbedding (C.endResultEmbedding hU₁ hU₂ h)) (hcomp : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) (p : ((C.seqOn U₁ hU₁).stage (Fin.last (C.seqOn U₁ hU₁).length)).carrier), (C.seqOn U₂ hU₂).toSuccession.composite ((C.endResultEmbedding hU₁ hU₂ h) p) = (M.restrictLE h) ((C.seqOn U₁ hU₁).toSuccession.composite p)) (m : ℕ) (q : (C.endResultOn Kex m).carrier) : Ideal.map (Manifold.germMap ⇑((C.endResultChain Kex hemb).toLimitMap m) ⋯ q) (Manifold.jacobianStalk (⇑(C.limitBlowDown Kex hemb hcomp)) (((C.endResultChain Kex hemb).toLimitMap m) q)) = Manifold.jacobianStalk (⇑(C.seqOn (Manifold.relCompactOpen Kex m) ⋯).toSuccession.composite) q

The Jacobian stalk of the glued blow-down on a piece: the Jacobian stalk of σ = C.limitBlowDown Kex hemb hcomp at a point of the piece m, transported along the analytic open embedding ι_m = toLimitMap m, is the Jacobian stalk of the piece's composite σ^{(m)} — σ ∘ ι_m = Π^{(m)} = inclusion ∘ σ^{(m)} (limitDesc_comp_toLimitMap and the definition of blowDownOn), and the chain rule keeps the piece's stalk because ι_m and the inclusion are local diffeomorphisms, with Jacobian stalk ⊤ (the two corollaries jacobianStalk_comp_of_isLocalDiffeomorphAt_right and _left of the chain rule). The gluing of the local principalizations is [Wlo09, §4.1].