Local coordinates at a point

Kollár's "local coordinates z_1, …, z_n ∈ 𝔪_x in the maximal ideal of the local ring 𝒪_{X,x}" of a smooth variety [Kol07, Definition 24] are a regular system of parameters — a family generating 𝔪_x with as many members as dim 𝒪_{X,x} (IsRegularSystemOfParameters, stated here in its unfolded form span (range z) = 𝔪 ∧ n = dim). They exist at every point of a scheme smooth over a field (the stalks are regular local rings, and a regular local ring has a generating system of 𝔪 with dim members by definition), they lie in 𝔪 ∖ 𝔪² and are a basis of 𝔪/𝔪², and distinct coordinates generate distinct ideals (an element of 𝔪 generating the same ideal as z_j is a unit multiple of z_j, so its class in 𝔪/𝔪² is proportional to that of z_j; a basis has no two proportional members).

theorem AlgebraicGeometry.exists_fin_span_eq_maximalIdeal (R : Type u) [CommRing R] [IsRegularLocalRing R] : ∃ (n : ℕ) (z : Fin n → R), Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑n = ringKrullDim R

A regular local ring has a regular system of parameters indexed by Fin n, n = dim R — a generating family of 𝔪 with spanFinrank 𝔪 = dim R members.

theorem AlgebraicGeometry.mem_maximalIdeal_and_notMem_sq_of_span_eq {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑n = ringKrullDim R) (i : Fin n) : z i ∈ IsLocalRing.maximalIdeal R ∧ z i ∉ IsLocalRing.maximalIdeal R ^ 2

The members of a regular system of parameters lie in 𝔪 and outside 𝔪² (Kollár's "z_1, …, z_n ∈ 𝔪_x").

theorem AlgebraicGeometry.span_singleton_ne_of_ne {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑n = ringKrullDim R) {i j : Fin n} (hij : i ≠ j) : Ideal.span {z i} ≠ Ideal.span {z j}

Distinct members of a regular system of parameters generate distinct ideals — their classes form a basis of 𝔪/𝔪², and two members generating the same ideal have proportional classes.

theorem AlgebraicGeometry.exists_fin_span_eq_maximalIdeal_stalk {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (x : ↥X) : ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)

At every point of a scheme smooth over k there are local coordinates in the sense of [Kol07, Definition 24], a regular system of parameters of 𝒪_{X,x}.