The chain rule for the Jacobian stalk #
For a composite of blow-ups, det DΠ_r = (det DΠ_{r−1} ∘ π_{r−1}) · det Dπ_{r−1} (the chain rule
and the multiplicativity of the determinant), so that the Jacobian ideal of a composite is the
product of the pull-back of the outer Jacobian ideal and the inner one. At the stalks of the
Jacobian ideal (jacobianStalk) this is
jacobianStalk (g ∘ f) a = (jacobianStalk g (f a)).map (germMap f a) · jacobianStalk f a
(jacobianStalk_comp): the chart representative of g ∘ f in charts χ (target) and φ
(source) is, near φ a, the composite of the representatives of g (charts χ, θ) and of f
(charts θ, φ) through an intermediate chart θ at f a (jacobianFun_comp, the pointwise
chain rule, proved as fderiv_chartRep_eq is), so the Jacobian determinants multiply pointwise;
exists_stalk_jacobianStalk_eq_span_of_charts turns the three determinant germs into generators
of the three stalks, and stalkToGerm_germMap identifies the pulled-back germ with the composite
function germ. Corollaries: when one factor is a local diffeomorphism at the point its Jacobian
stalk is the unit ideal (jacobianStalk_eq_top_of_isLocalDiffeomorphAt), so the composite's stalk
is the other factor's (transported along the stalk map, for the inner factor). The chain rule is
the step of the Jacobian ledger along a blow-up sequence
(Hironaka/Resolution/Analytic/BM97/LedgerStep.lean), and the corollaries transport the ledger
along the open embeddings and inclusions of the gluing
(Hironaka/Resolution/Analytic/BM97/LedgerLimit.lean). The Jacobian clause itself is BM97, Theorem
1.10, the sentence after it.
The pointwise chain rule: the Jacobian determinant of g ∘ f in charts χ (target) and φ
(source) at a point is the product of the determinants of g (charts χ, θ) at f y and of f
(charts θ, φ) at y, for any chart θ at f y — fderiv_comp on the local identity
χ ∘ (g ∘ f) ∘ φ⁻¹ = (χ ∘ g ∘ θ⁻¹) ∘ (θ ∘ f ∘ φ⁻¹) and det_clm_comp.
The chain rule for the Jacobian stalk:
jacobianStalk (g ∘ f) a = (jacobianStalk g (f a)).map (germMap f a) · jacobianStalk f a — the
three stalks are principal, generated by the determinant germs in the standard charts, and
jacobianFun_comp multiplies the germs.
When the outer map is a local diffeomorphism at f a, the composite's Jacobian stalk is the
inner map's (the case of an open inclusion after a blow-down).
When the inner map is a local diffeomorphism at a, the composite's Jacobian stalk is the
transport of the outer map's along the inner map's stalk map (the case of a glued blow-down after
the open embedding of a piece).