Independence of the embedding: uniqueness over the piece #
This module proves the UNIQUENESS half of the independence of the local resolution from the
embedding — two morphisms of the restricted local resolutions of a piece over an open N of the
piece, both compatible with the maps to the piece, are equal (localResolution_hom_ext_over) —
with its internals; then the GLUING bridge — the uniqueness packaged as the contract
Hom.UniqueOver of the general gluing tools of
Hironaka/Resolution/Analytic/Kol07Thm45/RestrictSetIncl.lean, the general-open existence
exists_isIso_localResolution_of_forall, its form at the common open and
localResolution_independent_of_local (the independence from its local form) — and the
FUNCTORIALITY leg resolution_commutes_localIso_of_independent (the commutation with local analytic
isomorphisms from the independence) with its two internals
(comp_localResolutionToPiece_transportAlongIso, embPreimage_transportAlongIso).
Mathematics (Kollár: "any two embeddings … become equivalent by an automorphism …, which
gives the required uniqueness" [Kol07, Theorem 36, proof]; Włodarczyk: the canonical
desingularization is independent of the choice of the ambient manifold [Wlo09, §4, (3)⇒(4)]). Let
Π = σ|_Ỹ : Ỹ → Y|_W be the local resolution map of a piece and Π_X : Ỹ → X|V its composite
with the identification of Y|_W with an open of the piece. Π is an isomorphism over the simple
locus (Y|_W).regularLocus (localResolutionMap_isIsoOver_reg); the points of Ỹ over the
singular locus are exactly those on the exceptional divisor E_r
(localResolutionMap_preimage_sing_eq_inter_exceptional); the points of Ỹ off E_r are dense,
Ỹ being non-singular (clause (3) of IsEmbeddedDesing;
mem_closure_cosupport_strictTransformSubspaceSeq_diff_support_of_isRegular). Hence two morphisms
ψ₁ ψ₂ : Ỹ₁|Π₁⁻¹N → Ỹ₂|Π₂⁻¹N over the piece coincide on the dense open Π₁⁻¹(regularLocus) (there
ψᵢ = Π₂⁻¹ ∘ Π₁), so on all points (the target is Hausdorff), and two morphisms of NON-SINGULAR
analytic spaces with the same underlying map are equal (hom_ext_toFun_of_isNonsingular,
Hironaka/AnalyticSpace/HomExtNonSingular.lean).
The argument. isNonsingular_localResolution: clause (3) of hbed.
mem_reg_iff_localResolutionToPiece: the read-down inv E.emb ∘ restrictedIdealHom W is an open
immersion (isOpenImmersion_homOfPullbackEq_of_injective; an isomorphism), and regularLocus
transports along open immersions (mem_reg_iff_of_isOpenImmersion).
injOn_localResolutionToPiece_preimage_reg: localResolutionMap_isIsoOver_reg.
dense_preimage_reg_localResolutionToPiece: the two density results named above. The uniqueness:
eqOn_of_comp_eq_of_dense on the restricted spaces, then hom_ext_toFun_of_isNonsingular.
Conventions. Every restriction here is at an open set (N open by hypothesis; Π ⁻¹' N
open); the restriction of a space to a non-open set is by convention the whole space (openOf).
Not in the sources beyond the two remarks; bookkeeping.
The local resolution is non-singular: clause (3) of hbed at the piece's triple over W
— the final strict transform Ỹ is smooth ([Wlo09, Theorem 2.0.2(3)]).
The restriction-of-a-quotient map restrictedIdealHom W : Sp(W)/𝓘|W → Sp(G)/𝓘 is an open
immersion: isOpenImmersion_homOfPullbackEq_of_injective — it is the closed-subspace morphism
along the open inclusion W ↪ G, injective.
The inverse of the piece's embedding is an open immersion — an isomorphism is one (Mathlib's
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_isIso).
A point of the local resolution lies over a simple point of Sp(W)/𝓘|W iff it lies over a
simple point of the piece X|V (simple points in Hironaka's sense, [Hir64, Ch. 0, §1]: the
local ring is regular): the read-down inv E.emb ∘ restrictedIdealHom W is an open immersion, and
regularLocus transports along open immersions (mem_reg_iff_of_isOpenImmersion).
The map to the piece is injective over the simple points of the piece:
localResolutionMap_isIsoOver_reg — Π restricted over (Sp(W)/𝓘|W).regularLocus is an
isomorphism, hence injective on its preimage — read down to the piece through the injective
read-down map.
The points of the local resolution over the simple points of the piece are dense: by
localResolutionMap_preimage_sing_eq_inter_exceptional they are the points off the exceptional
divisor E_r, and by mem_closure_cosupport_strictTransformSubspaceSeq_diff_support_of_isRegular
these accumulate at every point of the non-singular Ỹ.
The underlying map of the restriction f.restrictSet N on points: (f|_{f⁻¹N} p).1 = f p.1
(Hom.restrictSet_eq_restrictTo, Hom.toFun_restrictTo).
Uniqueness over the piece (Kollár's "the required uniqueness", [Kol07, Theorem 36, proof];
the independence of the choice of ambient manifold, [Wlo09, §4, (3)⇒(4)]): two morphisms of the
restricted local resolutions over an OPEN N of the piece, both compatible with the maps to the
piece, are equal — they agree on the dense open over the simple points
(injOn_localResolutionToPiece_preimage_reg, dense_preimage_reg_localResolutionToPiece,
eqOn_of_comp_eq_of_dense), hence on all points, hence as morphisms of non-singular spaces
(isNonsingular_localResolution, isNonsingular_restrictSet,
hom_ext_toFun_of_isNonsingular).
The uniqueness as the contract of the gluing tools: the local resolution maps to the piece
have unique morphisms over the piece (Hom.UniqueOver,
Hironaka/Resolution/Analytic/Kol07Thm45/RestrictSetIncl.lean).
Local isomorphisms over the piece around every point of an open O glue to an isomorphism
over O ([Kol07, Theorem 36, proof]; [Wlo09, §4, (3)⇒(4)]): the general gluing
Hom.UniqueOver.exists_isIso_restrictSetTo of
Hironaka/Resolution/Analytic/Kol07Thm45/RestrictSetIncl.lean at the local resolution maps, with
the uniqueness in both directions as the contract; IsIso of analytic spaces is the
K-local-ringed one (Hom.isIso_iff_isIso_toKLocallyRingedSpace).
The EXISTENCE half of the independence from its local form: the local isomorphisms over
the piece glue to an isomorphism over the common open embPreimage W₁ ∩ embPreimage W₂
(exists_isIso_localResolution_of_forall at that open, isOpen_embPreimage).
The independence from its local form ([Kol07, Theorem 36, proof]; [Wlo09, §4, (3)⇒(4)]):
the unique isomorphism over the common open E₁.embPreimage W₁ ∩ E₂.embPreimage W₂ from the
conclusion of localResolution_independent_local (LocalResolutionShear.lean) as the hypothesis
hloc — existence by the gluing (exists_isIso_localResolution_of_local), uniqueness by
localResolution_hom_ext_over at the common open.
The map to the piece of the transported embedding F.transportAlongIso φ hφ (the transport
of an embedding along an isomorphism of pieces; compare the lifting of a smooth morphism to the
ambient spaces in [Kol07, Lemma 41]) lies over φ: φ ∘ Π_{F'} = Π_F — the transport keeps the
ambient, the ideal and the local resolution, and its embedding is F.emb ∘ φ, so
inv (φ ≫ F.emb) ≫ φ = inv F.emb.
The points of the piece X|V over W' for the transported embedding are the preimage under
φ of the points of Y|U over W' ((F.transportAlongIso φ hφ).ambientPoint x = F.ambientPoint (φ x) by definition of the transport).
The commutation with local isomorphisms from the independence (Kollár's reduction of the
functoriality for smooth morphisms to the embedded case, [Kol07, Theorem 36, proof];
[Wlo09, Theorem 6.0.6(2)]): the unique isomorphism over φ of the restricted local resolutions
from the independence over X|V at the fixed bed as the hypothesis hind — the independence
at E and the transported embedding F.transportAlongIso φ hφ (same ambient, same ideal, the
embedding F.emb ∘ φ), the two opens identified through φ (an isomorphism, hence injective:
E.embPreimage W ∩ F'.embPreimage W' = φ⁻¹(φ(E.embPreimage W) ∩ F.embPreimage W')), and the
general transport Hom.existsUnique_isIso_restrictSetTo_transport of
Hironaka/Resolution/Analytic/Kol07Thm45/RestrictSetIncl.lean. The hypothesis IsEmbeddedDesing
enters only through hind.