The chart of the blow-up at a point of the exceptional divisor #
The local computation for the statement CP4 of the embedded desingularization
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) at a point q of the exceptional
divisor F of the blow-up π : B_Z X → X of a coordinate subspace Z_p = (z_c : c ∈ C) of a
regular system of parameters z at p = π(q).
- The pivot ([Kol07, Definition 60]; [Hau14, Proposition 5.4 (5)]):
F_qis principal and generated by the pullback of ONE centre coordinatez_{c₀},c₀ ∈ C—qlies in the chart ofz_{c₀}(exists_pivot_of_mem_support:F_q = (π^* z_c : c ∈ C)is a nonzero principal ideal of a local domain, so one generator suffices,exists_span_singleton_eq_of_span_range_eq). - The induced coordinates ([Hau14, Proposition 5.4 (6)];
exists_isRegularSystemOfParameters_induced, after the reindexing that puts the centre's coordinates last):w_i = π^* z_ifori ∉ Cand for the pivot,π^* z_i = w_i · π^* z_{c₀}for the other centre coordinates; thew_ivanishing atqare part of a regular system of parametersz'of𝒪_{B,q}(exists_inducedCoords). In the notation of the chain forms,ε = π^* e_{j₀},f_l = ε f_l'for the centre's chain equations,e_j = ε e_j'for the centre's other members,f_l,g,e_junchanged otherwise. - The chart datum
ChartAtpackages the pivot, the induced coordinates and the new parameters; the strict transforms of coordinate subspaces through the centre are computed in the chart (stalkIdeal_strictTransformAlong_eq_span_range: the saturation byεof the pulled-back ideal), and the mark-1transforms of the chain forms are read in the induced coordinates (stalkIdeal_controlledTransformAlong_chainKIdeal,stalkIdeal_controlledTransformAlong_chainIdeal) through the algebra ofHironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Algebra. The passage to the new regular system of parameters isHironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4NewCoords.
The pivot coordinate #
[Hau14, Proposition 5.4 (5)] at a point q of the exceptional divisor over a point where Z
is the coordinate subspace (z_c : c ∈ C): F_q is generated by the pullback of one of the centre
coordinates, which is nonzero.
The induced coordinates of the chart #
[Hau14, Proposition 5.4 (6)] in the pivot's chart (exists_isRegularSystemOfParameters_induced,
reindexed so that the centre's coordinates come last): with Z_p = (z_c : c ∈ C) and
F_q = (π^* z_{c₀}), c₀ ∈ C, there are induced coordinates w — w_i = π^* z_i off C and at
the pivot, π^* z_i = w_i · π^* z_{c₀} on C ∖ {c₀} — whose members vanishing at q are
coordinates of a regular system of parameters z' of 𝒪_{B,q}.
The chart datum #
The chart datum at q: the pivot c₀ ∈ C with F_q = (π^* z_{c₀}), the induced
coordinates w (w_i = π^* z_i off C and at the pivot, π^* z_i = w_i · π^* z_{c₀} on
C ∖ {c₀}), and a regular system of parameters z' of 𝒪_{B,q} containing the induced
coordinates vanishing at q (z' (τ i) = w i).
- c₀ : Fin n
The pivot: the centre coordinate whose pull-back generates
F_q. The pivot is a centre coordinate.
- hF : (Z.comap Z.blowUpπ).stalkIdeal q = Ideal.span {(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z self.c₀)}
F_q = (π^* z_{c₀}). - ε_ne : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z self.c₀) ≠ 0
The pivot's pull-back is nonzero.
The induced coordinates.
- hw (i : Fin n) : i ∉ C ∨ i = self.c₀ → self.w i = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z i)
Off the centre and at the pivot the induced coordinate is the pull-back.
- hw' (i : Fin n) : i ∈ C → i ≠ self.c₀ → (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z i) = self.w i * (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z self.c₀)
On the centre the pull-back is the induced coordinate times the pivot's pull-back.
- m : ℕ
The number of parameters at
q. A regular system of parameters at
q.- hz' : IsLocalRing.IsRegularSystemOfParameters self.z'
It is a regular system of parameters.
The induced coordinates vanishing at
qamong the parameters.- τ_injective : Function.Injective self.τ
Distinct induced coordinates are distinct parameters.
- hτ (i : { i : Fin n // self.w i ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q) }) : self.z' (self.τ i) = self.w ↑i
The parameter of an induced coordinate is the induced coordinate.
Instances For
At a point of the exceptional divisor over a point where the centre is a coordinate subspace of a regular system of parameters, a chart datum exists (the pivot, then the induced coordinates).
Definitional bridges: the transforms and the total transform's members #
The exceptional divisor is the pull-back of the centre (definitional unfolding).
The strict transform is the strict transform along the exceptional divisor (definitional unfolding).
The mark-1 transform is the controlled transform along the exceptional divisor (definitional
unfolding).
The index of a member of the total transform is inl j or inr u.
The ε-orders of a chart with centre coordinates C: e₀ = b(C), e_i = a_i(C), δ given.
Equations
- Hironaka.Resolution.epsOrderC C a b δ = Hironaka.Resolution.epsOrder (∑ k ∈ C, b k) (fun (i : Fin (r + 1)) => ∑ k ∈ C, a i k) δ
Instances For
The chart datum's arithmetic #
The exceptional coordinate ε = π^* z_{c₀}.
Equations
- D.ε = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z D.c₀)
Instances For
The ε-free induced coordinates: w with the pivot's entry replaced by 1.
Equations
- D.wHat = Function.update D.w D.c₀ 1
Instances For
The exceptional coordinate vanishes at a point of the exceptional divisor.
Hauser's chart substitution x_i ↦ x_i x_j on the centre, the identity off it: every
pull-back π^* z_i is ŵ_i · ε^{[i ∈ C]}.
The pull-back of a monomial: π^* z^a = ŵ^a · ε^{a(C)}.
The ε-order [i ∈ C] of a coordinate.
Off the pivot the ε-free coordinate is the induced coordinate.
An induced coordinate not vanishing at q is a unit.
Off the centre the induced coordinate vanishes at q (π^* is local).
Strict transforms in the chart #
The saturation defining a strict transform at q, with F_q = (ε).
The charts of the chain equations: if the pivot is one of the equations of Y then the
strict transform of Y misses q.
The chain coordinates of a coordinate subspace Y = (z (σ i) : i) through the centre vanish at
every point q of its strict transform on the exceptional divisor (no z (σ i) the pivot).
The strict transform of a coordinate subspace through the centre, given that its chain
coordinates vanish at q: the strict transform of Y = (z (σ i) : i) at q is (w (σ i) : i)
(the saturation of (ε^{δ_i} w (σ i) : i) by ε, a coordinate prime not containing ε).
The strict transform of a coordinate subspace through the centre: with Y_p = (z (σ i) : i)
and no z (σ i) the pivot, the strict transform of Y at q is (w (σ i) : i), provided q
lies on it — and then every w (σ i) vanishes at q.
The transforms of the chain forms in the chart #
The stalk of the mark-1 transform: the colon of the pull-back by (ε).
The pull-back of a K-shape in the chart: the equations gain ε^{[σ i ∈ C]}, the monomials
gain ε to their total exponent on C.
The pull-back of an un-isolated chain form in the chart.
The K-shape in the chart's induced coordinates: under the admissibility condition (★) in
the form of the ε-order conditions, the mark-1 transform of a K-shape at p has, at q, the
K-shape with equations ŵ (σ i), level monomials ε^{D_i} ŵ^{a_i} and top monomial
ε^{E_0 − 1} ŵ^{b}.
The un-isolated form in the chart's induced coordinates.