Local parameters adapted to a smooth center #
X is a scheme over a field k (f : X ⟶ Spec k), Z an ideal sheaf with closed subscheme
V(Z), x ∈ V(Z), Z_x = stalkIdeal Z x ⊆ 𝒪_{X,x} the stalk of Z, and
𝒪_{V(Z),x} = 𝒪_{X,x}/Z_x (stalkQuotientEquiv). For X smooth of relative dimension n and
V(Z) smooth of relative dimension n − r over a perfect field, this file produces Kollár's
adapted local coordinates: a regular system of parameters of 𝒪_{X,x} whose first r members
generate Z_x ("Z = (z_{j_1} = ⋯ = z_{j_s} = 0)", [Kol07, Definition 24, (4)]; the coordinates
"such that Z = (x_1 = ⋯ = x_r = 0)" of [Kol07, Definition 60]).
𝒪_{X,x}is regular forfsmooth ([TSPA, Tag 00TT];Scheme.isRegularAt_of_mem_smoothLocusat a point of the smooth locus, which is everything).𝒪_{X,x}/Z_x ≅ 𝒪_{V(Z),x}is regular forV(Z)smooth (the same forV(Z)); at a closed point ofV(Z)smooth of relative dimensionn − r, its dimension isn − r(Scheme.ringKrullDim_stalk_of_smoothOfRelativeDimension_of_isClosedforV(Z)).- At any
x ∈ V(Z),dim 𝒪_{X,x}/Z_x + r = dim 𝒪_{X,x}: the dimension formuladim 𝒪 + trdeg_k κ = nofHironaka/Algebra/RegularSmooth/SchemeForms.leanforXand forV(Z)givesdim 𝒪_{X,x} + t = nanddim 𝒪_{V(Z),x} + t' = n − rwitht, t'the transcendence degrees of the residue fields, which agree because the stalk map of the closed immersion induces ak-isomorphism of residue fields (residueFieldStalkEquiv, with thek-structuresScheme.Hom.stalkAlgebracompatible alongV(Z) ⟶ X ⟶ Spec k). - Adapted parameters: [TSPA, Tag 00NR] in the form
IsRegularLocalRing.exists_span_eq_maximalIdeal_and_eq_span_image_ltofHironaka/Algebra/Local/QuotientParameters.lean, applied toR = 𝒪_{X,x}andI = Z_x, gives a regular system of parametersywithZ_x = (y_0, …, y_{c-1});c = rbecausedim R/I + c = dim Randdim R/I + r = dim R. At a closed pointdim R = n, soyhasnmembers (exists_adaptedCoordinates).
The differentials of these parameters form a basis of the differentials at the point
(Hironaka/Scheme/Smooth/DifferentialBasis.lean), which is how they are spread out to étale
coordinates adapted to the center on an affine neighbourhood
(Hironaka/Scheme/Smooth/EtaleCoordinatesAdapted.lean).
The stalks of a scheme smooth over a field are regular local rings (the last sentence of
[TSPA, Tag 00TT]): every point lies in the smooth locus, and Scheme.isRegularAt_of_mem_smoothLocus
applies.
If V(Z) is smooth over k, 𝒪_{X,x}/Z_x ≅ 𝒪_{V(Z),x} is a regular local ring at every
x ∈ V(Z).
If V(Z) is smooth of relative dimension d over the perfect field k, then
dim 𝒪_{X,x}/Z_x = d at every closed point x ∈ V(Z) (the closed-point dimension formula,
applied to V(Z)).
The k-algebra structures Scheme.Hom.stalkAlgebra of 𝒪_{X,ι z} (through f) and of
𝒪_{V(Z),z} (through ι ≫ f) are compatible with the stalk map of ι : V(Z) ⟶ X.
The residue fields of 𝒪_{X,ι z} and 𝒪_{V(Z),z} have the same transcendence degree over
k (they are k-isomorphic through the stalk map of the closed immersion).
For X smooth of relative dimension n and V(Z) smooth of relative dimension n − r over
the perfect field k (r ≤ n), at every x ∈ V(Z), dim 𝒪_{X,x}/Z_x + r = dim 𝒪_{X,x}: the
dimension formula dim 𝒪 + trdeg_k κ = n of [TSPA, Tag 0A21, (10)] for X and for V(Z), whose
residue fields at x agree.
Adapted parameters at any point x ∈ V(Z): a regular system of parameters y of 𝒪_{X,x}
(with dim 𝒪_{X,x} members) whose first r members generate Z_x ([TSPA, Tag 00NR] together with
the dimension count ringKrullDim_quotient_stalkIdeal_add).
Adapted local coordinates at a closed point x ∈ V(Z): a regular system of parameters
y_0, …, y_{n-1} of 𝒪_{X,x} with Z_x = (y_0, …, y_{r-1}), Kollár's coordinates with
Z = (x_1 = ⋯ = x_r = 0) ([Kol07, Definition 24, (4)] and [Kol07, Definition 60]).