The Jacobian determinant of the blowing-up

In a blow-up chart Φ of index i over an adapted chart φ of the centre (the charts V'_i of Bierstone–Milman's blowing-up, in which π reads x_i = ξ_i, x_j = ξ_i ξ_j for j ≠ i [BM88, Definition 4.1]), the chart representative of the blowing-up is the chart map π_i of the model blow-up conjugated by the coordinates ψ (IsBlowUpChart.comm: ψ ∘ φ ∘ π = π_i ∘ ψ ∘ Φ on Φ.source, so φ ∘ π ∘ Φ⁻¹ = ψ⁻¹ ∘ π_i ∘ ψ on Φ.target), whose Jacobian determinant is u_{σ i}^{c-1} (det_fderiv_blowUpChartMap of Hironaka/Manifold/BlowUp/Jacobian.lean); conjugation by a linear isomorphism does not change the determinant (LinearMap.det_conj). Hence:

• jacobianFun_blowUpChart: J_{φ,Φ}(p) = ψ(Φ p)_{σ i}^{c-1} on Φ.source;
• jacobianStalk_blowUp: the stalk of the Jacobian ideal at a point of a blow-up chart of index i is (u_{σ i}^{c-1}), u_{σ i} the scaling coordinate germ (coord) — by the any-chart form exists_stalk_jacobianStalk_eq_span_of_charts of Hironaka/Manifold/Jacobian/Units.lean applied to the chart pair (φ, Φ), the germ of J_{φ,Φ} being that of u_{σ i}^{c-1}.

Boundary cases: c = 0 and c = 1 give exponent 0 and the unit ideal; off the exceptional divisor u_{σ i} is a unit, so the stalk is the unit ideal there too, as jacobianStalk_eq_top_of_isLocalDiffeomorphAt says directly. This is the one-blow-up computation det = y^{codim − 1} behind the Jacobian clause of the principalization theorem [BM97, Theorem 1.10, the sentence after it]; the ideal-sheaf form is Hironaka/Manifold/Jacobian/Bundled.lean.

theorem Manifold.jacobianFun_blowUpChart {𝕜 : 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'] {Y : Set M} {c : ℕ} {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) : jacobianFun 𝕜 π φ Φ p = ψ (↑Φ p) (σ i) ^ (c - 1)

In a blow-up chart Φ of index i over the adapted chart φ, the Jacobian determinant of π in the charts (φ, Φ) is u_{σ i}^{c-1} (the chart formulas of [BM88, Definition 4.1]): the chart representative is ψ⁻¹ ∘ π_i ∘ ψ (IsBlowUpChart.comm), and conjugation by ψ does not change the determinant.

theorem Manifold.jacobianStalk_blowUp {𝕜 : 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'] {Y : Set M} {c : ℕ} {π : M' → M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (h : IsBlowUp ψ Y c π) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) : jacobianStalk π p = Ideal.span {coord E ψ Φ ⋯ hp (σ i) ^ (c - 1)}

At a point p of a blow-up chart Φ of index i, the stalk of the Jacobian ideal of the blowing-up is generated by u_{σ i}^{c-1}: in the charts (φ, Φ) the Jacobian determinant is that power of the scaling coordinate, and in any other charts a unit times it.