The example states of the monomial procedure

Concrete states of Hironaka/Resolution/Algebraic/Monomial/State.lean on which the procedure of [Kol07, 111, Step 3] is computed, and the maximal-multiplicity procedure that [Kol07, Example 112] refutes. The computations themselves are in HironakaExamples/Monomial/Example112.lean (which is imported by the root) and in HironakaExamples/MonomialState.lean and HironakaExamples/MonomialRestrict.lean.

• example112 m hm: the surface of [Kol07, Example 112], two curves E¹, E² meeting at one point, both with exponent m + 1.
• maxMultChoice, maxMultRun, maxMultFaces, example112OtherPath: the maximal-multiplicity procedure that Kollár dismisses at the start of Step 3 (blow up the locus of highest multiplicity; "this, however, does not work, not even for surfaces"). It is defined here only to be computed against, not used by the procedure: the faces of maximal sum ≥ m (maxMultFaces), with the lexicographically largest label tuple as the tie-break (Kollár's E² ∩ E³); the centres of the other tie-break, which gives the same exponents by symmetry, are listed as example112OtherPath.
• threePhase: n = 3, m = 8, one component per label, exponents 4, 9, 3, 6, maximal faces {0} and {1, 2, 3}, an instance in which all three phases act.
• splitX, splitU: the example showing why the components of a member must carry their own exponents (the deviation recorded in Hironaka/Resolution/Algebraic/Monomial/State.lean), in its fine, labelled form: the four lines V(x), V(x-1) (label 0), V(y), V(y-1) (label 1) of 𝔸² with the exponents 1, 0, 1, 0 of I = (xy), m = 1, on X = 𝔸² and on U = D((x-1)(y-1)); coarseX, coarseU: the same example with one exponent per member, the minimum over its components, as the members of [Kol07, Definition–Lemma 110] are printed (not assumed irreducible): exponents 0, 0 on X and 1, 1 on U. Not in the sources.

Example 112

def Hironaka.Monomial.Examples.example112 (m : ℕ) (hm : 1 ≤ m) : MonomialState

The surface of [Kol07, Example 112]: E¹, E² two curves intersecting at a point with a₁ = a₂ = m + 1, as a state with components 0, 1 (labels 0, 1, the curves E¹, E²), nerve {0}, {1}, {0, 1}, exponents m + 1, n = 2.

Equations

• Hironaka.Monomial.Examples.example112 m hm = Hironaka.Monomial.MonomialState.ofValid 2 m 2 2 (fun (c : ℕ) => c) (fun (x : ℕ) => m + 1) {{0}, {1}, {0, 1}} ⋯

def Hironaka.Monomial.Examples.maxMultChoice (st : MonomialState) : Finset (Finset ℕ)

The maximal-multiplicity choice ([Kol07, 111, Step 3], the "usual method" that Kollár rejects), defined for the computations only: the faces of maximal sum ≥ m, with the lexicographically largest label tuple as the tie-break (Kollár's E² ∩ E³ in Example 112; the other tie-break gives the same exponents by symmetry).

Equations

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

def Hironaka.Monomial.Examples.maxMultRun : ℕ → MonomialState → MonomialState × List (Finset (Finset ℕ))

k steps of the maximal-multiplicity procedure: the final state and the list of centres, in order.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Monomial.Examples.maxMultRun 0 x✝ = (x✝, [])

def Hironaka.Monomial.Examples.maxMultFaces (st : MonomialState) : Finset (Finset ℕ)

The maximal-multiplicity locus before the tie-break: the faces of maximal sum ≥ m (Kollár's "highest multiplicity locus"); maxMultChoice is its tie-break.

Equations

• Hironaka.Monomial.Examples.maxMultFaces st = {T ∈ {T ∈ st.nerve | st.m ≤ st.total T} | st.total T = {T ∈ st.nerve | st.m ≤ st.total T}.sup st.total}

def Hironaka.Monomial.Examples.example112OtherPath : List (Finset (Finset ℕ))

The centres of six steps of the maximal-multiplicity procedure on Example 112 under the other tie-break (the lexicographically smallest label tuple): the point {0, 1}, then {0, 2} (Kollár's E¹ ∩ E³ instead of E² ∩ E³), then the unique maximizers {2, 3}, {3, 4}, {4, 5}, {5, 6}; the exponents come out the same by symmetry.

Equations

• Hironaka.Monomial.Examples.example112OtherPath = [{{0, 1}}, {{0, 2}}, {{2, 3}}, {{3, 4}}, {{4, 5}}, {{5, 6}}]

The three-phase instance

def Hironaka.Monomial.Examples.threePhase : MonomialState

An instance in which all three phases act: n = 3, m = 8, one component per label, exponents 4, 9, 3, 6, maximal faces {0} and {1, 2, 3}.

Equations

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

The split example

def Hironaka.Monomial.Examples.splitX : MonomialState

The fine split of the boundary E¹ = V(x(x-1)), E² = V(y(y-1)) of 𝔸²: the four lines V(x), V(x-1) (label 0) and V(y), V(y-1) (label 1) with the exponents 1, 0, 1, 0 of I = (xy) along them, m = 1; the nerve is the four double points.

Equations

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

def Hironaka.Monomial.Examples.splitU : MonomialState

The same on U = D((x-1)(y-1)): the components 1, 3 (V(x-1), V(y-1)) are dead, the nerve is {0}, {2}, {0, 2}.

Equations

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

def Hironaka.Monomial.Examples.coarseX : MonomialState

The coarse split, one exponent per member as in [Kol07, Definition–Lemma 110] with members not assumed irreducible: on X = 𝔸², E¹ = V(x(x-1)), E² = V(y(y-1)) with the coarse exponents c_j = min_D ord_D (xy) = 0, 0; m = 1; nerve {0}, {1}, {0, 1}.

Equations

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

def Hironaka.Monomial.Examples.coarseU : MonomialState

The coarse split on U = D((x-1)(y-1)): E¹|_U = V(x) and E²|_U = V(y) are irreducible, so the coarse exponents are 1, 1.

Equations

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