Coordinates on the localization at a coordinate prime

Kollár defines the order along a subvariety Z at its generic point, ord_Z I := ord_η I [Kol07, Definition 47]; with local coordinates Z = (x₁ = ⋯ = x_r = 0) [Kol07, Definition 60] the local ring at η is R_{P_r}, P_r = ⟨x₁, …, x_r⟩. Serre's theorem that every localization of a regular local ring is regular is not in Mathlib (an open pull request); for a prime generated by part of a regular system of parameters there is a direct argument, which this file follows:

• P₀ ⊊ P₁ ⊊ ⋯ ⊊ P_r is a chain of primes (each Pᵢ is prime by Hironaka/Algebra/Local/RegularSystem.lean, and xᵢ ∈ P_{i+1} ∖ Pᵢ), so dim R_{P_r} = ht P_r ≥ r (Order.length_le_height);
• P_r R_{P_r} is generated by the r elements x₀, …, x_{r-1}, so spanFinrank ≤ r;
• Krull's height theorem closes the circle: R_{P_r} is regular (of_spanFinrank_maximalIdeal_le) of dimension exactly r.

The coordinate derivations extend to R_{P_r} by the quotient rule (Derivation.localization), agree with the ∂ᵢ on the image of R, hence satisfy ∂̃ᵢ x̃ⱼ = δᵢⱼ; they commute because the commutator of two derivations is a derivation, and a derivation of the localization vanishing on the image of R is zero (eq_localization_of_algebraMap with D = 0). So R_{P_r} carries a RegularCoords structure on r coordinates (localizationCoords).

Commuting derivations extend to commuting derivations

The localization at P_r

theorem IsLocalRing.image_lt_eq_range {R : Type u_1} {n : ℕ} (x : Fin n → R) {r : ℕ} (hr : r ≤ n) : x '' {j : Fin n | ↑j < r} = Set.range fun (i : Fin r) => x (Fin.castLE hr i)

The generators of P_r, indexed by Fin r.

theorem IsLocalRing.maximalIdeal_localization_span_image_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) {r : ℕ} (hr : r ≤ n) [(Ideal.span (x '' {j : Fin n | ↑j < r})).IsPrime] : maximalIdeal (Localization.AtPrime (Ideal.span (x '' {j : Fin n | ↑j < r}))) = Ideal.span (Set.range fun (i : Fin r) => (algebraMap R (Localization.AtPrime (Ideal.span (x '' {j : Fin n | ↑j < r})))) (x (Fin.castLE hr i)))

P_r R_{P_r} is generated by the images of x₀, …, x_{r-1}.

theorem IsLocalRing.spanFinrank_maximalIdeal_localization_le {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) {r : ℕ} (hr : r ≤ n) [(Ideal.span (x '' {j : Fin n | ↑j < r})).IsPrime] : Submodule.spanFinrank (maximalIdeal (Localization.AtPrime (Ideal.span (x '' {j : Fin n | ↑j < r})))) ≤ r

theorem IsLocalRing.natCast_le_height_span_image_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) {r : ℕ} [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hr : r ≤ n) : ↑r ≤ (Ideal.span (x '' {j : Fin n | ↑j < r})).height

The chain P₀ ⊊ ⋯ ⊊ P_r gives ht P_r ≥ r.

theorem IsLocalRing.natCast_le_ringKrullDim_localization_span_image_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) {r : ℕ} [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hr : r ≤ n) [(Ideal.span (x '' {j : Fin n | ↑j < r})).IsPrime] : ↑r ≤ ringKrullDim (Localization.AtPrime (Ideal.span (x '' {j : Fin n | ↑j < r})))

theorem IsLocalRing.isRegularLocalRing_localization_span_image_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) {r : ℕ} [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hr : r ≤ n) [(Ideal.span (x '' {j : Fin n | ↑j < r})).IsPrime] : IsRegularLocalRing (Localization.AtPrime (Ideal.span (x '' {j : Fin n | ↑j < r})))

R_{P_r} is a regular local ring (the local ring at the generic point of the coordinate subspace Z = (x₁ = ⋯ = x_r = 0), [Kol07, Definition 47]).

theorem IsLocalRing.ringKrullDim_localization_span_image_lt {R : Type u_1} [CommRing R] {n : ℕ} (x : Fin n → R) {r : ℕ} [IsRegularLocalRing R] (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hr : r ≤ n) [(Ideal.span (x '' {j : Fin n | ↑j < r})).IsPrime] : ringKrullDim (Localization.AtPrime (Ideal.span (x '' {j : Fin n | ↑j < r}))) = ↑r

dim R_{P_r} = r.

The coordinate structure on R_{P_r}

theorem IsLocalRing.localization_pderiv_algebraMap_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {r : ℕ} (hr : r ≤ n) [(Ideal.span (c.x '' {j : Fin n | ↑j < r})).IsPrime] (i j : Fin r) : (Derivation.localization (Ideal.span (c.x '' {j : Fin n | ↑j < r})).primeCompl (c.pderiv (Fin.castLE hr i))) ((algebraMap R (Localization.AtPrime (Ideal.span (c.x '' {j : Fin n | ↑j < r})))) (c.x (Fin.castLE hr j))) = if i = j then 1 else 0

The localized derivations satisfy ∂̃ᵢ x̃ⱼ = δᵢⱼ.

noncomputable def IsLocalRing.localizationCoords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {r : ℕ} (hr : r ≤ n) [(Ideal.span (c.x '' {j : Fin n | ↑j < r})).IsPrime] : RegularCoords (Localization.AtPrime (Ideal.span (c.x '' {j : Fin n | ↑j < r}))) r

The coordinate structure on R_{P_r}: parameters x̃₀, …, x̃_{r-1}, derivations ∂̃₀, …, ∂̃_{r-1} (the local ring at the generic point of Z = (x₁ = ⋯ = x_r = 0), [Kol07, Definitions 47 and 60]).

Equations

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

theorem IsLocalRing.exists_localization_coords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {r : ℕ} (hr : r ≤ n) [(Ideal.span (c.x '' {j : Fin n | ↑j < r})).IsPrime] : ∃ (x : IsRegularLocalRing (Localization.AtPrime (Ideal.span (c.x '' {j : Fin n | ↑j < r})))) (c' : RegularCoords (Localization.AtPrime (Ideal.span (c.x '' {j : Fin n | ↑j < r}))) r), (c'.x = fun (i : Fin r) => (algebraMap R (Localization.AtPrime (Ideal.span (c.x '' {j : Fin n | ↑j < r})))) (c.x (Fin.castLE hr i))) ∧ c'.pderiv = fun (i : Fin r) => Derivation.localization (Ideal.span (c.x '' {j : Fin n | ↑j < r})).primeCompl (c.pderiv (Fin.castLE hr i))

The coordinate structure on R_{P_r} in existential form: R_{P_r} is regular local and carries coordinates whose parameters are the images of x₀, …, x_{r-1}.