Étale coordinates adapted to a smooth center #
At a closed point x of a center Z smooth of relative dimension n − r in X smooth of
relative dimension n over the perfect field k, there are étale coordinates adapted to Z: an
affine open U ∋ x with an étale coordinate morphism g : U ⟶ 𝔸ⁿ_k and
Z ∩ U = g⁻¹(V(t_0, …, t_{r-1})) (nonempty_etaleCoordinatesAdapted). This is Kollár's choice
of local coordinates with Z = (z_{j_1} = ⋯ = z_{j_s} = 0) near x ([Kol07, Definition 24, (4)];
Z = (x_1 = ⋯ = x_r = 0) in [Kol07, Definition 60]), with the coordinates made an étale chart.
The construction assembles the preceding modules: exists_adaptedCoordinates
(AdaptedCoordinates.lean) gives a regular system of parameters y of 𝒪_{X,x} with
Z_x = (y_0, …, y_{r-1}); the y_i lift to sections w_i of an affine open around x
(exists_affineOpen_germ_eq); their differentials 1 ⊗ d w_i form a basis of κ(x) ⊗ Ω
(DifferentialBasis.lean); so (w_i) are étale coordinates on a smaller affine open
(exists_etale_toAffineSpace_of_basis); and Z ∩ U = g⁻¹(L) holds on a yet smaller one
(exists_comap_eq_comap_coordinateSubspace, Adapted.lean), where the coordinates stay étale
(etale_toAffineSpace_restrict).
These charts cover the closed points of the center; Hironaka/Scheme/Smooth/BlowUpSmooth.lean and
ExceptionalDivisor.lean glue the smoothness of B_Z X and of its exceptional divisor from them.
At a closed point x of a center V(Z) smooth of relative dimension n − r in X smooth of
relative dimension n, there are étale coordinates adapted to Z ([Kol07, Definition 24, (4)]
and [Kol07, Definition 60], as an étale chart).