Snc coordinates at a closed point spread to an étale chart #
Hauser's proofs of [Hau14, Proposition 5.3] and [Hau14, Proposition 5.4] read the total transform of
an snc divisor "in local coordinates for which the blow-up is monomial": coordinates x_1, …, x_n
at
a point x₀ ∈ Z in which the centre is Z = (x_1 = ⋯ = x_r = 0) and each component of the divisor
through x₀ is a coordinate hyperplane (x_c = 0). [Kol07, Definition 24 (4)] provides such
coordinates on the stalk 𝒪_{X,x₀} (a regular system of parameters);
Hironaka.Scheme.Smooth.ChartIso computes the charts of the blow-up from a chart U ∋ x₀ of
étale coordinates adapted to Z (EtaleCoordinatesAdapted of
Hironaka.Scheme.Smooth.EtaleCoordinatesAdapted). This module spreads the snc data at a closed
point x₀ to such a chart on which, in addition, every component through x₀ is the coordinate
hyperplane of one of the étale coordinates and every other component misses the chart;
Hironaka.Scheme.Snc.TotalTransformOnCentre and Hironaka.Scheme.Snc.HypersurfaceCoordinates use
it.
Why the lemmas hold. The regular system of parameters z at x₀ lifts to sections w of an
affine open (exists_affineOpen_germ_eq); at a closed point of a scheme smooth of relative
dimension n their differentials form a basis of κ(x₀) ⊗ Ω, so on a smaller affine open the w
are étale coordinates. An equality of a stalk ideal with the ideal generated by the germs of
finitely many sections spreads to a basic open around x₀ because two finitely generated ideals
with the same localization at a prime agree after inverting a single element outside the prime
(exists_mem_map_eq_map_of_localization); finitely many such equalities hold simultaneously on the
basic open of the product. A component not through x₀ has closed support, so a basic open around
x₀ misses it. Adaptedness to Z on a further basic open is
exists_comap_eq_comap_coordinateSubspace after reindexing the parameters so that those of Z come
first (finsetEquiv of Hironaka.Scheme.Snc.ParameterSubset).
Sources: [Hau14, Proposition 5.3] (the proof); [Hau14, Proposition 5.4]; [Kol07, Definition 24 (4)].
An equality of a stalk ideal with the ideal generated by the germs of finitely many sections of
an affine open V ∋ x spreads to a basic open D(s) ∋ x of V: finitely generated ideals with the
same localization at the prime of x agree after inverting one element s outside it.
Finitely many such equalities hold simultaneously on the basic open of the product of the elements inverted for each of them.
A point outside finitely many closed sets has an affine neighbourhood inside a given affine open missing all of them.
Restriction of sections along U ≤ U' ≤ V composes.
An equality D(V) = ⟨S⟩ of ideals of an affine open restricts to a smaller affine open.
The reindexing of Fin n putting the members of s first.
Equations
Instances For
The chart of the proof of [Hau14, Proposition 5.3] ([Kol07, Definition 24 (4)]): snc data at a
closed point x₀ ∈ Z — a regular system of parameters z of 𝒪_{X,x₀} with
Z_{x₀} = (z_l : l ∈ s) and each component D i through x₀ equal to (z_{c i}) — spread to a
chart of étale coordinates adapted to Z on which every component through x₀ is the coordinate
hyperplane of the coordinate c' i (c' i < |s| exactly when c i ∈ s, i.e. when the component
contains Z near x₀) and every other component misses the chart.