The exceptional divisor of a compatible family, glued along the exhaustion #
Włodarczyk's divisor E on M̃ [Wlo09, Theorem 2.0.2] is the union of the exceptional divisors
of the successions over the members of the exhaustion, which agree on the overlaps up to the empty
blow-ups. For a compatible family C (CompatibleFamily), the last-stage exceptional families
exceptionalOn U of its values on the members U_m of a compact exhaustion form a chain along the
end-result embeddings (exceptionalChain: the transition of the members along
endResultEmbedding, exists_orderEmb_exceptionalOn_endResultEmbedding, is the one of
exists_orderEmb_totalTransformSeqFrom_last_pullback_eraseEmpty read through the compatibility
compat), and they glue to a hypersurface family on the glued space M̃ = endResultLimit
(gluedExceptional, by FamilyChain.glue): a simple normal crossings family when the pieces are
(isSnc_gluedExceptional), whose trace on every piece is the piece's family
(preimage_toLimit_support_gluedExceptional). Its reduced ideal sheaf pulls back along the
inclusion of every piece to the piece's last exceptional divisor
(idealSheaf_gluedExceptional_pullback_toLimitMap), by the general transport of the reduced ideal
sheaf of a simple normal crossings family along a local analytic isomorphism
(HypersurfaceFamily.idealSheaf_pullback_eq_idealSheaf_of_preimage_support).
Not in the sources beyond the statement cited; bookkeeping.
The reduced ideal sheaf of an snc family along a local analytic isomorphism #
The reduced ideal sheaf of a simple normal crossings family G, pulled back along a local
analytic isomorphism g, is the reduced ideal sheaf of any simple normal crossings family H
whose support is g⁻¹(|G|): the vanishing ideals of a set transport along the bijective germ
maps of g (comap_germMap_vanishingStalk).
The transition of the exceptional families along the end-result embeddings #
The last-stage exceptional family of the value of C on the relatively compact open U.
Equations
- C.exceptionalOn U hU = (C.seqOn U hU).toSuccession.totalTransformSeq (Fin.last (C.seqOn U hU).toSuccession.length)
Instances For
The transition of the exceptional families along an end-result embedding: for
U₁ ≤ U₂, an order embedding of the index set of the family over U₁ into that over U₂ such
that the trace of a matched member is the member and an unmatched member has empty trace
(exists_orderEmb_totalTransformSeqFrom_last_pullback_eraseEmpty, transported through the
compatibility compat and empty_comap).
The glued exceptional family #
The end-result embeddings are analytic open embeddings (the hypothesis hemb of the gluing,
isAnalyticOpenEmbedding_endResultEmbedding).
Equations
- ⋯ = ⋯
Instances For
The chain of the exceptional families along the exhaustion (FamilyChain on the chain of
end results endResultChain), with the transitions of
exists_orderEmb_exceptionalOn_endResultEmbedding.
Equations
- C.exceptionalChain Kex = { H := fun (m : ℕ) => C.exceptionalOn (Manifold.relCompactOpen Kex m) ⋯, ε := fun (m : ℕ) => ⋯.choose, preimage_hyp_ε := ⋯, preimage_hyp_eq_empty := ⋯ }
Instances For
Włodarczyk's exceptional divisor on M̃, as a hypersurface family: the exceptional
families of the pieces glued along the exhaustion.
Equations
- C.gluedExceptional Kex = (C.exceptionalChain Kex).glue
Instances For
The glued exceptional family has simple normal crossings when the exceptional families of the pieces do.
The trace of the glued exceptional family on a piece is the piece's exceptional family.
The reduced ideal sheaf of the glued exceptional family pulls back along the inclusion of a piece to the reduced ideal sheaf of the piece's exceptional family.