The step of the Jacobian ledger along one blow-up

From a Jacobian ledger for f : M' → M relative to a simple normal crossings family F with exceptional members exc, a centre Z ⊆ M' having simple normal crossings with F, and the blowing-up π : M'' → M' of Z, a ledger for f ∘ π relative to the total transform F.totalTransform π Z, the exceptional members being the strict transforms of exc together with the new exceptional divisor π⁻¹(Z) (JacobianLedger.step; the condition on the centres is Kollár's "the centers Z_i have simple normal crossings with E" [Kol07, Definition 25]).

The proof is the chain rule at the stalks (jacobianStalk_comp of Hironaka/Manifold/Jacobian/Comp.lean: jacobianStalk (f ∘ π) p = (jacobianStalk f (π p)).map (germMap π p) · jacobianStalk π p) with the two factors read at p. On the centre (π p ∈ Z): the simple normal crossings hypothesis gives an adapted chart of Z at π p that is a simple normal crossings chart of F, IsBlowUp.cover a blow-up chart through p; germMap_prod_vanishingStalk_pow_totalTransform (Hironaka/Resolution/Analytic/BM97/LedgerBlowUp.lean) transports the old monomial to the strict transforms with the exceptional exponent ∑ e_j over the members through the block, and jacobianStalk_blowUp reads jacobianStalk π p = (u_{σ i})^{c-1}, the vanishing stalk of π⁻¹(Z) at p to the power c − 1 (IsClosedSubmanifold.vanishingStalk_eq_span_coord on the adapted chart IsBlowUpChart.isAdaptedChart_preimage). Off the centre: π is a local analytic isomorphism at p (IsBlowUp.isLocalDiffeomorphOn_compl), so jacobianStalk π p = ⊤ (jacobianStalk_eq_top_of_isLocalDiffeomorphAt) and the strict transforms coincide with the preimages near p (HypersurfaceFamily.mem_strictTransform_iff_of_notMem); vanishingStalk_preimage_of_isLocalDiffeomorphAt' carries each member's vanishing stalk at π p to the strict transform's at p. In both cases the members whose strict transform misses p contribute the unit ideal (vanishingStalk_eq_top_of_notMem) and are dropped from the index set (Finset.prod_filter_of_ne), so the ledger's clause "x ∈ F.hyp j for j ∈ s" holds; the exponent of a strict transform is the member's, that of the exceptional divisor is the block sum plus c − 1; positivity of an exponent puts the member in exc or it is the exceptional divisor. This is the inductive step of Hironaka/Resolution/Analytic/BM97/LedgerSequence.lean; the one-blow-up computation it rests on is Bierstone–Milman's f'(w', z') = (z'_1)^{-d} f(…) in a blow-up chart [BM97, §3, "The strict transform"].

theorem Hironaka.Manifold.JacobianLedger.step {𝕜 : 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'] {M'' : Type u} [TopologicalSpace M''] [ChartedSpace E M''] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M''] [T2Space M''] [SecondCountableTopology M''] {f : M' → M} (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) {F : Manifold.HypersurfaceFamily M'} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {exc : Set F.ι} (hL : JacobianLedger ψ f F exc) {Z : Set M'} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ Z c) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Z c) {π : M'' → M'} (h : Manifold.IsBlowUp ψ Z c π) : JacobianLedger ψ (f ∘ π) (Manifold.HypersurfaceFamily.totalTransform π Z F) ((fun (j : F.ι) => toLex (Sum.inl j)) '' exc ∪ {toLex (Sum.inr PUnit.unit)})

The step of the Jacobian ledger along one blow-up ([Kol07, Definition 25]): a ledger for f relative to (F, exc), a centre Z having simple normal crossings with F and the blowing-up π of Z give a ledger for f ∘ π relative to F.totalTransform π Z, the exceptional members being the strict transforms of exc and the new exceptional divisor. Chain rule (jacobianStalk_comp), then on the centre germMap_prod_vanishingStalk_pow_totalTransform at a blow-up chart through p with jacobianStalk_blowUp, off it the local-isomorphism transport (vanishingStalk_preimage_of_isLocalDiffeomorphAt') with jacobianStalk π p = ⊤.