A common complement for two regular systems of parameters

Kollár, in the proof of the formal equivalence theorem [Kol07, 95], completes the equations x₁, x₁' of the two hypersurfaces of maximal contact and the equations x₂, …, x_{s+1} of the divisors Eⁱ to the local coordinate systems x₁, x₂, …, xₙ and x₁', x₂, …, xₙ by "a general choice of x_{s+2}, …, xₙ". This is the existence of a common complement of the two subspaces ⟨x̄₁, ē⟩, ⟨x̄₁', ē⟩ of 𝔪/𝔪². No genericity or infinite-field argument is needed: a union of two proper subspaces never exhausts a vector space, and here the construction is explicit. The ring-level statement is not in the sources in this form; it is used for the coordinates adapted to two hypersurfaces of maximal contact in Hironaka/Resolution/Algebraic/MaximalContact/Coordinates.lean.

Why it holds. Let R be a regular local ring with residue field κ, z = (z₀, …, z_d) a regular system of parameters (its classes z̄ᵢ form a basis b of 𝔪/𝔪², Hironaka/Algebra/Local/RegularSystem.lean), p₀ the index of the coordinate to be exchanged (Kollár's x₁ = z_{p₀}), T ∌ p₀ the set of indices of the protected coordinates (the equations of the Eⁱ through p), and x' ∈ 𝔪 (Kollár's x₁') whose class does not lie in ⟨z̄ᵢ : i ∈ T⟩ (because x₁' and the Eⁱ have simple normal crossings). Expand x̄' = ∑ᵢ rᵢ z̄ᵢ.

• If r_{p₀} ≠ 0, take y := (zᵢ)_{i ≠ p₀}: then (z_{p₀}, y) is z up to order, and (x', y) generates 𝔪 because z̄_{p₀} = r_{p₀}⁻¹ (x̄' − ∑_{i ≠ p₀} rᵢ z̄ᵢ) lies in the span of the classes of x' and y.
• If r_{p₀} = 0, some j₀ ∉ T, j₀ ≠ p₀, has r_{j₀} ≠ 0 (otherwise x̄' ∈ ⟨z̄_T⟩); take y := (zᵢ)_{i ≠ p₀} with z_{j₀} replaced by z_{j₀} + z_{p₀} (Kollár's "general choice": one coordinate is tilted by x₁). Then (z_{p₀}, y) still generates 𝔪 (z_{j₀} = (z_{j₀} + z_{p₀}) − z_{p₀}), and for (x', y): z̄_{j₀} = r_{j₀}⁻¹ (x̄' − ∑_{i ≠ p₀, j₀} rᵢ z̄ᵢ) and then z̄_{p₀} = (z̄_{j₀} + z̄_{p₀}) − z̄_{j₀} lie in the span, so all of b does.

In both cases the protected coordinates zᵢ, i ∈ T, are members of y unchanged, and a family of d + 1 = dim R elements of 𝔪 whose classes span 𝔪/𝔪² generates 𝔪 (Nakayama, span_eq_maximalIdeal_iff_span_toCotangent_eq_top of Hironaka/Algebra/Local/RegularSystem.lean).

theorem IsLocalRing.mem_maximalIdeal_of_eq_span {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {ι : Type u_2} {z : ι → R} (hz : maximalIdeal R = Ideal.span (Set.range z)) (i : ι) : z i ∈ maximalIdeal R

Members of a generating family of 𝔪 lie in 𝔪.

noncomputable def IsLocalRing.tiltedComplement {R : Type u_1} [CommRing R] {d : ℕ} (z : Fin (d + 1) → R) (p₀ : Fin (d + 1)) (t : Fin d → R) : Fin d → R

A regular system of parameters, one index removed and one coordinate possibly tilted by the removed one: the family y of exists_cons_regularSystem_common.

Equations

• IsLocalRing.tiltedComplement z p₀ t j = z (p₀.succAbove j) + t j * z p₀

theorem IsLocalRing.tiltedComplement_apply {R : Type u_1} [CommRing R] {d : ℕ} (z : Fin (d + 1) → R) (p₀ : Fin (d + 1)) (t : Fin d → R) (j : Fin d) : tiltedComplement z p₀ t j = z (p₀.succAbove j) + t j * z p₀

theorem IsLocalRing.span_range_cons_tiltedComplement {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {d : ℕ} (z : Fin (d + 1) → R) (hz : maximalIdeal R = Ideal.span (Set.range z)) (p₀ : Fin (d + 1)) (t : Fin d → R) : maximalIdeal R = Ideal.span (Set.range (Fin.cons (z p₀) (tiltedComplement z p₀ t)))

(z_{p₀}, y) generates 𝔪 whenever z does (the tilt is invertible).

theorem IsLocalRing.exists_cons_regularSystem_common {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {d : ℕ} (z : Fin (d + 1) → R) (hz : maximalIdeal R = Ideal.span (Set.range z)) (p₀ : Fin (d + 1)) (T : Set (Fin (d + 1))) (hT : p₀ ∉ T) (x' : R) (hx' : x' ∈ maximalIdeal R) (b : Module.Basis (Fin (d + 1)) (ResidueField R) (CotangentSpace R)) (hb : ∀ (i : Fin (d + 1)), b i = (maximalIdeal R).toCotangent ⟨z i, ⋯⟩) (hv : (maximalIdeal R).toCotangent ⟨x', hx'⟩ ∉ Submodule.span (ResidueField R) (⇑b '' T)) : ∃ (y : Fin d → R), (∀ i ∈ T, ∃ (j : Fin d), y j = z i) ∧ maximalIdeal R = Ideal.span (Set.range (Fin.cons (z p₀) y)) ∧ maximalIdeal R = Ideal.span (Set.range (Fin.cons x' y))

For a regular system of parameters z of R, an index p₀, a set T ∌ p₀ of protected indices and x' ∈ 𝔪 whose class in 𝔪/𝔪² is not in the span of the classes z̄ᵢ, i ∈ T, there is a family y of d elements containing every zᵢ, i ∈ T, such that both (z_{p₀}, y) and (x', y) are regular systems of parameters (Kollár's "for a general choice of x_{s+2}, …, xₙ", [Kol07, 95], made explicit).