The monomial phase is indifferent to empty boundary members #
The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the monomial
phase at the mark 1: deleting empty members of the boundary does not change the phase. Two triples
on the same manifold with the same ideal sheaf whose boundary families differ by an empty extension
along an order embedding e (HypersurfaceFamily.IsEmptyExtension: the members correspond along
e, the members outside its range are empty) have the same phase at every fuel
(step2bPhase_eq_of_isEmptyExtension): an empty member has an empty positive locus, so it is never
active; the active members correspond along e; the top members correspond (the maximum in a linear
order along an order embedding); the centres are the same set; and after one step the two total
transforms differ again by an empty extension, along e ⊕ₗ id (sumLexEmb; the strict transform of
an empty member is empty, strictTransformSet_empty).
The order embedding e ⊕ₗ id #
The order embedding α ⊕ₗ PUnit ↪o β ⊕ₗ PUnit induced by e : α ↪o β on the first summand.
Equations
- Hironaka.Manifold.sumLexEmb e = OrderEmbedding.ofMapLEIff (fun (s : α ⊕ₗ PUnit.{?u.1 + 1}) => toLex (Sum.map (⇑e) id (ofLex s))) ⋯
Instances For
The top member corresponds along the order embedding.
The Step 2b centres coincide.
After one step the two total transforms differ again by an empty extension, along e ⊕ₗ id
(the strict transform of an empty member is empty).
The phase is indifferent to empty members #
The phase does not see empty boundary members (the counterpart, for boundary members, of
[Kol07, 32]): two triples on the same manifold
with the same ideal sheaf whose boundaries differ by an empty extension have the same phase at
every fuel. Induction on the fuel: the centres coincide (step2bCenter_of_isEmptyExtension), and
the steps differ again by an empty extension (isEmptyExtension_stepTripleOf), compared on the
same blow-up through the step at the witness of the first triple (stepTripleOf,
heq_stepTripleOf).