The local resolution of a restricted piece embedding #
Włodarczyk: the canonical resolution pulled back along a local analytic isomorphism is an
extension of the canonical resolution of the source [Wlo09, Theorem 6.0.6(2)], and an open
embedding of germs Y_Z ⊂ Y_{Z'} extends to an open embedding U_Z ⊂ U_{Z'} of the ambient
manifolds [Wlo09, §4, (3)⇒(4)]; Kollár: a blow-up sequence functor commuting with smooth morphisms
gives, along an open immersion, the pull-back with the empty blow-ups deleted [Kol07, 34.1]. For
the restricted piece embedding E|V' = E.restrictPiece hV' hsub of PieceRestrict.lean and a
relatively compact open W' of the shrunk ambient G', the local resolution of E|V' over W'
is identified with the local resolution of E over the image pieceAmbientIncl '' W' ⊆ G — the
value of the functor on the pulled-back triple is the pull-back of its value on the image open,
empty blow-ups erased: the commutation of IsEmbeddedDesing with local analytic isomorphisms
(CommutesWithLocalIsos, the family functor's hbed.2 n) at the local analytic isomorphism
pieceAmbientIncl restricted to W' (a diffeomorphism onto its image, restrictPieceIncl). Then
the final strict transforms correspond under the last-stage lift
(strictTransformSubspaceSeq_last_of_eq_pullback_eraseEmpty, LocalResolutionRestrict.lean), the
lift is a diffeomorphism (pullbackLiftLastDiffeomorphOfBijective), and the morphism of closed
subspaces along it (IdealSheaf.homOfPullbackEq, an isomorphism by
isIso_homOfPullbackEq_of_diffeomorph) is the isomorphism of local resolutions
PieceEmbedding.localResolutionHomRestrictPiece E hV' hsub bed hbed W' hW'withisIso_localResolutionHomRestrictPiece.
Composed with localResolutionHomOfLe (LocalResolutionRestrict.lean) at
pieceAmbientImageOpens _ W' ≤ W this gives the transport of the local resolution along the open
inclusion of ambients, exists_localResolution_restrictPiece_iso (the second half of this
module).
Not in the sources beyond the remarks cited; bookkeeping.
The identification X|U' ≅ (X|U)|_V built from
imageOpens U V = U' (an eqToIso followed by the inverse of restrictOpen_restrictOpen_iso),
followed by the two open immersions, is the open immersion of U' — proved by subst, so that
the eqToIso is the identity and no equation proof is ever unfolded.
The associativity bookkeeping of the argument of
localResolutionToPiece_comp_localResolutionHomOfLe, in any category — two composites Y' → T
agree once each layer commutes
(e1/e1': the closed subspaces over the open inclusions, e2/e2': the maps of closed
subspaces over the blow-downs, e3: the lift, e4: the square of the ambient maps).
A morphism with a one-sided inverse is cancelled on the right.
The second half of that argument, in any category — the two composites into the closed
subspace Z agree after ι (h), so they agree (hι); the model isomorphisms emb, emb' are
moved across the chain hB1 (the model isomorphism of the restricted embedding over the inclusion
of the ambients) and cancelled.
The restricted embedding's triple is the pull-back of the piece's triple #
The triple (G', 𝓘', ∅) of the restricted embedding is the pull-back of the piece's triple
(G, 𝓘, ∅) along the ambient inclusion Sp(G') → Sp(G) ([Wlo09, §4, (3)⇒(4)]) — the ideal by
restrictPiece_ideal (rfl), the empty family by empty_comap.
The ambient inclusion restricted to W', a diffeomorphism onto its image #
The ambient inclusion restricted to W', onto the image open pieceAmbientImageOpens _ W'
(the smooth morphism along which the functor is pulled back, [Kol07, 34.1]).
Equations
Instances For
The restricted inclusion is a local analytic isomorphism
(AnalyticMap.isLocalDiffeomorph_restrictMap).
The restricted inclusion on points.
The restricted inclusion is bijective — injective as the inclusion is, onto its image open
(AnalyticMap.surjective_restrictMap).
The commutation with local isomorphisms at the restricted inclusion: the sequences #
The image of a relatively compact open is relatively compact
(AnalyticMap.isCompact_closure_image).
The embedded desingularization sequence of the restricted embedding over W' is the
pull-back along the restricted inclusion of the sequence of the piece over the image open, empty
blow-ups erased ([Wlo09, Theorem 6.0.6(2)] at an open embedding; [Kol07, 34.1]) — the
commutation CommutesWithLocalIsos of IsEmbeddedDesing (hbed.2 n) at the local analytic
isomorphism pieceAmbientIncl, the restricted embedding's triple being the pull-back of the
piece's (ambientTriple_restrictPiece_isPullbackOf).
The restricted ideal of the restricted embedding over W' is the pull-back, along the
restricted inclusion, of the piece's restricted ideal over the image open — both are 𝓘 pulled
back along W' → G (pullback_pullback).
The last-stage lift #
The last-stage lift of the restricted inclusion through localResolutionSeq_restrictPiece
(the lift of [Kol07, Definition 30.1] at the restricted inclusion): stageOfEq, then
eraseEmptyLast⁻¹, then pullbackLiftLast — an analytic map from the last stage of the restricted
embedding's sequence over W' to the last stage of the piece's sequence over the image open (the
pattern of liftOfLe, LocalResolutionRestrict.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lift, as a diffeomorphism — pullbackLiftLast of the bijective local isomorphism
restrictPieceIncl is a diffeomorphism (pullbackLiftLastDiffeomorphOfBijective), the two
transports are.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The diffeomorphism and the analytic map are the same function.
The final strict transforms correspond under the lift
(strictTransformSubspaceSeq_last_of_eq_pullback_eraseEmpty) — the final strict transform of
𝓘'|W' along the restricted embedding's sequence is the pull-back along liftRestrictPiece of
the final strict transform of 𝓘|_{g(W')} along the piece's sequence.
The same, along the diffeomorphism.
The lift lies over the restricted inclusion ([Kol07, Definition 30.1]) — the blow-down of
the lifted point is the inclusion of the blow-down
(stageMap_last_pullbackLiftLast, stageMap_last_eraseEmptyLast_symm,
stageMap_last_stageOfEq).
The isomorphism of local resolutions #
The local resolution of the restricted embedding over W' maps to the local resolution of
the piece over the image open ([Wlo09, §4, (3)⇒(4)]; [Wlo09, Theorem 6.0.6(2)]) — the morphism
of closed subspaces IdealSheaf.homOfPullbackEq along the lift, with
strictTransformSubspaceSeq_last_liftRestrictPieceDiffeo; typed as a morphism of K-spaces, so
that every composite with it is a K-composite.
Equations
- E.localResolutionHomRestrictPiece hV' hsub bed hbed W' hW' = Manifold.IdealSheaf.homOfPullbackEq ⇑(E.liftRestrictPieceDiffeo hV' hsub bed hbed W' hW') ⋯ ⋯
Instances For
It is an isomorphism of K-spaces — the morphism of closed subspaces along a diffeomorphism
(isIso_homOfPullbackEq_of_diffeomorph; the two categories share composition and identities
definitionally).
The restricted embedding lies over the inclusion, at the morphism level #
Sp(g) : Sp(G') → Sp(G), the morphism of ambient
spaces induced by the inclusion g of the shrunk ambient, typed at the abbreviations
restrictAmbientSpace/ambientSpace (the right-hand side of
restrictAmbientKIso_hom_comp_ofRestrict).
Equations
Instances For
openOf X V' ≤ openOf X V for V' ⊆ V.
The identification X|V' ≅ (X|V)|_W of
PieceRestrict.lean, followed by the open immersion (X|V)|_W → X|V, is the inclusion X|V' → X|V
(both are over X).
The model isomorphism of the restricted embedding lies over the inclusion of the ambients,
as morphisms — emb' ≫ ι' ≫ Sp(g)
is the inclusion X|V' → X|V followed by emb ≫ ι (the five-factor chain of
restrictPieceEmbIso, factor by factor; every junction is a syntactic Category.assoc, no
rewriting — the carriers mix Opens (pieceAmbient 𝕜 E.G) with Opens E.ambientSpace).
The compatibility square: the isomorphism of local resolutions lies over X #
The square of the ambient maps — incl_{g(W')} ∘ σ ∘ D = g ∘ incl_{W'} ∘ σ' as functions
from the last
stage of the restricted embedding's sequence to G (stageMap_last_liftRestrictPiece
pointwise).
The isomorphism of local resolutions lies over X — Φ ≫ (Ỹ(g W') → X) = (Ỹ'(W') → X);
the argument of localResolutionToPiece_comp_localResolutionHomOfLe in the two generic lemmas
layer_square_comp_eq (the layers) and over_square_comp_embInv_eq (the chain
restrictPiece_emb_comp_quotientι_comp_ambientInclHom moves emb' across,
Hom.ext_of_comp_quotientι cancels ι, embInv is prepended), instantiated
in the category of analytic 𝕜-spaces; the square of the ambient maps is
inclusion_comp_composite_comp_liftRestrictPieceDiffeo read as morphisms (ofManifoldHom_comp,
ofManifoldHom_congr).
The local resolution of the restricted embedding is the restriction of the local #
resolution
Transport of the local resolution along the open inclusion of ambients
([Wlo09, §4, (3)⇒(4)]; [Wlo09, Theorem 6.0.6(2)]; [Kol07, 34.1]) — the local resolution of the
restricted embedding E|V' over W' ⋐ G' is the part of the local resolution of E over
W ⊇ g(W') lying over the points of X with ambient point in g(W'), compatibly with the maps
to X. The isomorphism is Φ (localResolutionHomRestrictPiece, the sequences identified by the
commutation with local isomorphisms) followed by the open immersion Ỹ(g W') → Ỹ(W)
(localResolutionHomOfLe) read onto its range (isoOfRangeEq); the range is the part over the
base open by preimage_subset_range_localResolutionHomOfLe and the square
localResolutionToPiece_comp_localResolutionHomOfLe; the compatibility is
localResolutionHomRestrictPiece_comp_toSpaceMap.