CP3 along Step 3 at the mark 1 #
Step 3 of the proof of [Kol07, Theorem 107] (item 111, Step 3) reduces the order of the monomial
part M(I) = 𝒪(−∑ a_j E^j); here it is run at the mark 1. Each centre of the geometric Step 3
(PieceFamily.realize, Hironaka.Resolution.Algebraic.Monomial.Geometric.Pieces) is, at each of
its points q, the face of the stage family through q selected by the rule of Step 3 — an
intersection of members of total exponent ≥ 1 (realizeAux_center, exists_center_realize_eq,
realize_invariant, stalkIdeal_centerOf_eq_faceIdeal, m_le_total_of_mem_choice). For the
statement CP3 of the embedded desingularization
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): in any chain coordinates (z, c, σ, a, b) at q ([Kol07, Definition 24]) the stalk of the face is (z_s) with s a set of
coordinates of members (exists_stalkIdeal_faceIdeal_eq_span, stalkIdeal_vanishingIdeal_piece: a
piece through q is its member near q, whose coordinate is z_{c j}), which is the stratum of
level 0. Its admissibility condition (★) — some z_k, k ∈ s, carries b_k ≠ 0 — is read at the
piece c₀ of positive exponent: the stage monomial has order a_{c₀} at the generic point η₀ of
c₀ (ord_monomial_eq_total, faceAt_eq_singleton_of_mem_genericPoints); the marked transform of
the current ideal lies below the stage monomial (markedTransformSeq_mono,
markedTransformSeq_realize), so it has order ≥ a_{c₀} ≥ 1 there, and finite order
(ord_ne_top_of_isNonzeroEverywhere); and the exponent b_{c j} of either chain shape at the
coordinate of a member is the order of the current ideal at that member's generic point — the fine
split I = M(I) · N(I) of [Kol07, Definition–Lemma 110] read exponent by exponent
(toNat_ord_eq_of_stalkIdeal_eq_span_mul, from stalkIdeal_monomialPart_eq_span_prod and the
uniqueness eq_of_span_prod_pow_mul_eq of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Split,
with the chain part stalkIdeal_nonmonomialPart_of_kShape or
stalkIdeal_nonmonomialPart_of_iShape). The same stratum serves both shapes, so the I-shape clause
is the first alternative.
The general form cp3For_realize_of_le is stated for any piece family realizing the boundary and
any nonzero ideal below the marked monomial ideal; cp3For_step3Seq is its instance through the
bridge monomial_exponentAt_step3Family
(Hironaka.Resolution.Algebraic.MarkedOrderReduction.Step3Input) and I ⊆ M(I). This argument is
not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1.
The fine split of [Kol07, Definition–Lemma 110] read exponent by exponent: the exponent of a
chain shape at the coordinate of a member is the order of the ideal at the generic point of that
member through the point — M(K)_p is the monomial in the coordinates of the members with the
orders as exponents, N(K)_p is the chain part, and the monomial factor is unique.
CP3 along the geometric Step 3 of a piece family ([Kol07, 111, Step 3]), for any nonzero
ideal below the marked monomial ideal (the general form; cp3For_step3Seq is its instance): each
centre is, at each of its points, the face of the stage family through the point, of total
exponent ≥ 1; in any chain coordinates the face is (z_s) with s the coordinates of members,
and the exponent of the current ideal along a member through the point is b at that member —
the condition (★) at level 0; the same stratum serves the I-shape.
CP3 along Step 3 ([Kol07, 111, Step 3] at the mark 1): each centre is, at each of its
points, the face of the stage family through the point (centerOf), of total exponent ≥ 1; in
any chain coordinates a face is (z_s) with s the coordinates of members, and the exponent of
the current ideal along a member through the point is b at that member — the condition (★) at
level 0. An I-shape at a centre of Step 3 is classified by the same stratum. From the general
form through the bridge monomial_exponentAt_step3Family and I ⊆ M(I).