Coordinates on the local ring of the chart at its origin

On the chart x_r ≠ 0 of the blow-up of ⟨x₀, …, x_r⟩ the functions yᵢ = xᵢ/x_r (i < r), y_r = x_r, yⱼ = xⱼ (j > r) are local coordinates [Kol07, Definition 60], and the transformed derivations ∂'ⱼ of Hironaka/Algebra/Local/ChartRing.lean (∂'ⱼ = x_r ∂ⱼ for j < r, ∂'_r = ∂_r + ∑_{i<r} yᵢ ∂ᵢ, ∂'ⱼ = ∂ⱼ for j > r) satisfy ∂'ⱼ yₖ = δⱼₖ (Hironaka/Algebra/Local/Chart.lean). This module packages A' = R'_{𝔪'} with the images of the yᵢ and the localized ∂'ⱼ as a RegularCoords A' n, the coordinate structure of the chart at its origin:

• the ring-theoretic fields (regularity, 𝔪' A' = ⟨yᵢ⟩, dim A' = n) are proved in Hironaka/Algebra/Local/ChartLocal.lean;
• ∂'ⱼ yₖ = δⱼₖ transfers along the localization map (Derivation.localization_algebraMap);
• the ∂'ⱼ commute. The ∂ⱼ extended to R[1/x_r] commute (the extension of a commutator is the commutator of the extensions, Derivation.localization_comm), and for two commuting derivations D₁, D₂ and ring elements f, g one has the derivation identity [f D₁, g D₂] = f (D₁ g) D₂ − g (D₂ f) D₁; the five cases i < j < r, i < j = r, i < r < j, i = r < j, r < i < j are then read off the table ∂ⱼ x_r = δⱼᵣ, ∂ⱼ yₖ = δⱼₖ u − δⱼᵣ xₖ u² (k < r, u = 1/x_r) of Hironaka/Algebra/Local/Chart.lean — e.g. for i < j = r, [x_r ∂ᵢ, ∂_r] = −∂ᵢ and ∑_{k<r} [x_r ∂ᵢ, yₖ ∂ₖ] = ∑_{k<r} δᵢₖ x_r u ∂ₖ = ∂ᵢ. The commutation then descends to R' (chartDerivRing) and extends to A'.

Commutators of scaled derivations

theorem Derivation.commutator_smul_smul {k : Type u_1} {B : Type u_2} [CommRing k] [CommRing B] [Algebra k B] (D₁ D₂ : Derivation k B B) (h : ⁅D₁, D₂⁆ = 0) (f g : B) : ⁅f • D₁, g • D₂⁆ = (f * D₁ g) • D₂ - (g * D₂ f) • D₁

[f D₁, g D₂] = f (D₁ g) D₂ − g (D₂ f) D₁ for commuting derivations D₁, D₂.

theorem IsLocalRing.RegularCoords.awayPderiv_commutator {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r i j : Fin n) : ⁅c.awayPderiv r i, c.awayPderiv r j⁆ = 0

The extended coordinate derivations ∂ᵢ, ∂ⱼ of R[1/x_r] commute.

theorem IsLocalRing.RegularCoords.chartDeriv_commutator_of_lt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {i j : Fin n} (hij : i < j) : ⁅c.chartDeriv r i, c.chartDeriv r j⁆ = 0

The transformed derivations ∂'ᵢ, ∂'ⱼ commute, i < j (the five cases of the module docstring).

theorem IsLocalRing.RegularCoords.chartDeriv_commutator {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r i j : Fin n) : ⁅c.chartDeriv r i, c.chartDeriv r j⁆ = 0

The transformed derivations commute.

theorem IsLocalRing.RegularCoords.chartDeriv_comm {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r i j : Fin n) (z : Localization.Away (c.x r)) : (c.chartDeriv r i) ((c.chartDeriv r j) z) = (c.chartDeriv r j) ((c.chartDeriv r i) z)

theorem IsLocalRing.RegularCoords.chartDerivRing_comm {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r i j : Fin n) (z : ↥(chartRing c.x r)) : (c.chartDerivRing r i) ((c.chartDerivRing r j) z) = (c.chartDerivRing r j) ((c.chartDerivRing r i) z)

theorem IsLocalRing.RegularCoords.chartDerivRing_chartYR {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r i j : Fin n) : (c.chartDerivRing r i) (chartYR c.x r j) = if i = j then 1 else 0

∂'ᵢ yⱼ = δᵢⱼ in the chart ring R'.

The coordinate structure on R'_{𝔪'}

instance IsLocalRing.RegularCoords.chartOrigin_isPrime {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) : (chartOrigin c.x r).IsPrime

theorem IsLocalRing.RegularCoords.localization_chartDerivRing_algebraMap_chartYR {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r i j : Fin n) : (Derivation.localization (chartOrigin c.x r).primeCompl (c.chartDerivRing r i)) ((algebraMap (↥(chartRing c.x r)) (Localization.AtPrime (chartOrigin c.x r))) (chartYR c.x r j)) = if i = j then 1 else 0

∂'ᵢ yⱼ = δᵢⱼ in R'_{𝔪'}.

noncomputable def IsLocalRing.RegularCoords.chartCoords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) : RegularCoords (Localization.AtPrime (chartOrigin c.x r)) n

The coordinate structure on A' = R'_{𝔪'}: parameters the images of y₀, …, y_{n-1}, derivations the localized ∂'ⱼ — Kollár's local coordinates on the chart [Kol07, Definition 60].

Equations

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

theorem IsLocalRing.RegularCoords.exists_chartCoords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) : ∃ (h : IsRegularLocalRing (Localization.AtPrime (chartOrigin c.x r))) (c' : RegularCoords (Localization.AtPrime (chartOrigin c.x r)) n), (c'.x = fun (i : Fin n) => (algebraMap (↥(chartRing c.x r)) (Localization.AtPrime (chartOrigin c.x r))) (chartYR c.x r i)) ∧ ∀ (j : Fin n) (f : ↥(chartRing c.x r)), ∃ (g : ↥(chartRing c.x r)), ↑g = (c.chartDeriv r j) ↑f ∧ (c'.pderiv j) ((algebraMap (↥(chartRing c.x r)) (Localization.AtPrime (chartOrigin c.x r))) f) = (algebraMap (↥(chartRing c.x r)) (Localization.AtPrime (chartOrigin c.x r))) g

The coordinate structure of the chart in existential form: R'_{𝔪'} is regular local and carries coordinates whose parameters are the images of the yᵢ and whose derivations extend the transformed derivations ∂'ⱼ of R'.