The chart functions are étale coordinates #
Kollár's coordinates (60.2) y_i "give local coordinates on a chart of B_Z X"
[Kol07, Definition 60]; here in the strong form that the chart functions are étale coordinates on
the chart. For a chart E of étale coordinates adapted to Z with coordinate ring map
φ = aeval v : k[t] → Γ(U) (étale, so flat), the chart ring Γ(U)[J/x_j] is the base change
Γ(U) ⊗_{k[t]} k[t][L/t_j] of the model chart ring (tensorHom, bijective by flatness), and
k[t][L/t_j] ≃ k[y] is the polynomial identification of the model chart
(coordinateSubspaceEquiv; the affine chart of [Hau14, Definition 4.12]), under which
y_i ↦ x_i/x_j (i < r, i ≠ j) and y_i ↦ x_i otherwise. Hence k[y] → Γ(U)[J/x_j],
y_i ↦ (the chart function y_i), is the base change of the étale φ along k[t] → k[y] and is
étale (Algebra.Etale.baseChange, RingHom.Etale.respectsIso).
etale_aeval_aux proves this with the k[t]-algebra structure of Γ(U) as an instance and the
ideal J and generator x_j as variables (subst-able), so that every term matches the codomain
of tensorHom syntactically; etale_aeval_chartCoordinates instantiates it for E. Not stated
in this form in the sources. Used to give the standard charts of a smooth blow-up their own
étale coordinates (Hironaka/Scheme/Snc/ChartSncData.lean).
The base change k[t][L/t_j] → Γ(U)[J/x_j] of the model chart ring along an étale
k[t] → Γ(U) is étale: through tensorHom (bijective by flatness) it is the inclusion of the
first factor into k[t][L/t_j] ⊗_{k[t]} Γ(U) (Algebra.Etale.baseChange).
The coordinate map k[y] → Γ(U)[J/x_j], y_i ↦ x_i/x_j (i < r, i ≠ j), y_i ↦ x_i
otherwise, is the base change of the model chart composed with the identification
k[y] ≃ k[t][L/t_j] of the model chart (coordinateSubspaceEquiv).
Generic form: for an étale k[t]-algebra structure on Γ(U) sending t_i to v_i, the map
k[y] → Γ(U)[J/x_j], y_i ↦ x_i/x_j (i < r, i ≠ j), y_i ↦ x_i otherwise, is étale: the
base change of k[t] → Γ(U) along the identification of the model chart k[t][L/t_j] ≃ k[y].
On the chart of x_j, the chart functions y_i = x_i/x_j (i < r, i ≠ j) and y_i = x_i
(otherwise) are étale coordinates: k[t] → Γ(U)[J/x_j], t_i ↦ y_i, is étale (the coordinates
(60.2) of [Kol07, Definition 60], which "give local coordinates on a chart").