The local model of the glued resolution, and its automorphisms over X #
Włodarczyk's independence of the canonical desingularization from the ambient manifold
[Wlo09, §4, (3)⇒(4)] and Kollár's uniqueness of the comparison [Kol07, Theorem 36, proof], read on
the glued spaces: the part of resolutionOn D over an open P inside a piece's base open is that
piece's local resolution over P (the chosen gluing's partIso); the local model — at a
point x of the base open of ANY piece embedding E over W, the part of the glued space R(X)
(an exhaustion gluing) over a small open P ∋ x is the part of E's local resolution over P,
over X (the exhaustion glue's partIso, the first item, and the mixed local transition
exists_localTransition_pair under the independence hind); R(X) has no non-trivial
automorphism over X on any part (the assembly exists_isoOver_of_localTransitions for the
exhaustion glue against itself); and, in any category of spaces over Z, the absence of
automorphisms makes the isomorphisms over Z to any other space unique.
Why. The functoriality of the resolution for isomorphisms of open subspaces
(ResolutionFunctorial.lean) glues local isomorphisms over X between R(X) and R(Y)|V (viewed
over X through φ⁻¹) along a cover of U, by exists_isIso_over_of_cover; the local
isomorphisms come from the local models of both sides at the same local resolution (the transport
transportAlongIso), and the uniqueness hypothesis from the last two items.
Not in the sources beyond the remarks cited; bookkeeping.
If the parts of A over O have no non-trivial automorphism over Z, the isomorphisms over
Z from the parts of A to the parts of B over O are unique: s' ≫ s⁻¹ is an automorphism
over Z (inv_over), hence the identity.
The part of resolutionOn D over an open P ⊆ U inside a piece's base open is the part of
that piece's local resolution, over X ([Wlo09, §4, (3)⇒(4)]):
resolutionOn D = Ṽ_D|Π⁻¹U read into the full glued space
(exists_iso_restrictOpen_restrictOpen_comap), the pair unfolded to the chosen gluing
(resolutionOnFullPair_eq_of_glues), and its partIso at P ≤ pieceDom i (W i).
The local model of the glued resolution ([Wlo09, §4, (3)⇒(4)]; [Kol07, Theorem 36, proof];
with the independence of the local resolution as hind): at a point x of the base open of ANY
piece embedding E over W, the part of the glued space over a small open P ∋ x is the part of
E's local resolution over P, over X — the exhaustion glue's partIso at Uₙ ∋ x,
exists_isoOver_resolutionOn_localResolution for the datum Dₙ at a piece containing x, and the
mixed local transition exists_localTransition_pair between that piece's embedding and E.
The glued space has no non-trivial automorphism over X on any part (Kollár's uniqueness,
[Kol07, Theorem 36, proof]; with the independence as hind): an isomorphism over X from the part
over O to itself is the identity — the assembly exists_isoOver_of_localTransitions for the
exhaustion glue against ITSELF, whose local transitions are the unique ones of
exists_isoOver_resolutionOn (D n) (D n) on O' ⊓ Uₙ; its uniqueness clause applied to t and
to 𝟙.