Two coordinate systems on one affine open #
Kollár completes two given functions x_1, x_1' at p by common local coordinates
x_2, …, x_n, the last of them chosen generally, so that x_1, x_2, …, x_n and
x_1', x_2, …, x_n "are both local coordinate systems" ([Kol07, 95], the proof of Theorem 92);
Włodarczyk likewise takes u_2, …, u_n such that u, u_2, …, u_n and v, u_2, …, u_n "form two
sets of parameters on U" ([Wlo05, Lemma 2.9.5], step (0) of the proof). The "general choice"
is made where the theorem is proved
(Hironaka/Resolution/Algebraic/MaximalContact/Theorem92.lean); here both systems are hypotheses:
at a closed point p of X smooth of relative dimension n over the perfect field k, u and
u with its i-th member replaced by v are regular systems of parameters of 𝒪_{X,p}. Then
(exists_etaleCoordinates_pair) there is one affine open U ∋ p carrying two coordinate systems
whose sections have germs u and update u i v at p and agree away from the i-th.
The argument, an assembly of the étale-coordinate lemmas: lift v, u_0, …, u_{n-1} to sections
of an affine open V ∋ p (exists_affineOpen_germ_eq); the differentials of each regular system
of parameters form a basis of κ(p) ⊗ Ω[𝒪_{X,p}⁄k]
(exists_basis_tensor_kaehlerDifferential_of_span_eq_maximalIdeal), so each lifted system is
étale on an affine open U_1, resp. U_2, around p (exists_etale_toAffineSpace_of_basis); a
basic open U ⊆ U_1 ∩ U_2 around p is affine and étaleness restricts to it
(etale_toAffineSpace_restrict). Restrictions compose (Mathlib's
TopCat.Presheaf.restrict_restrict) and preserve germs (germ_res_apply).
At a closed point p, two regular systems of parameters u and update u i v of 𝒪_{X,p}
differing in one member spread out to two coordinate systems on a common affine open U ∋ p,
with the prescribed germs at p and equal sections away from the i-th ([Kol07, 95]; the proof
of [Wlo05, Lemma 2.9.5]).