The transitions of the gluing datum: the local data #
Włodarczyk glues the canonical desingularizations Ṽ_i of the local embeddings along the
isomorphisms over the overlaps Ṽ_i ∩ Ṽ_j [Wlo09, §4, (3)⇒(4)]; Kollár glues the local
resolutions of the affine pieces by a formal property of blow-up sequence functors
[Kol07, Theorem 36, proof]. Here the transition between two pieces of the gluing datum is
assembled LOCAL-TO-GLOBAL from the independence of the local resolution from the embedding
(LocalResolutionIndependentOn: the local resolutions of two embeddings of the same piece are
isomorphic over the piece by a unique isomorphism), applied to the two embeddings RESTRICTED
(PieceRestrict.lean) to small opens of the overlap, transported (PieceRestrictResolution.lean)
and glued. This module holds the topological data of one point of the overlap:
exists_nested_opens_of_isOpen: two nested relatively compact opensz ∈ N,closure N ⊆ N',closure N' ⊆ O'(Mathlib'sexists_open_between_and_isCompact_closure, the space being locally compact Hausdorff);PieceEmbedding.exists_restrictAmbientOpens: for the embedding restricted toN', a relatively compact ambient openW' ⋐ G'_{N'}whose image lies in the piece's ambient openWand which contains the compact ambient image ofclosure N(exists_opens_isCompact_closure_supersetinsideG'_{N'} ⊓ g⁻¹(W));PieceEmbedding.mem_embPreimage_restrictPiece_iff_mem_domOpensanddomOpens_pieceAmbientImageOpens_subset: the points of the restricted embedding overW'are the points ofXin the base opendomOpens (g W'), and that base open lies insideN'(the shrunk ambient sees no point outsideN');LocalEmbeddingData.exists_transitionData: the package for two piecesi,jand a pointzof an openO'of their common base open;exists_transition_over_pairandLocalEmbeddingData.exists_transition_over: the local transition over the cover memberP_z, unique among the isomorphisms overX.
Not in the sources beyond the gluing remarks; bookkeeping.
The compatibility over the base of a morphism obtained by transporting a morphism ψ over the
base along four identifications, in any category — the transport's associativity bookkeeping.
A morphism whose transport is ψ is the transport of ψ back — the four identifications
being inverse pairs.
The inverse of an identification over the base is over the base.
A morphism over the base, transported BACK along the four identifications, is over the base — the uniqueness step's bookkeeping.
A morphism over a piece B of the base (through the open immersion o of the part over S)
is over the base — the compatibility of the independence's ψ read after the open immersion
p : B → Z.
The open subspaces of two opens with the same underlying set are isomorphic — isoOfRangeEq
of the two open immersions (no eqToIso).
Equations
Instances For
Its hom lies over X.
Its inv lies over X.
The two nested relatively compact opens #
Around a point z of an open O', two nested opens with compact closures, z ∈ N,
closure N ⊆ N', closure N' ⊆ O' (Mathlib's exists_open_between_and_isCompact_closure twice,
the analytic space being locally compact Hausdorff).
The base opens and the restricted embedding #
The base open of the piece over any ambient open lies in the piece (an open V).
The base open of the piece over the image of an ambient open of the SHRUNK ambient G'_{V'}
lies in V' — the shrunk ambient sees no point of the piece outside V'
(pieceCoord_ambientPoint_mem_restrictAmbient_iff).
A point of the restricted piece X|V' lies over the ambient open W' of the shrunk ambient
iff, as a point of X, it lies in the base open of the piece over the image g(W')
(embPreimage_restrictPiece).
The ambient open of the restricted embedding around a compact #
For a compact closure N ⊆ V' whose points of the piece lie over W, a relatively compact
ambient open W' of the SHRUNK ambient whose image lies in W and over which every point of
closure N lies (Włodarczyk's V̄_i ⊂ W_i at the restricted embedding, [Wlo09, §4, (3)⇒(4)];
exists_opens_isCompact_closure_superset inside G'_{V'} ⊓ g⁻¹(W)). The compact is the ambient
image of closure N pulled into X|V' (Subtype.isCompact_iff, the closed embedding
ambientPoint).
The transport: the local resolution of the restricted embedding as an open part #
The local resolution of the restricted embedding over W' maps by an OPEN IMMERSION over X
onto the part of the piece's local resolution over W lying over the base open domOpens (g W')
(exists_localResolution_restrictPiece_iso read as an open immersion).
For an open P of X inside the base open domOpens (g W'), the parts over P of the local
resolution of the restricted embedding and of the piece's local resolution are isomorphic over X
(the mechanism of exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion read with
isoOfRangeEq).
The pair forms: two embeddings of two pieces, the dimensions free #
A point of the piece over the base open lies over the ambient open.
The local data of the transition at a point, in the PAIR form (two embeddings
E : PieceEmbedding 𝕜 n X V, E' : PieceEmbedding 𝕜 m X V' of two pieces, the dimensions free;
[Wlo09, §4, (3)⇒(4)]) — for z in an open O' of the common base open of the two pieces: an open
N' ⊆ V ∩ V' with compact closure in O', and for each of the two embeddings restricted to N' a
relatively compact ambient open of the shrunk ambient whose image lies in the piece's ambient open
and whose base open contains z. The intersection of the two base opens is the member P_z of the
cover of O' on which the independence of the local resolution is applied.
The local transition over P_z for a pair of embeddings: existence, compatibility, #
uniqueness (the independence transported)
The local transition over the cover member P = domOpens_E (g W₁) ⊓ domOpens_E' (g W₂),
in the PAIR form (LocalEmbeddingData.exists_transition_over is its instance;
[Wlo09, §4, (3)⇒(4)]; [Kol07, Theorem 36, proof]) — an isomorphism over X between the parts of
the two local resolutions over P, UNIQUE among such: it is the isomorphism of the independence
hind for the two embeddings restricted to N' at the ambient opens (W₁, W₂), transported along
the identifications of exists_iso_restrictOpen_comap and the equality of sets Π'⁻¹ S = π'⁻¹ P
(restrictOpenIsoOfSetEq); any isomorphism over X on the parts over P transports back to one
of that kind on exactly S, so the uniqueness in hind applies verbatim.
The local data of the transition at a point ([Wlo09, §4, (3)⇒(4)]) — for z in an open
O' of the common base open of the pieces i, j: an open N' ⊆ piece i ∩ piece j with compact
closure in O', and for each of the two embeddings restricted to N' a relatively compact ambient
open of the shrunk ambient whose image lies in the piece's ambient open and whose base open
contains z. The intersection of the two base opens is the member P_z of the cover of O' on
which the independence of the local resolution is applied.
The local transition over P_z: existence, compatibility, uniqueness #
The local transition over the cover member P = domOpens_i (g W'i) ⊓ domOpens_j (g W'j)
([Wlo09, §4, (3)⇒(4)]; [Kol07, Theorem 36, proof]) — an isomorphism over X between the parts of
the two pieces' local resolutions over P, UNIQUE among such: it is the isomorphism of the
independence hind for the two embeddings restricted to N' at the ambient opens (W'i, W'j),
transported along the identifications of exists_iso_restrictOpen_comap and the equality of sets
Π'⁻¹ S = π'⁻¹ P (restrictOpenIsoOfSetEq); any isomorphism over X on the parts over P
transports back to one of that kind on exactly S, so the uniqueness in hind applies
verbatim.