The exceptional family of a restricted push-forward, read on the carried slice #
Kollár pushes a blow-up sequence L_S of the slice S ∩ U forward to the padded sequence
L_P = pushforwardRestrict hS U L_S of U [Kol07, Definition 30.3]; the carried slice S_r of
the last stage, with the identification G : (L_S)_r ≃ S_r, is where the padded local resolution
is read (exists_closedSubmanifold_last_pushforwardRestrict, LocalResolutionPad.lean).
PushforwardBoundaryTrace.lean and exists_closedSubmanifold_last_pushforwardRestrict_boundary
(LocalResolutionPad.lean) add, under the normal-crossings clause (3′) of [Kol07, Definition 66]
for L_P: the last-stage exceptional family of L_P has simple normal crossings with S_r
properly, and an order isomorphism o of the stage sets with (j_r ∘ G)⁻¹(H^P_{o j}) = H^S_j —
the set-level statement that the padded run's exceptional divisors trace to the slice run's,
stage for stage. This module provides the ideal-level form for the gluing of the exceptional
families: the padded members restrict to the slice members as closed subspaces. Two theorems, of
which the first is what CoproductPadIdentity.lean uses, while the second packages it along the
order isomorphism o and has no other user:
IsClosedSubmanifold.pullback_idealSheaf_inclusionMap_comp_of_hasSncWithProper: the ideal sheaf of a member of a family having simple normal crossings withSproperly, pulled back alongincl_S ∘ Gfor a diffeomorphismGonto the bundledS, is the ideal sheaf of its preimage —pullback_idealSheaf_inclusionMap_of_hasSncWithProperalong the inclusion, then the pull-back alongGas a local diffeomorphism (comap_idealSheaf_of_isLocalDiffeomorph);BlowUpSequence.exists_orderIso_pullback_idealSheaf_pushFamily: with the boundary data ofexists_closedSubmanifold_last_pushforwardRestrict_boundaryas binders, an order isomorphisme := o.symmof the stage sets along which every padded member pulls back, as a reduced ideal sheaf, to the slice member — for any closed-submanifold witnesses of the members (the witnesses are proofs of propositions).
Sources: the counterpart, for the boundary, of the restriction Z_i ∩ S_i of
[Kol07, Definition 30.2], at the level of ideals, along the push-forward of
[Kol07, Definition 30.3]. The proofs are routine.
The ideal sheaf of a member of a family having simple normal crossings with S properly,
pulled back along incl_S ∘ G for a diffeomorphism G : X ≃ S, is the ideal sheaf of its
preimage (any closed-submanifold witness of that preimage; the counterpart, for the boundary, of
the restriction Z_i ∩ S_i of [Kol07, Definition 30.2], in the transverse case) — the
composite-map form of
pullback_idealSheaf_inclusionMap_of_hasSncWithProper: that theorem along the inclusion, then the
pull-back along G as a local diffeomorphism (comap_idealSheaf_of_isLocalDiffeomorph) and the
preimage read through G.
The padded run's last-stage exceptional members pull back along the carried-slice
identification incl_{S_r} ∘ G to the slice run's, as reduced ideal sheaves, through an order
isomorphism of the stage sets ([Kol07, Definitions 30.2–30.3]). The binders hprop (the proper
simple normal crossings) and o/ho (the trace identity) are the fourth conjunct of
exists_closedSubmanifold_last_pushforwardRestrict_boundary and determine G; hsncP is clause
(1) of IsEmbeddedDesing (the exceptional divisors have simple normal crossings) for the padded
run at its last stage; hclP/hclS are any witnesses of the members (proofs of propositions).
Then e := o.symm and, per member,
pullback_idealSheaf_inclusionMap_comp_of_hasSncWithProper at the set identity ho.