Kollár's chart formulas: the transformed derivations of the chart ring

Kollár computes, in the blow-up chart with coordinates y_j = x_j / x_r (j < r), y_r = x_r, y_j = x_j (j > r), the derivatives of f ∘ π by the chain rule: ∂_{y_j}(f ∘ π) = x_r (∂_{x_j} f) ∘ π for j < r, (∂_{x_j} f) ∘ π for j > r, and (∂_{x_r} f) ∘ π + ∑_{i<r} y_i (∂_{x_i} f) ∘ π for j = r: the unmarked content of [Kol07, 75, (75.1)–(75.3)]. The version for schemes packages exactly these three formulas as the transformed derivations ∂'_j of the chart ring R' = R[x_i/x_r : i < r] (chartDerivRing of Hironaka.Algebra.Local.ChartCoords). This file proves that the ring map χ : R' → 𝒪_{M', a'} of Hironaka.Manifold.BlowUp.Transform.KollarChart carries ∂'_j to the partial derivative ∂_{u_{τ j}} of the blow-up chart Φ (τ Kollár's order of the coordinates, τ r = σ i):

• chartRingHom_chartDerivRing_eq_coordDerivStalk: χ(∂'_j g) = ∂_{u_{τ j}}(χ g) for every g.

Both sides are derivations of R' along χ (additive, Leibniz along χ), so it suffices to compare them on the generators of R' over R: on algebraMap R R' the comparison is the chain rule for germs (derivation_germMap_eq_sum_coordDerivStalk) together with the pullbacks of the coordinates along the blow-up chart (x_k ∘ π = u_{σ i} u_k on the centre block, = u_k transversally), and on the y_i both sides are δ_{ij} (chartDerivRing_chartYR; χ(y_i) = u_{τ i}).

This is the rule by which the derivative of a birational transform is computed in Hironaka.Manifold.BlowUp.Transform.DerivTransform.

theorem Manifold.x_eq_coord_of_eq_σ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (haY : π a' ∈ Y) (x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) (τ : Fin n ≃ Fin n) (hτ : ∀ (j : Fin n), x j = coord E ψ φ ⋯ ⋯ (τ j) - (const 𝕜 E M (π a')) ((eval 𝕜 E M (π a')) (coord E ψ φ ⋯ ⋯ (τ j)))) {m : Fin n} {k : Fin c} (hmk : τ m = σ k) : x m = coord E ψ φ ⋯ ⋯ (σ k)

On the centre block the centred coordinates are the adapted coordinates (which vanish at the points of Y).

theorem Manifold.germMap_x_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (haY : π a' ∈ Y) (x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) (r : Fin n) (τ : Fin n ≃ Fin n) (hτr : τ r = σ i) (hτ : ∀ (j : Fin n), x j = coord E ψ φ ⋯ ⋯ (τ j) - (const 𝕜 E M (π a')) ((eval 𝕜 E M (π a')) (coord E ψ φ ⋯ ⋯ (τ j)))) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) {m : Fin n} (hm : m < r) : (germMap π ⋯ a') (x m) = coord E ψ Φ ⋯ ha' (τ r) * coord E ψ Φ ⋯ ha' (τ m)

[Kol07, Definition 60, (60.2)] for the centre block: x_m ∘ π = u_{τ r} u_{τ m} for m < r.

theorem Manifold.germMap_x_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (haY : π a' ∈ Y) (x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) (r : Fin n) (τ : Fin n ≃ Fin n) (hτr : τ r = σ i) (hτ : ∀ (j : Fin n), x j = coord E ψ φ ⋯ ⋯ (τ j) - (const 𝕜 E M (π a')) ((eval 𝕜 E M (π a')) (coord E ψ φ ⋯ ⋯ (τ j)))) : (germMap π ⋯ a') (x r) = coord E ψ Φ ⋯ ha' (τ r)

[Kol07, Definition 60, (60.2)] for the divisor coordinate: x_r ∘ π = u_{τ r}.

theorem Manifold.germMap_x_of_gt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) (r : Fin n) (τ : Fin n ≃ Fin n) (hτr : τ r = σ i) (hτ : ∀ (j : Fin n), x j = coord E ψ φ ⋯ ⋯ (τ j) - (const 𝕜 E M (π a')) ((eval 𝕜 E M (π a')) (coord E ψ φ ⋯ ⋯ (τ j)))) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) {m : Fin n} (hm : r < m) : (germMap π ⋯ a') (x m) = coord E ψ Φ ⋯ ha' (τ m) - (const 𝕜 E M' a') ((eval 𝕜 E M (π a')) (coord E ψ φ ⋯ ⋯ (τ m)))

[Kol07, Definition 60, (60.2)] for the transversal coordinates: x_m ∘ π = u_{τ m} − u_{τ m}(a') for m > r.

theorem Manifold.chartRingHom_chartDerivRing_eq_coordDerivStalk {𝕜 : 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] [FiniteDimensional 𝕜 E] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (haY : π a' ∈ Y) (κ : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) n) (r : Fin n) (τ : Fin n ≃ Fin n) (hτr : τ r = σ i) (hτ : ∀ (j : Fin n), κ.x j = coord E ψ φ ⋯ ⋯ (τ j) - (const 𝕜 E M (π a')) ((eval 𝕜 E M (π a')) (coord E ψ φ ⋯ ⋯ (τ j)))) (hpd : ∀ (j : Fin n), κ.pderiv j = Derivation.restrictScalars ℚ (coordDerivStalk E ψ φ ⋯ ⋯ (τ j))) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) (χ : ↥(IsLocalRing.chartRing κ.x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')) (hχ : ∀ (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))), χ ((algebraMap ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) ↥(IsLocalRing.chartRing κ.x r)) s) = (germMap π ⋯ a') s) (hχy : ∀ j < r, χ (IsLocalRing.chartYR κ.x r j) = coord E ψ Φ ⋯ ha' (τ j)) (j : Fin n) (g : ↥(IsLocalRing.chartRing κ.x r)) : χ ((κ.chartDerivRing r j) g) = (coordDerivStalk E ψ Φ ⋯ ha' (τ j)) (χ g)

The transformed derivations ∂'_j of the chart ring (chartDerivRing) are carried by the chart-ring map χ to the partial derivatives ∂_{u_{τ j}} of the blow-up chart: χ(∂'_j g) = ∂_{u_{τ j}}(χ g) [Kol07, 75, (75.1)–(75.3)].