Lifting local analytic isomorphisms to the resolutions #
Włodarczyk's canonical desingularization is functorial with respect to local analytic
isomorphisms: "for any local analytic isomorphism φ : Y' → Y there is a natural lifting
φ̃ : Ỹ' → Ỹ which is a local analytic isomorphism" [Wlo09, Theorem 2.0.1 (3)]; for Kollár these
are the étale morphisms of his clause (5), "R commutes with smooth K-morphisms"
[Kol07, Theorem 45 (5)]. The lifting of isomorphisms between open subspaces of inputs (the unique
isomorphism R(X')|_{Π⁻¹U'} ≅ R(X)|_{Π⁻¹V} over χ : X'|_{U'} ≅ X|_V) is the only morphism over
χ, by rigidity, and extends to every local analytic isomorphism φ : X' ⟶ X between inputs by
gluing; these are the two clauses of ResolutionAssignment.LiftsLocalIsomorphisms
(ResolutionAssignment.liftsLocalIsomorphisms_of_existsUnique_lift):
- Local lifts. Around each point of
X',φis an isomorphismχof an openU'onto an open subspaceX|_V; the liftψ₀ofχ, followed by the open immersionR(X)|_{Π⁻¹V} → R(X), is a morphismR(X')|_{Π⁻¹U'} → R(X)overφ; the opensΠ⁻¹U'coverR(X'). - Rigidity over
φ(ResolutionAssignment.eq_of_comp_map_eq_of_isLocalIso): two morphismsh₁ h₂ : A → R(X)from a non-singular spaceAoverX'(throughp : A → X'withp⁻¹(Reg X')dense) lying overφ ∘ pare equal. A local analytic isomorphism carries simple points to simple points (Hom.IsLocalIso.mem_regularLocus), so overp⁻¹(Reg X')both land inΠ⁻¹(Reg X), whereΠ_Xis an isomorphism (clause (2)), and there both are the lift ofφ ∘ pthroughΠ_X; a morphism out of a non-singular space is determined on a dense open subset (hom_ext_of_dense,Hironaka/AnalyticSpace/HomExtDense.lean). The density ofΠ⁻¹(Reg X')inR(X')is clause (3): its complement is the support of a simple normal crossings divisor (Hom.IsStrongResolution.dense_preimage_regularLocus). - Gluing. The local lifts agree on the overlaps by rigidity and glue
(
KLocallyRingedSpace.glueOfCover) toψ : R(X') → R(X), which lies overφ(equality of morphisms is local on the source), is a local analytic isomorphism (the local lifts are its restrictions), and is the only morphism overφ, by rigidity. The lift of an isomorphismχ : X'|_{U'} ≅ X|_Vis likewise the only morphism overχ: composed with the inverse of another lift it lies over the identity ofX|_V. - Restriction (
LiftsLocalIsomorphisms.lift_restrict): for everyRlifting local analytic isomorphisms, the lift ofφrestricts over every openU'whichφmaps isomorphically onto an open subspace to the lift of that isomorphism, since the restriction lies over it and the lift is the only morphism over it. - Naturality (
LiftsLocalIsomorphisms.lift_comp,lift_id): the lift of a composite is the composite of the lifts and the lift of an identity is the identity, by the uniqueness; composites of local analytic isomorphisms are local analytic isomorphisms (Hom.IsLocalIso.comp), as are identities, isomorphisms and open immersions.
The sources state the clause and do not prove it in this form; the argument is the gluing of [Kol07, Proposition 37, proof] with the uniqueness of [Kol07, Theorem 36, proof].
Local analytic isomorphisms #
A local analytic isomorphism maps the open U' of its definition into the open V.
The isomorphism χ of the definition of a local analytic isomorphism is the restriction
Hom.restrictTo of φ (lifts through an open immersion are unique).
A local analytic isomorphism has bijective stalk maps: at x' it is the restriction of
φ to an open neighbourhood, an isomorphism onto an open subspace
(bijective_stalkMap_of_isIso_restrictTo).
A local analytic isomorphism carries simple points to simple points: the stalk map at x'
is a ring isomorphism 𝒪_{X,φ x'} ≅ 𝒪_{X',x'}, and regularity is invariant under ring
isomorphisms.
At every point, a local analytic isomorphism φ restricts to an isomorphism of open
subspaces, in the form Hom.restrictTo φ U' V of the restriction.
Composites of local analytic isomorphisms are local analytic isomorphisms: at x, with
U₁ ∋ x and U₂ ∋ φ₁ x the injectivity opens of φ₁ and φ₂, the composite maps the open
U := U₁ ∩ φ₁⁻¹U₂ bijectively onto the open φ₂(φ₁(U)) with bijective stalk maps, so it
restricts to an isomorphism there (isIso_restrictTo_of_bijOn_of_bijective_stalkMap).
The identity is a local analytic isomorphism.
The preimage of the simple locus under a strong resolution is dense: its complement is
the support of a simple normal crossings divisor (isSncDivisorSet_of_isSncBoundary,
IsSncDivisorSet.dense_compl).
Rigidity over a local analytic isomorphism #
Rigidity over φ: for a local analytic isomorphism φ : X' ⟶ X and Π_X an isomorphism
over the simple locus, two morphisms h₁ h₂ : A ⟶ R(X) from a non-singular space A over X'
(through p, with p⁻¹(Reg X') dense) that lie over φ ∘ p are equal: over p⁻¹(Reg X') both
land in Π⁻¹(Reg X) (Hom.IsLocalIso.mem_regularLocus) and are the lift of φ ∘ p through the
isomorphism Π_X|_{Reg X}, so they agree on a dense open subset (hom_ext_of_dense).
Rigidity over an open subspace: for Π_T a strong resolution, the only endomorphism h
of R(T)|_{Π⁻¹V} over the identity of T|_V (h ≫ Π_T|_V = Π_T|_V) is the identity: h
followed by the inclusion into R(T) and the inclusion itself lie over the identity of T, and
their source R(T)|_{Π⁻¹V} is non-singular (eq_of_comp_map_eq_of_isLocalIso).
The glued lift #
Lifting local analytic isomorphisms from the lifting of isomorphisms of open subspaces
([Wlo09, Theorem 2.0.1 (3)] from clause (5) of [Kol07, Theorem 45]): a resolution assignment R
on inputs whose values are strong resolutions and which lifts every isomorphism between open
subspaces of inputs to exactly one isomorphism over it (h5) lifts local analytic isomorphisms
(LiftsLocalIsomorphisms). The lift of an isomorphism φ of open subspaces is the only morphism
over φ: for another one ψ', the composite ψ⁻¹ ≫ ψ' lies over the identity, hence is the
identity by rigidity (eq_of_comp_map_eq_of_isLocalIso). For a local analytic isomorphism, the
local lifts of h5, one for each point of X', agree on the overlaps by rigidity over φ and
glue (KLocallyRingedSpace.glueOfCover); the glued morphism lies over φ, is a local analytic
isomorphism and is unique, by rigidity.
Naturality #
The lifts respect composition: for R lifting local analytic isomorphisms, the lift of a
composite φ₁ ≫ φ₂ of local analytic isomorphisms between inputs is the composite of the lifts, by
the uniqueness of the lift.
The lifts respect identities: for R lifting local analytic isomorphisms, the lift of the
identity of an input is the identity.
Restriction to the lifts of isomorphisms of open subspaces #
The lift of a local analytic isomorphism restricts to the lifts of isomorphisms of open
subspaces: for R lifting local analytic isomorphisms and a morphism ψ : R(X') → R(X) over
φ : X' → X (such as the lift of a local analytic isomorphism φ), over every open U' ⊆ X'
which φ maps isomorphically onto an open subspace X|_V (through χ), every morphism
ψ₀ : R(X')|_{Π⁻¹U'} → R(X)|_{Π⁻¹V} over χ, in particular the lift of χ, is the restriction
of ψ: the restriction of ψ lies over χ, and the lift of χ is the only morphism over it.