Functoriality of the monomial run under restriction: worked examples

Examples, decided by decide through the fuelled copies of the algorithm, of the restriction and refinement properties of the monomial order-reduction run step3 on the combinatorial state MonomialState (Hironaka/Resolution/Algebraic/Monomial/Restrict/RefinePhase.lean):

• the split example (splitX, splitU of HironakaExamples/Monomial/Examples.lean): the run on the U-nerve {0}, {2}, {0, 2} is the run on the X-nerve with the empty faces deleted; here every center meets U, so restrictRun keeps both centers and the renumbering is the identity;
• a subnerve pair in which the run on N blows up a center disjoint from L first (the component 0 of exponent 5 ≥ m = 4, absent from L) and then the double point {1, 2} common to both (exponents 2 + 2 = 4 ≥ m): restrictRun drops the first center, the direct run on L has the single center {1, 2}, and the exceptional component is numbered 3 in the direct run but 4 in the pulled-back run (the empty blow-up allocated the dead component 3): the order-preserving correspondence 3 ↦ 4 of step3_restrict;
• a refinement pair: Y = X ⊔ X, two copies of the two-component state L (ρ the fold), refines L; the run on Y blows up both copies of each center of L at once (one center of Y with twice the faces): it is the preimage run refineRun of the run on L, with ρ extended by 4, 5 ↦ 2 and 6, 7 ↦ 3.

theorem Hironaka.Monomial.Examples.splitX_centers : splitX.step3.2 = [{{0}}, {{2}}]

The centers of the split example on X.

theorem Hironaka.Monomial.Examples.splitU_centers : splitU.step3.2 = [{{0}}, {{2}}]

The centers of the split example on U.

def Hironaka.Monomial.Examples.bigN : MonomialState

N: components 0, 1, 2 (labels 0, 1, 2), exponents 5, 2, 2, m = 4, nerve {0}, {1}, {2}, {1, 2}.

Equations

• One or more equations did not get rendered due to their size.

def Hironaka.Monomial.Examples.subL : MonomialState

L: the subnerve without the component 0.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Monomial.Examples.bigN_centers : bigN.step3.2 = [{{0}}, {{1, 2}}]

The run on N: phase 1 blows up {0}, phase 2 blows up {1, 2}.

theorem Hironaka.Monomial.Examples.subL_centers : subL.step3.2 = [{{1, 2}}]

The run on L: only {1, 2}.

A refinement pair

def Hironaka.Monomial.Examples.baseL : MonomialState

L: two components 0, 1 (labels 0, 1) meeting at a point, exponents 1, m = 1.

Equations

• Hironaka.Monomial.Examples.baseL = Hironaka.Monomial.MonomialState.ofValid 2 1 2 2 (fun (c : ℕ) => c) (fun (x : ℕ) => 1) {{0}, {1}, {0, 1}} Hironaka.Monomial.Examples.baseL._proof_1

def Hironaka.Monomial.Examples.doubleY : MonomialState

Y = X ⊔ X: two copies 0, 1 and 2, 3 of the components of L, with their labels.

Equations

• One or more equations did not get rendered due to their size.

def Hironaka.Monomial.Examples.fold : ℕ → ℕ

The fold X ⊔ X → X on components.

Equations

• Hironaka.Monomial.Examples.fold c = [0, 1, 0, 1].getD c 0

theorem Hironaka.Monomial.Examples.baseL_centers : baseL.step3.2 = [{{0}}, {{1}}]

theorem Hironaka.Monomial.Examples.doubleY_centers : doubleY.step3.2 = [{{0}, {2}}, {{1}, {3}}]

The run on Y blows up both copies of E⁰ at once, then both copies of E¹.

def Hironaka.Monomial.Examples.fold' : ℕ → ℕ

The extension of the fold: the new components 4, 5 (over {0}, {2}) go to 2, the new components 6, 7 to 3.

Equations

• Hironaka.Monomial.Examples.fold' c = [0, 1, 0, 1, 2, 2, 3, 3].getD c 0