The boundary of an erased sequence embeds into the boundary of the sequence #
The empty blow-up convention [Kol07, 32] deletes the empty blow-ups, and the second clause of
functoriality for smooth morphisms [Kol07, 34.1] reindexes. Here the total transform appends one
member per blow-up, the member appended by an empty blow-up being the unit ideal
(exceptionalDivisor_top); so the boundary induced at the end of S.eraseEmpty has fewer
members than the inverse image, along eraseEmptyLastHom, of the boundary induced at the end of
S: it embeds order-preservingly into it, matching members, with the unit ideal at every index
outside the range, a deletion of ⊤ members (IsTopErasure), which is the relation behind
IndifferentToEmptyMembers (Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferent.lean),
and the embedding carries the transforms of the original members to the transforms of the original
members (originalIdx). The boundary is a divisor with ordered index set as in Kol07, Definition
31.
IsTopErasure E' E e:E'isEwith⊤members deleted along the order embeddinge; reflexive, transitive, preserved bycomapand by the total transform (sumLexMapEmb, the lift of an embedding to the lexicographic sums that index total transforms).exists_isTopErasure_totalTransformSeq: a deletion of⊤members of the starting family induces one between the families at the end of any sequence, compatible withoriginalIdx.EraseEmbeds S' E' R F φ e₀: the relation between the end data of two sequences along a morphism of last stages;eraseEmbeds_eraseEmpty : EraseEmbeds S.eraseEmpty E S E S.eraseEmptyLastHom idis the theorem, by induction onSwith the pull-back (EraseEmbeds.pullback, along the trivial blow-up'sinv (blowUpπ X ⊤)) and the extension of the target family by the empty exceptional member (EraseEmbeds.extend).monoEquivOfFin_totalTransformSeq_of_lt: the firstcard E.ιpositions of the induced family are the transforms of the original members, in order.exceptionalFamily_eraseEmpty_embeds: the exceptional sub-family of the erased sequence is the exceptional sub-family of the sequence with⊤members deleted.
Deletion of ⊤ members along an order embedding #
E' is E with ⊤ members deleted along the order embedding e: the members of E' are
the members of E at the indices in the range of e, and every index of E outside the range
carries the unit ideal [Kol07, 32].
Equations
Instances For
A deletion of unit members is an extension by empty members (ExtendsByEmpty): the same
data, the order embedding forgotten to an injection.
The lift of an order embedding to the lexicographic sums with a common right summand
(Sum.map e id), the index sets of total transforms (totalTransform, append).
Equations
- Hironaka.Sequence.sumLexMapEmb e = OrderEmbedding.ofMapLEIff (fun (x : α ⊕ₗ γ) => toLex (Sum.map (⇑e) id (ofLex x))) ⋯
Instances For
Deletion of ⊤ members is preserved by the total transform: the strict transform of the unit
ideal is the unit ideal (strictTransform_top_right), the exceptional members match.
A deletion of ⊤ members of the starting family induces one between the families at the end
of any sequence, carrying the transforms of the original members to the transforms of the
original members.
Casts along equalities of families, and originalIdx under pullback #
The order isomorphism of index sets induced by an equality of families.
Equations
- Hironaka.Sequence.castι h = h ▸ OrderIso.refl F₁.ι
Instances For
originalIdx commutes with pull-back: the transform of an original member along the
pulled-back sequence is the transform along the sequence (the index sets agree definitionally;
the heterogeneous equality carries the equality of the families).
The relation between the end data of two sequences #
The end data of S' (with family E') embed into the end data of R (with family F) along
φ and the map of original members e₀: an order embedding of the induced families matching the
members through the inverse image along φ, with the unit ideal at every index outside its range,
carrying the transforms of the original members of E' to those of F along e₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transport along an equality of source families.
Peeling one blow-up on both sides.
Peeling one blow-up on the target side only.
Extending the target family by a deletion of ⊤ members.
Pulling back the source sequence along a flat morphism.
The original members of E, embedded into the total transform of the trivial blow-up.
Equations
- Hironaka.Sequence.inlEmb E D = OrderEmbedding.ofMapLEIff (fun (a : (E.comap D.blowUpπ).ι) => toLex (Sum.inl a)) ⋯
Instances For
Under the trivial blow-up, the inverse image of E is its total transform with the (empty)
exceptional member deleted (strictTransform_top_left, exceptionalDivisor_top).
The trivial blow-up case of eraseEmbeds_eraseEmpty: the erased sequence is the erased tail
carried back along inv (D.blowUpπ) (EraseEmbeds.pullback), and the family of the sequence is
the inverse image of E extended by the empty exceptional member (EraseEmbeds.extend along
isTopErasure_inlEmb_of_eq_top).
The transport of the source family ((E.comap π).comap (inv π) = E); the equality is a
hypothesis, not a local have — with the proof term in scope the kernel check does not
terminate.
The nontrivial blow-up case of eraseEmbeds_eraseEmpty: peel the common first blow-up.
The boundary at the end of the erased sequence is the inverse image, along the last-stage
isomorphism, of the boundary at the end of the sequence with ⊤ members deleted, the transforms
of the original members carried to the transforms of the original members [Kol07, 32].
Positions of the original members; the exceptional sub-family #
The first card E.ι positions of the family induced at the end of a sequence are the
transforms of the original members, in the original order (monoEquivOfFin_lex_inl).
The exceptional sub-family of the erased sequence is the inverse image of the exceptional
sub-family of the sequence with ⊤ members deleted.