Uniqueness of lifts through the charted blow-up #
Hironaka's universal property (**) of the blowing-up [Hir64, Ch. 0, §2, p. 123] for the charted
blow-up π : M' → M of an analytic manifold along a closed submanifold Y ([BM88, 4.1]), the
uniqueness half: two K-morphisms g₁ g₂ : Y' → Sp(M') from an analytic K-space with
g₁ ≫ Sp(π) = g₂ ≫ Sp(π) = f', where the inverse image of the centre along f' is invertible,
coincide (lift_unique_of_comp_eq). Not proved in the sources; the argument:
The proof reads the blow-up charts ([BM88, 4.1 (2)]): in a chart Φ of index i over an adapted
chart φ of Y, π^* z_{σ i} = u_{σ i}, π^* z_{σ k} = u_{σ i} · u_{σ k} for k ≠ i and
π^* z_j = u_j off the block. Hence the coordinates of a lift g in Φ are forced by
f' = g ≫ Sp(π) (pullback_coord_self, pullback_coord_of_ne, pullback_coord_off): the
scaling coordinate is f'^* z_{σ i}, which generates the (invertible) inverse-image ideal of the
centre and is therefore a non-zero-divisor (stalkIdeal_comap_comp_eq_span,
mem_nonZeroDivisors_pullback_coord), so the ratio coordinates are recovered by cancellation and
the off-block ones directly (stalkMap_coord_eq_of_mem_source). The same cancellation shows that
g₂ z lies in the chart containing g₁ z (mem_source_of_lift). Equal coordinate germs give
equal base points, since a nonzero constant is a unit (base_eq_of_coord), and two K-morphisms
into Sp(M') with the same base point and the same coordinate germs have the same stalk map by
ringHom_ext_of_coord' (Hironaka/AnalyticSpace/Manifold/FullyFaithful.lean;
stalkMap_eq_of_coord). Off the centre π is a local diffeomorphism and the coordinates of a
transported chart are forced directly (germMap_coord_transportChart).
General lemmas: hom_ext_of_coord_chart — two K-morphisms from an analytic space into Sp(M)
that agree on the coordinate germs of a chart at every point are equal — with its ingredients
base_eq_of_coord and stalkMap_eq_of_coord, the composite stalk-map formula
stalkMap_comp_ofManifoldHom_apply, and the residue toolkit stalkMap_coord_sub_constAt_mem,
eq_of_sub_constAt_mem, mul_sub_constAt_mem (a germ's residue is the constant it is congruent
to modulo 𝔪_x). Used by Hironaka/Resolution/Analytic/Kol07Thm45/PieceLemma39.lean and
PieceLemma39Hom.lean.
The stalk map of g ≫ Sp(π) at z is the stalk map of g after the germ map germMap π at
g z (stalkMap_ofManifoldHom_eq_germMap).
Transport of a pulled-back coordinate germ along an equality of morphisms into Sp(M).
Two morphisms into Sp(M') over the same morphism into Sp(M) have base points with the same
image under π.
Two K-morphisms into Sp(M') with the same base point at z and the same action on the
constants and on the coordinate germs of a chart at that point have the same stalk map at z
(ringHom_ext_of_coord'; the stalks of an analytic space are Noetherian; compare the local
coordinations of [Hir64, Ch. 0, §1, p. 120]).
Residues along a K-morphism into Sp(M'): a coordinate germ u_j of a chart Φ pulled back
along g is congruent modulo 𝔪_x to the constant u_j(g x).
Residues are unique: a germ congruent modulo 𝔪_x to two constants has equal constants (a
nonzero constant is a unit, isUnit_constAt).
Residues are multiplicative.
Two K-morphisms into Sp(M') whose images of z lie in a chart Φ and which pull the
coordinate germs of Φ back to the same germs have the same base point at z — the constant
u_j(g₁ z) - u_j(g₂ z) lies in 𝔪_z, and a nonzero constant is a unit (isUnit_constAt).
Two K-morphisms from an analytic K-space into Sp(M') that agree, at every point z, on
the coordinate germs of some chart containing both images of z are equal — base points by
base_eq_of_coord, stalk maps by stalkMap_eq_of_coord, then Mathlib's
SheafedSpace.hom_stalk_ext.
The scaling coordinate is forced ([BM88, 4.1 (2)], germMap_coord_self):
(g ≫ π)^* z_{σ i} = g^* u_{σ i}.
A ratio coordinate (germMap_coord_of_ne): (g ≫ π)^* z_{σ k} = g^* u_{σ i} · g^* u_{σ k} for
k ≠ i.
An off-block coordinate (germMap_coord_off): (g ≫ π)^* z_j = g^* u_j.
If the stalk of the centre's ideal sheaf D at π (g z) is spanned by the adapted coordinates,
the stalk at z of the inverse image of D along g ≫ π is generated by the pulled-back scaling
coordinate (g ≫ π)^* z_{σ i} — every other generator is a multiple of it by a ratio coordinate
([Hir64, Ch. 0, §2, p. 123]; [BM88, 4.1]).
Under Hironaka's invertibility hypothesis on the test pair [Hir64, Ch. 0, §2, p. 123] the
pulled-back scaling coordinate is a non-zero-divisor — it generates the same stalk ideal as a
non-zero-divisor, so it differs from it by a unit
(exists_unit_mul_eq_of_span_range_eq_span_singleton).
In a blow-up chart containing the images of z under both lifts, the lifts pull the chart's
coordinate germs back to the same germs — the scaling coordinate is f'^* z_{σ i} for both, the
ratio coordinates follow by cancelling that non-zero-divisor, the off-block ones are f'^* z_j
for both.
The second lift's image lies in the blow-up chart Φᵢ containing the first lift's image. In a
blow-up chart Φₖ containing g₂ z the coordinate u_{σ i} pulls back to a unit — its product
with g₁^* u_{σ k} is 1 after cancelling the non-zero-divisor f'^* z_{σ i} — so its value at
g₂ z is nonzero and the chart change mem_source_of_coord_ne_zero lands g₂ z in Φᵢ; for
k = i the two charts have the same source.
Uniqueness of the lift through the charted blow-up (Hironaka's (**),
[Hir64, Ch. 0, §2, p. 123]; [BM88, 4.1]): two K-morphisms g₁ g₂ : Y' → Sp(M') with
g₁ ≫ Sp(π) = g₂ ≫ Sp(π), the inverse image of the centre along that composite being invertible,
coincide. Over the centre the chart coordinates are forced (stalkMap_coord_eq_of_mem_source);
off it π is a local diffeomorphism and the transported chart's coordinates are forced
directly.