The boundary family along the deletion of empty blow-ups #
The boundary family totalTransformSeqFrom F at the last stage of a list has one exceptional
member per step (HypersurfaceFamily.totalTransform appends a PUnit summand to the index set at
each step). After the deletion of the empty blow-ups ([Kol07, 34.1]) the cleaned list has fewer
members, one per deleted step, so the two boundary families are not equal: the cleaned list's
boundary family embeds order-preservingly into the list's boundary family pulled back along
eraseEmptyLast⁻¹, matching the members, with the members outside the range (the exceptional
divisors of the deleted steps, π⁻¹(∅) = ∅, and their empty strict transforms) empty, and the
original members matched along originalIdx (BlowUpSequence.eraseEmptyIdx, hyp_eraseEmptyIdx,
hyp_eq_empty_of_notMem_range_eraseEmptyIdx, eraseEmptyIdx_originalIdx). These are exactly the
hypotheses of IndifferentToEmptyMembers on the erased induced triple against the exact
pull-back (the values agree by the convention of [Kol07, 32]).
The proof is a recursion on the list with the two families generalised along an order embedding
that is an empty extension (HypersurfaceFamily.IsEmptyExtension: members matched, empty
outside the range): a kept step extends the embedding by the new exceptional divisor
(isEmptyExtension_totalTransform), a deleted step drops one
(isEmptyExtension_totalTransform_of_eq_empty: along the empty blowing-up the strict transforms
of closed members are their preimages and the exceptional divisor is empty), and the transport of
the cleaned tail along Bl_∅ M ≃ M is the transport of its boundary family along map
(totalTransformSeqFrom_last_map). The identifications of index types along the propositional
equalities of families (the cons computation rule cons_totalTransformSeqFromAux_succ, the map
transport) are carried as heterogeneous equalities of originalIdx (heq_originalIdx_cons_last,
heq_originalIdx_last_map).
Closedness of the members (hF : ∀ j, IsClosed (F.hyp j)) is needed: along an empty blowing-up
the strict transform of a non-closed set is the preimage of its closure. The lexicographic-sum
order embedding is the generic Hironaka.Sequence.sumLexMapEmb.
The cons computation rule of the boundary family and of originalIdx #
The boundary family from F along cons hY rest at stage k + 1 is the family along rest
from the total transform of F under the first blowing-up (the constructor form of
totalTransformSeqFrom_succ).
The boundary family at the last stage of cons hY rest.
originalIdx is compatible with an equality of families (heterogeneously).
The index of an original member at the last stage of cons hY rest is its index, as a member
of the total transform of F, at the last stage of rest (heterogeneously, across the cons
computation rule of the boundary family).
Empty extensions of hypersurface families #
The relation between two hypersurface families on the same space that
IndifferentToEmptyMembers (Hironaka.Resolution.Analytic.Functor.Family) asks for: G embeds
order-preservingly into G' along e₀, the members are matched along e₀, and the members of
G' outside the range of e₀ are empty.
Equations
Instances For
The order embedding α ↪o α ⊕ₗ PUnit of the original members.
Equations
- Manifold.HypersurfaceFamily.inlLexEmb α = OrderEmbedding.ofMapLEIff (fun (a : α) => toLex (Sum.inl a)) ⋯
Instances For
Every member of a total transform of a family is closed when the centre is: the strict transforms are closures, the exceptional divisor a preimage of a closed set.
An empty extension is propagated through the total transform under a blowing-up: the strict transforms of matched members are matched, the new exceptional divisors are matched, the strict transform of an empty member is empty.
Along a blowing-up with EMPTY centre, an empty extension G ↪ G' is propagated to
π⁻¹(G) ↪ G'.totalTransform π ∅ through the original members: the strict transforms of the closed
members are their preimages, the (empty) exceptional divisor is outside the range.
The boundary correspondence #
The correspondence between a family GA on A and a family GB on B along
T : A ≃ B, with the original members oA, oB (indexed by ι₀): an order embedding
GB.ι ↪o GA.ι matching the members through T⁻¹, with the members of GA outside its range empty
and the original members matched.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transport of the correspondence along an equality of lists (the cast stageOfEq).
The boundary family at the last stage of the transported list Z.map φ is the pull-back along
(mapLast φ)⁻¹ of the boundary family from φ⁻¹(F) at the last stage of Z
(totalTransform_comap_of_square at each step).
The index of an original member at the last stage of the transported list is its index for the
pulled-back family at the last stage of the list (heterogeneously, across
totalTransformSeqFrom_last_map).
[Kol07, 32] and 34.1, the recursion: for an empty extension
e₀ : G ↪ G' of families with closed members, the boundary family from G at the last stage of the
cleaned list corresponds along eraseEmptyLast to the boundary family from G' at the last stage
of the list, the original members matched along e₀.
The boundary tool #
The correspondence for the same family on both sides.
[Kol07, 32] and 34.1: the order embedding of the boundary family
at the last stage of the cleaned list into the boundary family at the last stage of the list
(the e of IndifferentToEmptyMembers), for a family F with closed members.
Equations
- L.eraseEmptyIdx F hF = Classical.choose ⋯
Instances For
The members are matched through eraseEmptyLast⁻¹: the member eraseEmptyIdx i of the list's
boundary family pulled back to the cleaned list's last stage is the member i of the cleaned
list's boundary family (the first hypothesis of IndifferentToEmptyMembers, in the comap form
of AnalyticTriple.pullback).
The members of the list's boundary family outside the range of eraseEmptyIdx — the exceptional
divisors of the deleted steps and their strict transforms — are empty (the second
hypothesis of IndifferentToEmptyMembers).
hyp_eq_empty_of_notMem_range_eraseEmptyIdx for the pulled-back family.
The original members are matched: eraseEmptyIdx sends the index of the transform of the
original member j in the cleaned list's boundary family to its index in the list's boundary
family.