The kernel of the chart presentation

Kollár asserts that y₁ = x₁/x_r, …, y_{r-1} = x_{r-1}/x_r, y_r = x_r, … "give local coordinates on a chart" [Kol07, Definition 60]; Hauser states that for a regular sequence g₁, …, g_k the only relations among the gⱼ/gᵢ over R are the trivial ones, so that R[g₁/gᵢ, …, g_k/gᵢ] ≅ R[t₁, …, t_k]/(gᵢ tⱼ − gⱼ) [Hau14, Theorem 4.20 (b)]. Hironaka/Algebra/Local/Chart.lean gives the presentation R[Y₀, …, Y_{r-1}] → R' = R[xᵢ/x_r], Yᵢ ↦ yᵢ, and its surjectivity; this file proves that its kernel is exactly the ideal ⟨x_r Yᵢ − xᵢ⟩ of the obvious relations:

• the list [x_r, x₀, …, x_{r-1}] is weakly regular on R — it is a prefix of a permutation of the regular system of parameters, which is a regular sequence (Hironaka/Algebra/Local/RegularSystem.lean);
• the assembly: ⟨x_r Yᵢ − xᵢ⟩ ⊆ ker because x_r yᵢ = xᵢ in R'; for p in the kernel, the elimination lemma of Hironaka/Scheme/BlowUp/LinearType.lean gives x_rᵈ p ≡ c (mod ⟨x_r Yᵢ − xᵢ⟩) with c ∈ R, so c = 0 in R[1/x_r], hence x_rᵏ c = 0 in R and c = 0 (x_r is a nonzerodivisor); then x_rᵈ p ∈ ⟨x_r Yᵢ − xᵢ⟩ and the torsion-freeness of the ideal of relations modulo x_r (Hironaka/Scheme/BlowUp/LinearType.lean, for a weakly regular sequence) gives p ∈ ⟨x_r Yᵢ − xᵢ⟩.

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartList {R : Type u_1} {n : ℕ} (x : Fin n → R) (r : Fin n) : List R

The list [x_r, x₀, …, x_{r-1}]: the denominator first, then the divided coordinates.

Equations

• IsLocalRing.chartList x r = x r :: List.ofFn fun (i : Fin ↑r) => x (Fin.castLE ⋯ i)

@[reducible, inline]

noncomputable abbrev IsLocalRing.chartTail {R : Type u_1} {n : ℕ} (x : Fin n → R) (r : Fin n) : List R

The remaining parameters x_{r+1}, …, x_{n-1}.

Equations

• IsLocalRing.chartTail x r = List.ofFn fun (i : Fin (n - ↑r - 1)) => x ⟨↑r + 1 + ↑i, ⋯⟩

theorem IsLocalRing.ofList_chartList_append_chartTail {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : Ideal.ofList (chartList x r ++ chartTail x r) = Ideal.span (Set.range x)

theorem IsLocalRing.length_chartList_append_chartTail {R : Type u_1} {n : ℕ} (x : Fin n → R) (r : Fin n) : (chartList x r ++ chartTail x r).length = n

theorem IsLocalRing.isWeaklyRegular_chartList {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) : RingTheory.Sequence.IsWeaklyRegular R (chartList x r)

[x_r, x₀, …, x_{r-1}] is weakly regular on R (a prefix of a permutation of a regular system of parameters; regular sequences as in [TSPA, Tag 00LJ]).

theorem IsLocalRing.isSMulRegular_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) : IsSMulRegular R (x r)

x_r is a nonzerodivisor of R (the head of the weakly regular list).

The kernel of the presentation

theorem IsLocalRing.chartPresentation_sub_eq_zero {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (i : Fin ↑r) : (chartPresentation x r) (MvPolynomial.C (x r) * MvPolynomial.X i - MvPolynomial.C (x (Fin.castLE ⋯ i))) = 0

theorem IsLocalRing.chartRelations_le_ker_chartPresentation {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : chartRelations x r ≤ RingHom.ker (chartPresentation x r)

⟨x_r Yᵢ − xᵢ⟩ ⊆ ker.

theorem IsLocalRing.mem_presentationIdeal_of_C_pow_mul_mem {A : Type u_2} [CommRing A] {k : ℕ} (a : A) (g : Fin k → A) (h : RingTheory.Sequence.IsWeaklyRegular A (a :: List.ofFn g)) (d : ℕ) (p : MvPolynomial (Fin k) A) (hp : MvPolynomial.C a ^ d * p ∈ AlgebraicGeometry.affineBlowUpAlgebra.presentationIdeal a g) : p ∈ AlgebraicGeometry.affineBlowUpAlgebra.presentationIdeal a g

theorem IsLocalRing.ker_chartPresentation {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) : RingHom.ker (chartPresentation x r) = chartRelations x r

The kernel of the chart presentation is the ideal of the relations x_r Yᵢ − xᵢ ([Hau14, Theorem 4.20 (b)]; the coordinates of the chart of [Kol07, Definition 60]).