The Jacobian determinant of the blow-up chart map

The chart map π_i (blowUpChartMap σ i: x_{σ i} = u_{σ i}, x_{σ k} = u_{σ i} u_{σ k} for k ≠ i, the other coordinates unchanged) has derivative t ↦ u_{σ i} t_{σ k} + u_{σ k} t_{σ i} on the ratio slots and t ↦ t_j elsewhere. Its matrix differs from the diagonal matrix with entries u_{σ i} (ratio slots) and 1 (the other slots) only in the column σ i, by a vector vanishing at the row σ i; by multilinearity of the determinant in that column the Jacobian determinant is the diagonal product u_{σ i}^{c-1}. For c ≥ 2 the derivative is therefore invertible exactly off the exceptional hyperplane {u_{σ i} = 0} of the chart.

The chart maps are those of the local model of [BM88, Definition 4.1]; the computation is not in the source. The determinant enters the Jacobian of the blow-down map of a manifold (Hironaka.Manifold.Jacobian.BlowUp).

noncomputable def Manifold.blowUpChartMapDeriv {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : (Fin n → 𝕜) →L[𝕜] Fin n → 𝕜

The derivative of the chart map π_i at u: t ↦ u_{σ i} t_j + u_j t_{σ i} on the ratio slots j = σ k, k ≠ i, and t ↦ t_j on the other slots.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.hasFDerivAt_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : HasFDerivAt (blowUpChartMap σ i) (blowUpChartMapDeriv σ i u) u

The Fréchet derivative of the chart map π_i at u is blowUpChartMapDeriv σ i u.

theorem Manifold.fderiv_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : fderiv 𝕜 (blowUpChartMap σ i) u = blowUpChartMapDeriv σ i u

The Fréchet derivative of π_i, as an equation.

noncomputable def Manifold.jacobianDiag {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : Fin n → 𝕜

The diagonal of the Jacobian: u_{σ i} on the ratio slots, 1 elsewhere.

Equations

• Manifold.jacobianDiag σ i u j = if ∃ (k : Fin c), k ≠ i ∧ σ k = j then u (σ i) else 1

noncomputable def Manifold.jacobianCol {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : Fin n → 𝕜

The off-diagonal column σ i of the Jacobian: u_j on the ratio slots, 0 elsewhere.

Equations

• Manifold.jacobianCol σ i u j = if ∃ (k : Fin c), k ≠ i ∧ σ k = j then u j else 0

theorem Manifold.not_exists_ne_and_apply_eq_self {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : ¬∃ (k : Fin c), k ≠ i ∧ σ k = σ i

The block indices are injective: no k ≠ i has σ k = σ i.

theorem Manifold.toMatrix'_blowUpChartMapDeriv {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : LinearMap.toMatrix' ↑(blowUpChartMapDeriv σ i u) = (Matrix.diagonal (jacobianDiag σ i u)).updateCol (σ i) ((fun (j : Fin n) => Matrix.diagonal (jacobianDiag σ i u) j (σ i)) + jacobianCol σ i u)

The matrix of the derivative: the diagonal matrix with the column σ i perturbed.

theorem Manifold.prod_jacobianDiag {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (u : Fin n → 𝕜) : ∏ j : Fin n, jacobianDiag σ i u j = u (σ i) ^ (c - 1)

The diagonal product: u_{σ i}^{c - 1}.

theorem Manifold.det_fderiv_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (u : Fin n → 𝕜) : (fderiv 𝕜 (blowUpChartMap σ i) u).det = u (σ i) ^ (c - 1)

The Jacobian determinant of the chart map π_i is u_{σ i}^{c-1}.