The local ring of the chart at its origin is regular of dimension n

Kollár's yᵢ "give local coordinates on a chart of B_Z X" [Kol07, Definition 60]; in the local model this is the statement that A' := R'_{𝔪'}, the local ring of the chart ring R' = R[xᵢ/x_r : i < r] at the origin 𝔪' = ⟨y₀, …, y_{n-1}⟩ of the chart, is a regular local ring of dimension n whose maximal ideal is generated by the n images of the yᵢ (a regular system of parameters).

The argument closes a chain of primes against a bound on the generators by Krull's height theorem, as for the quotients by a regular system of parameters in Hironaka/Algebra/Local/RegularSystem.lean, and needs no intermediate description of A'/x_r A':

• R' is Noetherian, as a quotient of R[Y₀, …, Y_{r-1}] (the presentation of Hironaka/Algebra/Local/Chart.lean is surjective), so A' is a Noetherian local ring; its maximal ideal 𝔪' A' is generated by the n images of the yᵢ, hence spanFinrank ≤ n;
• dim A' = ht 𝔪' ≥ n by a chain of n + 1 primes of R' ending at 𝔪': with x' the regular system of parameters obtained from x by moving x_r to the last place, the ideals Qⱼ = ⟨x'₀, …, x'_{j-1}⟩, j ≤ n − 1, are primes of R not containing x_r (Hironaka/Algebra/Local/RegularSystem.lean), so they extend to primes of R[1/x_r] and contract to primes 𝔮ⱼ of R' ⊆ R[1/x_r], strictly increasing because x'ⱼ ∈ Q_{j+1} ∖ Qⱼ, and 𝔮_{n-1} ⊊ 𝔪': every element of 𝔮_{n-1} is killed by the map ψ : R[1/x_r] → Frac(R/Q_{n-1}) used for 1 ∉ 𝔪' in Hironaka/Algebra/Local/Chart.lean, which characterizes 𝔪' inside R' as the preimage of the maximal ideal of R/Q_{n-1} (R' = R + 𝔪' and 𝔪' ∩ R = 𝔪), while x_r ∈ 𝔪' ∖ 𝔮_{n-1}.
• spanFinrank 𝔪'A' ≤ n ≤ dim A' and Krull's height theorem give regularity (IsRegularLocalRing.of_spanFinrank_maximalIdeal_le) and dim A' = n.

theorem IsLocalRing.isNoetherianRing_chartRing {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) : IsNoetherianRing ↥(chartRing x r)

R' is Noetherian: a quotient of the Noetherian ring R[Y₀, …, Y_{r-1}].

theorem IsLocalRing.maximalIdeal_localization_chartOrigin {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) [(chartOrigin x r).IsPrime] : maximalIdeal (Localization.AtPrime (chartOrigin x r)) = Ideal.span (Set.range fun (i : Fin n) => (algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOrigin x r))) (chartYR x r i))

The maximal ideal of R'_{𝔪'} is generated by the images of the yᵢ.

theorem IsLocalRing.spanFinrank_maximalIdeal_localization_chartOrigin_le {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) [(chartOrigin x r).IsPrime] : Submodule.spanFinrank (maximalIdeal (Localization.AtPrime (chartOrigin x r))) ≤ n

The chain of primes below the origin

@[reducible, inline]

abbrev IsLocalRing.lastIdx {n : ℕ} (r : Fin n) : Fin n

The last index n - 1 (Fin n is nonempty since r : Fin n).

Equations

• IsLocalRing.lastIdx r = ⟨n - 1, ⋯⟩

@[reducible, inline]

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

The regular system of parameters with x_r moved to the last position.

Equations

• IsLocalRing.swapLast x r = x ∘ ⇑(Equiv.swap r (IsLocalRing.lastIdx r))

theorem IsLocalRing.swapLast_last {R : Type u_1} {n : ℕ} (x : Fin n → R) (r : Fin n) : swapLast x r (lastIdx r) = x r

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

@[reducible, inline]

noncomputable abbrev IsLocalRing.swapPrime {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (j : ℕ) : Ideal R

Qⱼ = ⟨x'₀, …, x'_{j-1}⟩, a prime of R not containing x_r for j ≤ n − 1.

Equations

• IsLocalRing.swapPrime x r j = Ideal.span (IsLocalRing.swapLast x r '' {i : Fin n | ↑i < j})

theorem IsLocalRing.swapPrime_isPrime {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) (j : ℕ) : (swapPrime x r j).IsPrime

theorem IsLocalRing.swapPrime_mono {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {j j' : ℕ} (h : j ≤ j') : swapPrime x r j ≤ swapPrime x r j'

theorem IsLocalRing.x_notMem_swapPrime {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) {j : ℕ} (hj : j ≤ n - 1) : x r ∉ swapPrime x r j

theorem IsLocalRing.swapLast_mem_swapPrime_succ {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (j : ℕ) (hj : j < n) : swapLast x r ⟨j, hj⟩ ∈ swapPrime x r (j + 1)

theorem IsLocalRing.swapLast_notMem_swapPrime {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) (j : ℕ) (hj : j < n) : swapLast x r ⟨j, hj⟩ ∉ swapPrime x r j

theorem IsLocalRing.disjoint_powers_swapPrime {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) {j : ℕ} (hj : j ≤ n - 1) : Disjoint ↑(Submonoid.powers (x r)) ↑(swapPrime x r j)

@[reducible, inline]

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

The prime 𝔮ⱼ of R': the contraction of Qⱼ R[1/x_r].

Equations

• IsLocalRing.chartPrime x r j = Ideal.comap (↑(IsLocalRing.chartRing x r).val) (Ideal.map (algebraMap R (Localization.Away (x r))) (IsLocalRing.swapPrime x r j))

theorem IsLocalRing.chartPrime_isPrime {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) {j : ℕ} (hj : j ≤ n - 1) : (chartPrime x r j).IsPrime

theorem IsLocalRing.chartPrime_mono {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) {j j' : ℕ} (h : j ≤ j') : chartPrime x r j ≤ chartPrime x r j'

theorem IsLocalRing.algebraMap_mem_chartPrime_iff {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) {j : ℕ} (hj : j ≤ n - 1) (a : R) : (algebraMap R ↥(chartRing x r)) a ∈ chartPrime x r j ↔ a ∈ swapPrime x r j

theorem IsLocalRing.chartPrime_lt_succ {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) {j : ℕ} (hj : j + 1 ≤ n - 1) : chartPrime x r j < chartPrime x r (j + 1)

𝔮_{n-1} ⊊ 𝔪', through the fraction field of R/Q_{n-1}

theorem IsLocalRing.chartPrime_le_chartOrigin {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) : chartPrime x r (n - 1) ≤ chartOrigin x r

theorem IsLocalRing.chartPrime_lt_chartOrigin {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) : chartPrime x r (n - 1) < chartOrigin x r

Regularity and dimension

noncomputable def IsLocalRing.chartChain {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (i : ℕ) : Ideal ↥(chartRing x r)

The chain 𝔮₀ ⊊ ⋯ ⊊ 𝔮_{n-1} ⊊ 𝔪' as a function on Fin (n + 1).

Equations

• IsLocalRing.chartChain x r i = if i < n then IsLocalRing.chartPrime x r i else IsLocalRing.chartOrigin x r

theorem IsLocalRing.chartChain_isPrime {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) (i : ℕ) : (chartChain x r i).IsPrime

theorem IsLocalRing.chartChain_lt_succ {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) {i : ℕ} (hi : i < n) : chartChain x r i < chartChain x r (i + 1)

theorem IsLocalRing.natCast_le_height_chartOrigin {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) : ↑n ≤ (chartOrigin x r).height

ht 𝔪' ≥ n.

theorem IsLocalRing.natCast_le_ringKrullDim_localization_chartOrigin {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) [(chartOrigin x r).IsPrime] : ↑n ≤ ringKrullDim (Localization.AtPrime (chartOrigin x r))

theorem IsLocalRing.isRegularLocalRing_localization_chartOrigin {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) [(chartOrigin x r).IsPrime] : IsRegularLocalRing (Localization.AtPrime (chartOrigin x r))

R'_{𝔪'} is a regular local ring: the yᵢ are local coordinates on the chart [Kol07, Definition 60].

theorem IsLocalRing.ringKrullDim_localization_chartOrigin {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) [(chartOrigin x r).IsPrime] : ringKrullDim (Localization.AtPrime (chartOrigin x r)) = ↑n

dim R'_{𝔪'} = n.