The glued exceptional family of a chain of gluings #
The resolution of a whole analytic space is glued from the resolutions of the members of an
exhaustion by relatively compact open subsets, along their overlaps ([Kol07, Proposition 37];
[Kol07, 44]; [Wlo09, §4.3]); the exceptional divisors of the levels glue with them once their
components are matched level to level by a label, the stage of the common blow-up sequence at which
each is created [Kol07, Proposition 37, (37.2)]. For a gluing datum G : GlueOver X R π dom over a
chain (ι := ULift ℕ, dom monotone), with a simple-normal-crossings family H n on every level
and label maps e n on the members with non-empty trace on the overlap with the next level,
satisfying the labelled identity on the overlaps (hpair, the conclusion of the locality lemma
ClosedSubspace.comap_eq_of_forall_exists_local) and covering every member of the next level that
meets the overlap (hsurj: a component of a higher level meeting a lower level restricts to a
component of that level), the members glue to a simple-normal-crossings family on the glued space
(chainGlueFamily, isSncFamily_chainGlueFamily), locally finite
(locallyFinite_chainGlueFamily), indexed by the colimit of the levels' members along the label
maps (chainColimitIndex), with each level's members as the pull-backs
(comap_ιGlued_chainGlueFamily_mk) and support the preimage of the levels' common support
(iUnion_support_chainGlueFamily).
Three general tools carry it.
- The colimit index is a tree of chains: the step relation
⟨n, σ⟩ ↦ ⟨n+1, f n σ⟩is functional and raises the level, so its generated equivalence is "a common descendant" and two members of one level are identified only when equal (chainColimitIndex.mk_injective,mk_eq_mk_succ_iff). - Compatibility of closed subspaces of the levels (
CompatClosedSubspacesofHironaka.AnalyticSpace.Glue.OverFamily, asked for every pair byglueClosedSubspace) follows on a chain from the adjacent pairs (compatClosedSubspaces_of_chain): compatibility of a pair is the agreement of the transported stalk idealspieceStalkIdealat the common glued points, in both directions (pieceStalkIdeal_eq_of_pair,compat_pair_of_forall_pieceStalkIdeal_eq), and on a chain the images of the levels are nested, so agreement propagates by induction, with no cocycle bookkeeping. - The locality and partner tools of
Hironaka.Resolution.Analytic.Kol07Thm45.Glue.OverFamilyPartner, restated in therestrictOpenspelling of the traces (ClosedSubspace.comap_eq_of_forall_exists_local,existsUnique_comap_eq_of_forall_exists_local,IsSncFamily.eq_of_comap_ofRestrict_eq_of_nonempty), the spelling in which the transitionsG.tare stated.
The labelled compatibility (chainLabelledCompat) has four cases per label and adjacent pair: both
levels represented (the identity hpair, the representatives related by mk_eq_mk_succ_iff); the
lower level only (the trace on the overlap is empty, both sides are the unit ideal sheaf); the upper
only (by hsurj its trace on the overlap is empty, so again both sides are the unit ideal sheaf);
neither.
The glued chain family is the exceptional family of the resolution glued along an exhaustion
(Hironaka.Resolution.Analytic.Kol07Thm45.ResolutionSncGlobal); the clause that the exceptional
locus is a divisor with simple normal crossings ([Kol07, Theorem 45, (3)]; Wlo09, Theorem 2.0.1,
(2)) follows.
The colimit index of a chain of partial maps f n : {σ // p n σ} → Λ (n+1): the quotient of
Σ n, Λ n by the generated equivalence ⟨n, σ⟩ ~ ⟨n+1, f n ⟨σ, h⟩⟩.
Equations
Instances For
A descendant at the same level is the point itself.
Descendants of one point are linearly ordered: the step relation is functional.
Two ancestors of one point at the same level coincide when every f n is injective.
Descent is contained in the generated equivalence.
The generated equivalence of the (functional) step relation is "a common descendant".
Two members of one level are identified only when equal (each f n injective): the colimit
index is a tree of chains, no two members of one level identified.
A level-n member and a level-(n+1) member share a class iff the second is the first's image.
The pull-back of the unit ideal sheaf is the unit ideal sheaf.
An ideal sheaf with empty cosupport is the unit ideal sheaf.
A point of the cosupport of a trace on an open subspace lies in the cosupport of the member
(QuotientSpace.cosupport_comap; the restrictInclusion form is
mem_support_of_comap_restrictInclusion of
Hironaka.Resolution.Analytic.Kol07Thm45.Glue.OverFamilyPartner).
Two closed subspaces with the same trace on an open subspace have the same stalk ideal at every
point of the open subset (KLocallyRingedSpace.isIso_ofRestrict_stalkMap; the restrictInclusion
form is
stalkIdeal_eq_of_comap_restrictInclusion_eq of
Hironaka.Resolution.Analytic.Kol07Thm45.Glue.OverFamilyPartner).
Two members of a simple-normal-crossings family with the same trace on an open subset, the trace
non-empty, are the same member (IsSncFamily.eq_of_comap_restrictInclusion_eq_of_nonempty in the
restrictOpen spelling).
A labelled identity between two families along a morphism holds as soon as it holds on an open
neighbourhood of every point: equality of closed subspaces is stalkwise
(comap_restrict_eq_of_forall_exists_local in the restrictOpen spelling; Kol07, Proposition 37,
(37.2)).
Along an isomorphism, a member with non-empty support has a unique partner in a
simple-normal-crossings family whose pull-back is the member, once one is given locally (uniqueness
by the rigidity of the pulled-back family; existsUnique_partner_of_forall_exists_local_label in
the restrictOpen spelling).
The converse of comap_eq_of_stalk_square: in the square α ≫ a = σ' ≫ β ≫ b with α, β
surjective and σ, σ' inverse, ideals identified under σ after pulling back have the same
image.
Representative independence for one pair from that pair's compatibility (pieceStalkIdeal_eq,
pairwise).
Compatibility of one pair from representative independence at every point of its gluing open
subset (the converse of pieceStalkIdeal_eq_of_pair).
Representative independence is symmetric in the two representatives
(stalkSpecializes_comp_eq_id).
The base open subsets of a chain are monotone.
On a chain, a lower level lies entirely over the base open subset of every higher level: its gluing open subset with a higher level is everything.
A point of level n as a point of the gluing open subset with level m ≥ n.
Instances For
The point-level glue identity along the chain: a point of level n and its image in level
m ≥ n under the transition have the same image in the glued space (ofRestrict_comp_ιGlued).
Representative independence along the chain, by induction on the higher level from the adjacent
pairs (pieceStalkIdeal_eq_of_pair) through the nested images.
Representative independence for every pair of levels of a chain (both orders, by symmetry).
On a chain, compatibility of closed subspaces of the levels follows from compatibility of the adjacent pairs, in one direction: the transported stalk ideals agree at every glued point by induction along the nested images of the levels; no cocycle bookkeeping.
The members of level n with non-empty trace on the overlap with level n+1.
Equations
- AnalyticSpace.GlueOver.chainTraceNonempty π dom H n σ = (AnalyticSpace.GlueOver.restrictGlue π dom { down := n } { down := n + 1 } (H n σ)).support.Nonempty
Instances For
The index of the glued chain family: the colimit of the levels' members along the label maps on the non-empty traced members.
Equations
- AnalyticSpace.GlueOver.ChainIndex π dom H e = Hironaka.chainColimitIndex Λ (AnalyticSpace.GlueOver.chainTraceNonempty π dom H) e
Instances For
The label maps are injective: rigidity of the members of a simple-normal-crossings family on the
non-empty traces (IsSncFamily.eq_of_comap_ofRestrict_eq_of_nonempty).
The labels are injective on every level (chainColimitIndex.mk_injective).
Labelled compatibility of a chain of simple-normal-crossings families: the levels' members
labelled by their classes in the colimit index are compatible closed subspaces, given the adjacent
identities on the non-empty traced members (hpair) and that every level-(n+1) member meeting the
overlap is a partner (hsurj): four cases per label and adjacent pair (both levels represented; the
lower only, its trace empty by the definition of the label maps' domain; the upper only, its trace
empty by hsurj, so both sides are again the unit ideal sheaf; neither), then the chain lemma
compatClosedSubspaces_of_chain.
The glued chain family on the glued space, indexed by the colimit of the levels' members
(glueFamily on the labelled data; [Kol07, Theorem 45, (3)]; [Wlo09, §4.3]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The glued member of the class of ⟨n, σ⟩ pulls back to level n as H n σ.
The glued chain family is a simple-normal-crossings family (isSncFamily_glueFamily).
The glued chain family is locally finite (locallyFinite_glueFamily: each level's family is
locally finite).
The support of the glued chain family is the preimage of S under the descended map when every
level's family has support the preimage of S under its map (toFun_descMap_ιGlued,
exists_ιGlued_eq).