The chart ring of a blow-up along a coordinate subspace: definitions

Kollár computes with the blow-up of Z = (x₁ = ⋯ = x_r = 0) in the chart with coordinates y₁ = x₁/x_r, …, y_{r-1} = x_{r-1}/x_r, y_r = x_r, …, yₙ = xₙ [Kol07, Definition 60, (60.2)]. This file fixes the ring-level form of that chart: for a family x : Fin n → R (a regular system of parameters in use) and an index r, the elements yᵢ of R[1/x_r], the chart ring R' = R[x_i/x_r : i < r] ⊆ R[1/x_r], the origin 𝔪' = ⟨y₁, …, yₙ⟩R' of the chart, the presentation R[Y_i : i < r] → R' with its Koszul relations x_r Y_i − x_i, the other K-rational points 𝔪'_a of the exceptional fibre and the shifted coordinates x'_i = x_i − ã_i x_r, the extension of a derivation to R[1/a] and the transformed derivations ∂'_j.

Conventions

Indices are Fin n; Kollár's 1 ≤ r ≤ n (one-based) is r : Fin n (zero-based), the divided coordinates are the i < r, and x_r itself is the denominator. The denominator is a separate argument d of chartYOf, chartRingOf, chartOriginOf, so that the chart of a second family with the same r-th coordinate (the shifted coordinates: x'_r = x_r only propositionally) lives in the same ring R[1/x_r]; chartY x r, chartRing x r, chartOrigin x r are the specializations d = x r. Localization.Away d is Mathlib's Localization (Submonoid.powers d), and Localization.mk a ⟨d, _⟩ is a / d. The transformed derivations are ℚ-derivations of R[1/x_r]; that they preserve R' is proved in Hironaka/Algebra/Local/Chart.lean (chartDeriv_mem), so here they are defined on R[1/x_r] only.

Main declarations

• IsLocalRing.chartY, chartRing, chartYR, chartY_mem: the chart coordinates and the chart ring.
• IsLocalRing.chartOrigin and maximalIdeal_le_comap_chartOrigin (the map R → R' sends 𝔪 into 𝔪', so that the residue map R/𝔪 → R'/𝔪' is defined).
• IsLocalRing.chartPresentation, chartRelations: the polynomial presentation of R'.
• IsLocalRing.shiftCoords, chartOriginAt: the other rational points of the exceptional fibre and the coordinates centred at them.
• Derivation.extendAway: the extension of a derivation to A[1/a] (the specialization of Derivation.localization to Submonoid.powers a).
• IsLocalRing.RegularCoords.awayPderiv, chartDeriv: the transformed derivations ∂'_j = x_r ∂_j for j < r, ∂'_r = ∂_r + ∑_{i<r} yᵢ ∂ᵢ, ∂'_j = ∂_j for j > r.

The properties of these constructions (beginning with ∂'ⱼ yₖ = δⱼₖ and the stability of R' under the ∂'ⱼ) are proved in Hironaka/Algebra/Local/Chart.lean.

noncomputable def IsLocalRing.chartYOf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) (i : Fin n) : Localization.Away d

The chart coordinates of [Kol07, Definition 60, (60.2)] with a general denominator d: yᵢ = xᵢ / d for i < r and yᵢ = xᵢ for i ≥ r, in R[1/d].

Equations

• IsLocalRing.chartYOf x r d i = if i < r then Localization.mk (x i) ⟨d, ⋯⟩ else (algebraMap R (Localization.Away d)) (x i)

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartY {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r a✝ : Fin n) : Localization.Away (x r)

The chart coordinates yᵢ = xᵢ/x_r for i < r, y_r = x_r, yⱼ = xⱼ for j > r, in R[1/x_r] [Kol07, Definition 60, (60.2)].

Equations

• IsLocalRing.chartY x r = IsLocalRing.chartYOf x r (x r)

theorem IsLocalRing.chartYOf_of_lt {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) {i : Fin n} (h : i < r) : chartYOf x r d i = Localization.mk (x i) ⟨d, ⋯⟩

theorem IsLocalRing.chartYOf_of_not_lt {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) {i : Fin n} (h : ¬i < r) : chartYOf x r d i = (algebraMap R (Localization.Away d)) (x i)

theorem IsLocalRing.chartYOf_self {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) : chartYOf x r d r = (algebraMap R (Localization.Away d)) (x r)

noncomputable def IsLocalRing.chartRingOf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) : Subalgebra R (Localization.Away d)

With a general denominator d: the subalgebra R[xᵢ/d : i < r] of R[1/d].

Equations

• IsLocalRing.chartRingOf x r d = Algebra.adjoin R ((fun (i : Fin n) => Localization.mk (x i) ⟨d, ⋯⟩) '' {i : Fin n | i < r})

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartRing {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : Subalgebra R (Localization.Away (x r))

The chart ring R' = R[xᵢ/x_r : i < r] ⊆ R[1/x_r] of the chart (60.2) of [Kol07, Definition 60] and [Kol07, 75 (Birational transform of derivatives)], as Algebra.adjoin R {x_i / x_r : i < r}.

Equations

• IsLocalRing.chartRing x r = IsLocalRing.chartRingOf x r (x r)

theorem IsLocalRing.chartYOf_mem {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) (i : Fin n) : chartYOf x r d i ∈ chartRingOf x r d

theorem IsLocalRing.chartY_mem {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r i : Fin n) : chartY x r i ∈ chartRing x r

Every yᵢ lies in the chart ring.

noncomputable def IsLocalRing.chartYROf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) (i : Fin n) : ↥(chartRingOf x r d)

With a general denominator: yᵢ as an element of the chart ring.

Equations

• IsLocalRing.chartYROf x r d i = ⟨IsLocalRing.chartYOf x r d i, ⋯⟩

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartYR {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r a✝ : Fin n) : ↥(chartRing x r)

yᵢ as an element of the chart ring R'.

Equations

• IsLocalRing.chartYR x r = IsLocalRing.chartYROf x r (x r)

@[simp]

theorem IsLocalRing.coe_chartYROf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) (i : Fin n) : ↑(chartYROf x r d i) = chartYOf x r d i

noncomputable def IsLocalRing.chartOriginOf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) : Ideal ↥(chartRingOf x r d)

With a general denominator: the ideal ⟨y₁, …, yₙ⟩ of the chart ring.

Equations

• IsLocalRing.chartOriginOf x r d = Ideal.span (Set.range (IsLocalRing.chartYROf x r d))

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartOrigin {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : Ideal ↥(chartRing x r)

The origin 𝔪' = ⟨y₁, …, y_{r-1}, x_r, x_{r+1}, …, xₙ⟩ R' of the chart: the point "p' ∈ B_Z X, the origin of the chart we consider" of the proof of [Kol07, Lemma 61].

Equations

• IsLocalRing.chartOrigin x r = IsLocalRing.chartOriginOf x r (x r)

theorem IsLocalRing.chartYROf_mem_chartOriginOf {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (d : R) (i : Fin n) : chartYROf x r d i ∈ chartOriginOf x r d

theorem IsLocalRing.algebraMap_x_mem_chartOrigin {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r i : Fin n) : (algebraMap R ↥(chartRing x r)) (x i) ∈ chartOrigin x r

Every coordinate xᵢ of R maps into the origin of the chart: xᵢ = yᵢ for i ≥ r and xᵢ = yᵢ · x_r for i < r.

theorem IsLocalRing.maximalIdeal_le_comap_chartOrigin {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) [IsLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) : maximalIdeal R ≤ Ideal.comap (algebraMap R ↥(chartRing x r)) (chartOrigin x r)

The algebra map R → R' sends 𝔪 into 𝔪', so the residue map R/𝔪 → R'/𝔪' (Ideal.quotientMap) is defined.

noncomputable def IsLocalRing.chartPresentation {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : MvPolynomial (Fin ↑r) R →ₐ[R] ↥(chartRing x r)

The presentation R[Y_i : i < r] → R', Y_i ↦ yᵢ = xᵢ/x_r, of the chart ring.

Equations

• IsLocalRing.chartPresentation x r = MvPolynomial.aeval fun (i : Fin ↑r) => IsLocalRing.chartYR x r (Fin.castLE ⋯ i)

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartRelations {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : Ideal (MvPolynomial (Fin ↑r) R)

The Koszul relations x_r Y_i − xᵢ (i < r) of the presentation: the relation ideal presentationIdeal of the affine blow-up algebra at a = x_r, gᵢ = xᵢ.

Equations

• IsLocalRing.chartRelations x r = AlgebraicGeometry.affineBlowUpAlgebra.presentationIdeal (x r) fun (i : Fin ↑r) => x (Fin.castLE ⋯ i)

noncomputable def IsLocalRing.shiftCoords {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : Fin n → R

The coordinates after the linear change of the (x₁, …, x_r)-coordinates moving the origin of the chart to the point a (the proof of [Kol07, Lemma 61]): x'ᵢ = xᵢ − ãᵢ x_r for i < r, x'ⱼ = xⱼ for j ≥ r (ã the given lifts).

Equations

• IsLocalRing.shiftCoords x r a i = if i < r then x i - a i * x r else x i

theorem IsLocalRing.shiftCoords_self {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : shiftCoords x r a r = x r

noncomputable def IsLocalRing.chartOriginAt {R : Type u} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) : Ideal ↥(chartRing x r)

The other K-rational points of the exceptional fibre, 𝔪'_a = ⟨yᵢ − ãᵢ (i < r), x_r, x_{r+1}, …, xₙ⟩ R', the points the linear change of coordinates in the proof of [Kol07, Lemma 61] moves to the origin.

Equations

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

noncomputable def Derivation.extendAway {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (D : Derivation k A A) (a : A) : Derivation k (Localization.Away a) (Localization.Away a)

The extension of a derivation D of A to A[1/a], D(f / aᵏ) = (a · D f − k · f · D a) / aᵏ⁺¹ (the extension of the ∂/∂uᵢ to the fraction field in the proof of [Wlo05, Lemma 2.6.3]); the specialization of Derivation.localization to Submonoid.powers a.

Equations

• D.extendAway a = Derivation.localization (Submonoid.powers a) D

noncomputable def IsLocalRing.RegularCoords.awayPderiv {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r j : Fin n) : Derivation ℚ (Localization.Away (c.x r)) (Localization.Away (c.x r))

The coordinate derivation ∂ⱼ extended to R[1/x_r].

Equations

• c.awayPderiv r j = (c.pderiv j).extendAway (c.x r)

noncomputable def IsLocalRing.RegularCoords.chartDeriv {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r j : Fin n) : Derivation ℚ (Localization.Away (c.x r)) (Localization.Away (c.x r))

The transformed derivations on R[1/x_r], ∂'ⱼ = x_r ∂ⱼ for j < r, ∂'_r = ∂_r + ∑_{i<r} yᵢ ∂ᵢ, ∂'ⱼ = ∂ⱼ for j > r: the derivations of the chart expressed through those of the base, as in [Kol07, 75], the proof of [Wlo05, Lemma 2.6.3] and [BM08, Lemma 3.1].

Equations

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

theorem IsLocalRing.RegularCoords.chartDeriv_of_lt {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (h : j < r) : c.chartDeriv r j = (algebraMap R (Localization.Away (c.x r))) (c.x r) • c.awayPderiv r j

theorem IsLocalRing.RegularCoords.chartDeriv_self {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) : c.chartDeriv r r = c.awayPderiv r r + ∑ i : Fin n with i < r, chartY c.x r i • c.awayPderiv r i

theorem IsLocalRing.RegularCoords.chartDeriv_of_gt {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : Fin n) {j : Fin n} (h : r < j) : c.chartDeriv r j = c.awayPderiv r j