Regular local rings with coordinates

This file fixes the setting of the local algebra shared by the algebraic and the analytic parts of the library: a regular local ring R containing ℚ, a regular system of parameters x₁, …, xₙ and derivations ∂₁, …, ∂ₙ with ∂ᵢ xⱼ = δᵢⱼ. It is the ring-level form of Kollár's "local coordinates at a point of a smooth variety" [Kol07, Definition 55] together with the partial derivatives ∂/∂xᵢ that generate the derivations there [Kol07, Definition 73]; the same structure is carried by the rings of real- and complex-analytic germs.

Main declarations

• IsLocalRing.RegularCoords R n: the coordinate structure. The four propositional fields say that the xᵢ generate the maximal ideal, that n is the Krull dimension (so x is a regular system of parameters), that ∂ᵢ xⱼ = δᵢⱼ, and that the ∂ᵢ commute.
• IsLocalRing.isUnit_natCast, charZero_residueField: how "characteristic zero" enters — nonzero natural numbers are units of R and of its residue field.
• IsLocalRing.RegularCoords.jacobian, transportPderiv, isUnit_jacobian, changeCoords: a second generating system x' of the maximal ideal has an invertible Jacobian matrix Mᵢⱼ = ∂ᵢ x'ⱼ, and the transported derivations ∂'ⱼ = ∑ₗ (M⁻¹)ⱼₗ ∂ₗ satisfy ∂'ⱼ x'ᵢ = δᵢⱼ.
• IsLocalRing.RegularCoords.span_range_transportPderiv: the R-span of the derivations does not depend on the coordinates.
• IsLocalRing.RegularCoords.SpansDerivations: the condition every instance of the structure supplies, that the ∂ᵢ generate all derivations.

The change-of-coordinates argument

Kollár chooses local coordinates adapted to a subvariety without comment, for instance when computing a blow-up in coordinates [Kol07, Definition 60] or in the proof of [Kol07, Proposition 99]; the underlying algebra is the following. Let x' be another generating system of the maximal ideal 𝔪 and M the matrix Mᵢⱼ = ∂ᵢ x'ⱼ. If det M were not a unit, its residue would vanish and the residue matrix would have a nonzero kernel vector v; lifting v to w : Fin n → R, the element y = ∑ⱼ wⱼ x'ⱼ lies in 𝔪 and all its partials ∂ᵢ y = ∑ⱼ wⱼ ∂ᵢ x'ⱼ + ∑ⱼ (∂ᵢ wⱼ) x'ⱼ lie in 𝔪. An element of 𝔪 all of whose partials lie in 𝔪 lies in 𝔪²: writing y = ∑ aₗ xₗ, the relation ∂ᵢ y ≡ aᵢ (mod 𝔪) forces every aₗ ∈ 𝔪. Some wⱼ₀ is a unit, so x'ⱼ₀ ∈ 𝔪² + ⟨x'ⱼ : j ≠ j₀⟩, and Nakayama's lemma gives 𝔪 = ⟨x'ⱼ : j ≠ j₀⟩, generated by n - 1 elements. But the minimal number of generators of the maximal ideal of a regular local ring is its dimension n, a contradiction. This is where regularity of R (through dim R = n) is used; nothing else in the file needs it.

Index convention

With the pair of conventions Mᵢⱼ = ∂ⱼ x'ᵢ and ∂'ⱼ = ∑ₗ (M⁻¹)ⱼₗ ∂ₗ one would get ∂'ⱼ x'ᵢ = (M · (M⁻¹)ᵀ)ᵢⱼ, which is δᵢⱼ only for symmetric M. We take the Jacobian convention Mᵢⱼ = ∂ᵢ x'ⱼ and keep ∂'ⱼ = ∑ₗ (M⁻¹)ⱼₗ ∂ₗ, so that ∂'ⱼ x'ᵢ = (M⁻¹ M)ⱼᵢ = δⱼᵢ.

Instances

RegularCoords is data, not a class: a ring carries many coordinate systems, and the change of coordinates above moves between them. The instances constructed in the library are the stalks of smooth k-schemes at their points, the power series ring K⟦X₁, …, Xₙ⟧ (Hironaka.Algebra.Local.PowerSeries) and the rings of analytic germs; each also supplies SpansDerivations for the derivations of its setting.

structure IsLocalRing.RegularCoords (R : Type u) [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (n : ℕ) : Type u

The coordinate structure [Kol07, Definitions 55 and 73]. A regular system of parameters x of the regular local ring R ⊇ ℚ together with commuting derivations pderiv i satisfying pderiv i (x j) = δᵢⱼ. The field card says n = dim R; with span_x it makes x a minimal generating system of the maximal ideal.

• x : Fin n → R

  The regular system of parameters x₁, …, xₙ.

• pderiv : Fin n → Derivation ℚ R R

  The partial derivatives ∂₁, …, ∂ₙ, as ℚ-derivations of R.

• span_x : maximalIdeal R = Ideal.span (Set.range self.x)

  The xᵢ generate the maximal ideal.

• card : ↑n = ringKrullDim R

  n is the Krull dimension of R.

• pderiv_x (i j : Fin n) : (self.pderiv i) (self.x j) = if i = j then 1 else 0

  ∂ᵢ xⱼ = δᵢⱼ.

• pderiv_comm (i j : Fin n) (f : R) : (self.pderiv i) ((self.pderiv j) f) = (self.pderiv j) ((self.pderiv i) f)

  The partial derivatives commute.

theorem IsLocalRing.isUnit_natCast (R : Type u) [CommRing R] [Algebra ℚ R] {a : ℕ} (ha : a ≠ 0) : IsUnit ↑a

A nonzero natural number is a unit of the ℚ-algebra R.

instance IsLocalRing.charZero_residueField (R : Type u) [CommRing R] [Algebra ℚ R] [IsLocalRing R] : CharZero (ResidueField R)

The residue field of a local ℚ-algebra has characteristic zero (Mathlib's algebraRat.charZero, made an instance; the Algebra ℚ structure is Mathlib's IsLocalRing.ResidueField.algebra).

theorem IsLocalRing.derivation_sum_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (s : Finset ι) (D : ι → Derivation R A M) (a : A) : (∑ i ∈ s, D i) a = ∑ i ∈ s, (D i) a

Evaluating a finite sum of derivations (Mathlib has Derivation.coeFnAddMonoidHom but no summed evaluation lemma).

theorem IsLocalRing.RegularCoords.x_mem_maximalIdeal {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) : c.x i ∈ maximalIdeal R

theorem IsLocalRing.RegularCoords.mem_maximalIdeal_sq_of_pderiv_mem {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {y : R} (hy : y ∈ maximalIdeal R) (h : ∀ (i : Fin n), (c.pderiv i) y ∈ maximalIdeal R) : y ∈ maximalIdeal R ^ 2

The partial derivatives lower the 𝔪-adic filtration by one step at the first level: an element of 𝔪 all of whose partials lie in 𝔪 lies in 𝔪². (A step of the change-of-coordinates argument; the Euler-identity computation ∂ᵢ (∑ aₗ xₗ) ≡ aᵢ (mod 𝔪).)

def IsLocalRing.RegularCoords.jacobian {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) : Matrix (Fin n) (Fin n) R

The Jacobian matrix Mᵢⱼ = ∂ᵢ x'ⱼ of a second family x' with respect to the coordinates c (index convention in the module docstring).

Equations

• c.jacobian x' = Matrix.of fun (i j : Fin n) => (c.pderiv i) (x' j)

@[simp]

theorem IsLocalRing.RegularCoords.jacobian_apply {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (i j : Fin n) : c.jacobian x' i j = (c.pderiv i) (x' j)

noncomputable def IsLocalRing.RegularCoords.transportPderiv {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) : Fin n → Derivation ℚ R R

The derivations ∂'ⱼ = ∑ₗ (M⁻¹)ⱼₗ ∂ₗ transported to a second family x'.

Equations

• c.transportPderiv x' j = ∑ l : Fin n, (c.jacobian x')⁻¹ j l • c.pderiv l

theorem IsLocalRing.RegularCoords.transportPderiv_apply {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (j : Fin n) (f : R) : (c.transportPderiv x' j) f = ∑ l : Fin n, (c.jacobian x')⁻¹ j l * (c.pderiv l) f

theorem IsLocalRing.RegularCoords.isUnit_jacobian {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : IsUnit (c.jacobian x')

If x' also generates the maximal ideal, the Jacobian matrix ∂ᵢ x'ⱼ is invertible over R. Uses dim R = n (regularity) through the minimal number of generators of the maximal ideal; see the module docstring for the argument.

theorem IsLocalRing.RegularCoords.transportPderiv_x {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (i j : Fin n) : (c.transportPderiv x' i) (x' j) = if i = j then 1 else 0

The transported derivations satisfy ∂'ᵢ x'ⱼ = δᵢⱼ.

noncomputable def IsLocalRing.RegularCoords.changeCoords {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (hcomm : ∀ (i j : Fin n) (f : R), (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)) : RegularCoords R n

A second generating system x' of the maximal ideal, together with the transported derivations, is again a coordinate structure, once the transported derivations are known to commute (a hypothesis here; changeCoordsOfSpans derives it from SpansDerivations).

Equations

• c.changeCoords x' hx' hcomm = { x := x', pderiv := c.transportPderiv x', span_x := hx', card := ⋯, pderiv_x := ⋯, pderiv_comm := hcomm }

@[simp]

theorem IsLocalRing.RegularCoords.changeCoords_x {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (hcomm : ∀ (i j : Fin n) (f : R), (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)) : (c.changeCoords x' hx' hcomm).x = x'

@[simp]

theorem IsLocalRing.RegularCoords.changeCoords_pderiv {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (hcomm : ∀ (i j : Fin n) (f : R), (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)) : (c.changeCoords x' hx' hcomm).pderiv = c.transportPderiv x'

theorem IsLocalRing.RegularCoords.pderiv_eq_sum_transportPderiv {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (i : Fin n) : c.pderiv i = ∑ j : Fin n, c.jacobian x' i j • c.transportPderiv x' j

The old derivations in terms of the transported ones: ∂ᵢ = ∑ⱼ Mᵢⱼ ∂'ⱼ.

theorem IsLocalRing.RegularCoords.span_range_transportPderiv {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : Submodule.span R (Set.range (c.transportPderiv x')) = Submodule.span R (Set.range c.pderiv)

The R-submodule of Derivation ℚ R R spanned by the transported derivations equals that spanned by the original ones.

def IsLocalRing.RegularCoords.SpansDerivations {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (k : Type v) [CommRing k] [Algebra k R] : Prop

The spanning condition [Kol07, Definition 73], [Wlo05, Definition 2.6.1]: the partial derivatives generate the derivations of R over the base k, δ = ∑ᵢ δ(xᵢ) ∂ᵢ for every k-derivation δ. Kollár takes the derivative ideal D(I) over all derivations and says the ∂/∂xᵢ generate them; here D(I) is defined with the fixed ∂ᵢ (Hironaka/Algebra/Local/Derivative.lean), and this predicate is what each instance supplies to identify the two (for smooth stalks, freeness of Ω_{X/k} on the dxᵢ; for analytic germs, uniqueness of Taylor coefficients).

Equations

• c.SpansDerivations k = ∀ (δ : Derivation k R R) (f : R), δ f = ∑ i : Fin n, δ (c.x i) * (c.pderiv i) f

theorem IsLocalRing.RegularCoords.SpansDerivations.transport {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (δ : Derivation ℚ R R) (f : R) : δ f = ∑ k : Fin n, δ (x' k) * (c.transportPderiv x' k) f

The spanning identity in transported coordinates: if the ∂ᵢ span the ℚ-derivations, then so do the ∂'ⱼ of a second generating system, δ = ∑ₖ δ(x'ₖ) ∂'ₖ. (Proof: δ(x'ₖ) = ∑ₗ δ(xₗ) Mₗₖ by the spanning identity, and ∑ₖ Mₗₖ (M⁻¹)ₖₚ = δₗₚ.)

theorem IsLocalRing.RegularCoords.transportPderiv_comm {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (i j : Fin n) (f : R) : (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)

If the ∂ᵢ span the ℚ-derivations, the transported derivations of a second generating system commute — their commutator is a derivation killing every x'ₖ, hence zero by the spanning identity. This discharges the commutation hypothesis of changeCoords for every coordinate structure with spanning derivations.

noncomputable def IsLocalRing.RegularCoords.changeCoordsOfSpans {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) : RegularCoords R n

Change of coordinates for a structure whose derivations span: no commutation hypothesis is needed.

Equations

• c.changeCoordsOfSpans hs x' hx' = c.changeCoords x' hx' ⋯

theorem IsLocalRing.RegularCoords.spansDerivations_changeCoords {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (hcomm : ∀ (i j : Fin n) (f : R), (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)) : (c.changeCoords x' hx' hcomm).SpansDerivations ℚ

The transported coordinate structure again has spanning derivations.