The push-forward relation of the glued families along a closed embedding #
Kollár's commutation of a blow-up sequence functor with closed embeddings over the compact sets,
for the glued families: for family functors B in dimension n and B' in dimension n − s on
the standard models with B(M, I, ∅) = τ_* B'(S, I|_S, ∅) over every relatively compact open
(AnalyticFamilyFunctor.CommutesWithClosedEmbeddingsOfEmptyDivisorFam, [Kol07, 34.3]) and B'
commuting with local analytic isomorphisms, the succession of the glued family of B(M, I, ∅) over
the neighbourhood of a compact K ⊆ M is the push-forward along a closed embedding τ : N → M
with image S of the succession of the glued family of B'(N, τ^*I, ∅) over the neighbourhood of
a compact K' ⊆ N with τ(U_{K'}) ⊆ U_K, up to blow-ups whose centres lie outside the part over
τ(U_{K'}) (FiniteSuccession.IsPushforwardUpToEmptyAlong):
isPushforwardUpToEmptyAlong_toExtensionCompatibleFamily.
The argument: with L the value of B' on the trace U_S of U_K on the bundled submanifold S,
the value of B on U_K is the push-forward of L from the stage (U_K, S ∩ U_K, e)
(IsClosedSubmanifold.restrictStageOf), whose stages receive the inclusions
PushforwardStage.inclStage; the value of B' on U_{K'} is, through the identification
e : N ≃ S over τ, the pull-back of L up to empty blow-ups
(CompatibleFamily.isPullbackUpToEmptyAlong_seqOn), with lifts f_k bijective on the fibres
(bijOn_fiber_of_isPullbackUpToEmptyAlong_clauses). The embeddings of the relation are the
inclusions after the lifts; the fibre bijections make them embeddings with image the part of the
strict transform over τ(U_{K'}), and the centres of the push-forward are the images of the
centres of L.
For an empty N the two successions are empty (length_eq_zero_of_isEmpty,
eq_nil_of_isEmpty) and the relation holds for any model space of N
(isPushforwardUpToEmptyAlong_seqOn_of_isEmpty).
Successions over an empty manifold #
A finite succession over an empty manifold with no empty centre has length 0: every stage is
empty, so every centre is the unit ideal sheaf.
A list of centres on an empty manifold with no empty centre is the empty list.
The push-forward relation of the glued families #
The push-forward relation for an empty N: both successions are empty, and the relation
holds with the restriction of τ as the only embedding. The class Dom' is required only at the
pull-back of I to the bundled submanifold τ(N).
The push-forward relation for an empty N: both successions are empty, and the relation
holds with the restriction of τ as the only embedding
(isPushforwardUpToEmptyAlong_seqOn_of_isEmpty_of_dom, for a class Dom' containing every
triple with nonzero stalks and empty boundary).
The succession of the glued family of B(M, I, ∅) over U_K is the push-forward along the
closed embedding τ : N → M of the succession of the glued family of B'(N, τ^*I, ∅) over
U_{K'}, up to blow-ups whose centres lie outside the part over τ(U_{K'})
([Kol07, 34.3] over the compact sets), for τ(U_{K'}) ⊆ U_K, I ⊇ I_S with S = τ(N), and N
identified with the bundled S by e over τ. The value of B on U_K is the push-forward of
the value L of B' on the trace U_S from the stage (U_K, S ∩ U_K, e); the value of B' on
U_{K'} is the pull-back of L along e up to empty blow-ups; the embeddings are the stage
inclusions of the push-forward after the lifts of the pull-back, which are bijective on the fibres
over U_{K'}. The class Dom' is required at J and at the pull-back of I to the bundled
submanifold τ(N).
isPushforwardUpToEmptyAlong_toExtensionCompatibleFamily_of_dom for a class Dom'
containing every triple with nonzero stalks and empty boundary.