The Jacobian ledger #
The Jacobian clause of the principalization theorem — the Jacobian ideal of the blow-down times
the pull-back of the ideal is a normal-crossings divisor BM97, Theorem 1.10, the sentence after
it — is proved by carrying an inductive invariant along the sequence of blow-ups, a Jacobian
ledger: the Jacobian determinant of the composite Π : M_r → M, relative to the accumulated
exceptional divisor E_r on M_r, is at every point a unit times a monomial in the coordinates of
the exceptional components through the point, det D(x ∘ Π ∘ u⁻¹) = b(u) ∏_j u_j^{h_j} with b
a unit near u(a), h_j ∈ ℕ and h_j > 0 only for exceptional components. The one-blow-up input
is det = y_k^{codim − 1} in the blow-up chart (Hironaka/Manifold/Jacobian/BlowUp.lean).
The definition here is stalk-level and chart-free: the Jacobian of Π is the principal stalk
jacobianStalk Π x (spanned by the Jacobian determinant in any chart pair,
exists_stalk_jacobianStalk_eq_span_of_charts), so the unit b and the chart x at Π a of the
function form are absorbed by the ideal; the coordinates u_j of the components of E_r through
a generate their vanishing stalks in a simple normal crossings chart
(IsSncChartAt.mem_vanishingStalk_hyp_iff). JacobianLedger ψ f F exc (the map is written f,
Π being Lean's pi-notation token) therefore says: at every x of the source there is a simple
normal crossings chart of F at x, and there are finitely many members of F through x with
exponents, positive only on the exceptional members exc, whose vanishing stalks' powers multiply
to jacobianStalk Π x. In such a chart the stalk is generated by the monomial ∏ u_{c j}^{h j} —
the function form det = b · ∏ u_j^{h_j} is a corollary, not a second definition. The set
exc : Set F.ι marks the exceptional components: for the total transform along a sequence it is
the complement of the range of originalIdx (the strict transforms of the original members are the
non-exceptional ones, Kollár's total transform [Kol07, Definition 25]); for the empty start every
member is exceptional. The ledger is established along a blow-up sequence in
Hironaka/Resolution/Analytic/BM97/LedgerStep.lean and LedgerSequence.lean, and read off as the
Jacobian clause in Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean.
A Jacobian ledger for Π : M' → M relative to the hypersurface family F on M' with
exceptional members exc — at every point x of M' there is a simple normal crossings chart of
F at x, and finitely many members s of F through x with exponents h, positive only on
members of exc, such that the stalk of the Jacobian ideal of Π at x (jacobianStalk) is the
product of the powers (vanishing stalk of the member)^{h j}; in the chart, the monomial
∏ u_{c j}^{h j} in the coordinates of the members through x generates it. Stalk-level and
chart-free: units and the target chart are absorbed by the ideal. The inductive invariant behind
the Jacobian clause of [BM97, Theorem 1.10, the sentence after it].
Equations
- One or more equations did not get rendered due to their size.