The monomial state: Kollár's Step 3 as a combinatorial object

Step 3 of the proof of [Kol07, Theorem 107] ([Kol07, 111, Step 3]) reduces the order of a monomial ideal 𝒪_X(-∑ a_j E^j), E = ∑ E^j a simple normal crossing divisor with an ordered index set, below the mark m by blowing up intersections of the E^j in a prescribed order. The procedure only looks at which intersections are nonempty and at the exponents, so this module runs it on a purely combinatorial state, with no scheme in sight. The state records the irreducible components of the divisors as natural numbers below nextComp, each with the label of its divisor E^j (a natural number below nextLabel; the exceptional divisor of a blow-up gets the label nextLabel, [Kol07, Definition 65]: the new divisor is put last) and an exponent, and the nerve: the finite family of nonempty sets of components with nonempty common intersection. The nerve is down-closed, its faces have size at most the dimension bound n and carry at most one component per label; dead components (empty divisors) lie in no face.

Deviation from the source. Kollár's state has one exponent per divisor E^j and blows up the whole intersection E^{j₁} ∩ ⋯ ∩ E^{j_r}. Here every irreducible component of E^j has its own exponent (the order of the ideal along that component, the fine monomial split of Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialPart.lean), and the centre at a phase is a set of faces with a common label tuple, each of which contributes its own exceptional component with its own exponent. With one component per label the two procedures coincide. The refinement is forced by functoriality under open immersions: with one exponent per possibly reducible member the procedure is not even compatible with restriction to an open subscheme (HironakaExamples/Monomial/Examples.lean, coarseX and coarseU, and the computation split_coarse_runs of HironakaExamples/Monomial/Example112.lean). Not in the sources in this form.

• MonomialState; total (the sum a(T) of the exponents of a face), labels, labelTuple (the sorted list of the labels of a face, Kollár's (j₁ < ⋯ < j_r)).
• blowUp st S: the transition for a centre S (a finset of faces with a common label tuple): new label nextLabel; one new component newComp S P per face P ∈ S with that label and exponent a(P) - m; the nerve transformed by the rule N ↦ {T ∈ N : P ⊄ T} ∪ {T₁ ∪ {c_P} : T₁ ∪ P ∈ N, P ⊄ T₁} for the faces P of the centre. The definition applies the rule to all faces of S at once and asks, for the new faces of P, that no face of the centre be contained in T₁; for a centre this is the condition P ⊄ T₁ of the rule (mem_blowUp_nerve), and it makes the transition a total function of the state and an arbitrary finset of faces, preserving every invariant of the state. That this rule is what the total transform of the boundary does under the blow-up of the centre is proved on schemes in Hironaka/Resolution/Algebraic/Monomial/Geometric/Kernel.lean (nerve_blowUpPieces).
• faces st r, maxTotal, numMax, measure st r = toLex (m_r, n_r) and Star st s: Kollár's (m_r(E), n_r(E)) and (∗_s) of [Kol07, 111, Step 3.r], counting faces of components.
• choice st r: Kollár's choice at phase r, the faces of size r of maximal sum among those of sum ≥ m, whose label tuple is lexicographically smallest among the maximizers; empty when no r-face has sum ≥ m (mem_choice, choice_eq_empty_iff).
• Valid, ofValid, valid_self: the invariants as a decidable predicate on the raw data, so that concrete states can be built by decide.

The measure decreases under a blow-up along choice st r (Hironaka/Resolution/Algebraic/Monomial/Measure.lean); the phases and their termination are Hironaka/Resolution/Algebraic/Monomial/Step3Phases.lean. The geometric realisation of the state on a scheme is Hironaka.Monomial.PieceFamily (Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean), and the real-analytic strand (Hironaka/Resolution/Analytic/OrderReduction/BMO/Step3Monomial/) runs the same combinatorial procedure on its own piece families.

structure Hironaka.Monomial.MonomialState : Type

The combinatorial state of the monomial procedure of [Kol07, 111, Step 3]. Components and labels are natural numbers below nextComp and nextLabel; label c is the divisor E^j the component c belongs to, a c its exponent; nerve is the family of faces (nonempty sets of components with nonempty common intersection): down-closed, every face of size at most the dimension bound n, with injective labels. Dead components lie in no face.

• n : ℕ

  The dimension bound n = dim X (the last phase of Step 3 is Step 3.n).

• m : ℕ

  The marking m ≥ 1 of the marked monomial ideal.

• one_le_m : 1 ≤ self.m
• nextComp : ℕ

  Components are 0, …, nextComp - 1; a blow-up allocates from nextComp.

• nextLabel : ℕ

  Labels are 0, …, nextLabel - 1; a blow-up creates the label nextLabel.

• label : ℕ → ℕ

  The label (index of the divisor E^j) of a component.

• a : ℕ → ℕ

  The exponent of a component.

• nerve : Finset (Finset ℕ)

  The nerve: the faces.

• nerve_nonempty (T : Finset ℕ) : T ∈ self.nerve → T.Nonempty
• nerve_lt (T : Finset ℕ) : T ∈ self.nerve → ∀ c ∈ T, c < self.nextComp
• label_lt (c : ℕ) : c < self.nextComp → self.label c < self.nextLabel
• nerve_down (T : Finset ℕ) : T ∈ self.nerve → ∀ T' ⊆ T, T'.Nonempty → T' ∈ self.nerve
• nerve_card (T : Finset ℕ) : T ∈ self.nerve → T.card ≤ self.n
• nerve_labels (T : Finset ℕ) : T ∈ self.nerve → Set.InjOn self.label ↑T

theorem Hironaka.Monomial.MonomialState.ext_iff {x y : MonomialState} : x = y ↔ x.n = y.n ∧ x.m = y.m ∧ x.nextComp = y.nextComp ∧ x.nextLabel = y.nextLabel ∧ x.label = y.label ∧ x.a = y.a ∧ x.nerve = y.nerve

theorem Hironaka.Monomial.MonomialState.ext {x y : MonomialState} (n : x.n = y.n) (m : x.m = y.m) (nextComp : x.nextComp = y.nextComp) (nextLabel : x.nextLabel = y.nextLabel) (label : x.label = y.label) (a : x.a = y.a) (nerve : x.nerve = y.nerve) : x = y

def Hironaka.Monomial.MonomialState.total (st : MonomialState) (T : Finset ℕ) : ℕ

The sum a(T) = ∑_{c ∈ T} a_c of the exponents of a set of components.

Equations

• st.total T = ∑ c ∈ T, st.a c

def Hironaka.Monomial.MonomialState.labels (st : MonomialState) (T : Finset ℕ) : Finset ℕ

The set of labels of a set of components.

Equations

• st.labels T = Finset.image st.label T

def Hironaka.Monomial.MonomialState.sortedList (s : Finset ℕ) : List ℕ

The elements of a finset of naturals as an increasing list: the numbers below sup + 1 that lie in the set. (Mathlib's Finset.sort is defined by well-founded recursion and does not reduce in the kernel; this enumeration does, so that the example computations run by decide.)

Equations

• Hironaka.Monomial.MonomialState.sortedList s = List.filter (fun (x : ℕ) => decide (x ∈ s)) (List.range (s.sup id + 1))

theorem Hironaka.Monomial.MonomialState.mem_sortedList {s : Finset ℕ} {x : ℕ} : x ∈ sortedList s ↔ x ∈ s

theorem Hironaka.Monomial.MonomialState.sortedList_toFinset (s : Finset ℕ) : (sortedList s).toFinset = s

theorem Hironaka.Monomial.MonomialState.sortedList_injective : Function.Injective sortedList

theorem Hironaka.Monomial.MonomialState.sortedList_pairwise (s : Finset ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (sortedList s)

sortedList s is increasing.

def Hironaka.Monomial.MonomialState.labelTuple (st : MonomialState) (T : Finset ℕ) : List ℕ

The label tuple of a face: its labels as an increasing list, Kollár's (j₁ < ⋯ < j_r), compared lexicographically.

Equations

• st.labelTuple T = Hironaka.Monomial.MonomialState.sortedList (st.labels T)

theorem Hironaka.Monomial.MonomialState.total_insert (st : MonomialState) {T : Finset ℕ} {c : ℕ} (hc : c ∉ T) : st.total (insert c T) = st.a c + st.total T

theorem Hironaka.Monomial.MonomialState.total_erase_add (st : MonomialState) {T : Finset ℕ} {c : ℕ} (hc : c ∈ T) : st.total (T.erase c) + st.a c = st.total T

theorem Hironaka.Monomial.MonomialState.total_empty (st : MonomialState) : st.total ∅ = 0

theorem Hironaka.Monomial.MonomialState.labelTuple_eq_iff (st : MonomialState) {T T' : Finset ℕ} : st.labelTuple T = st.labelTuple T' ↔ st.labels T = st.labels T'

theorem Hironaka.Monomial.MonomialState.lt_nextComp_of_mem (st : MonomialState) {T : Finset ℕ} (hT : T ∈ st.nerve) {c : ℕ} (hc : c ∈ T) : c < st.nextComp

A face of the nerve has all its components below nextComp.

theorem Hironaka.Monomial.MonomialState.mem_nerve_of_subset (st : MonomialState) {T T' : Finset ℕ} (hT : T ∈ st.nerve) (h : T' ⊆ T) (hne : T'.Nonempty) : T' ∈ st.nerve

The nonempty subsets of a face are faces.

Kollár's measure and (∗_s)

def Hironaka.Monomial.MonomialState.faces (st : MonomialState) (r : ℕ) : Finset (Finset ℕ)

The faces of size r.

Equations

• st.faces r = {T ∈ st.nerve | T.card = r}

theorem Hironaka.Monomial.MonomialState.mem_faces (st : MonomialState) {r : ℕ} {T : Finset ℕ} : T ∈ st.faces r ↔ T ∈ st.nerve ∧ T.card = r

def Hironaka.Monomial.MonomialState.maxTotal (st : MonomialState) (r : ℕ) : ℕ

Kollár's m_r(E) of [Kol07, 111, Step 3.r]: the maximal sum of an r-face (0 if there is none).

Equations

• st.maxTotal r = (st.faces r).sup st.total

def Hironaka.Monomial.MonomialState.numMax (st : MonomialState) (r : ℕ) : ℕ

Kollár's n_r(E) of [Kol07, 111, Step 3.r]: the number of r-faces achieving m_r(E).

Equations

• st.numMax r = {T ∈ st.faces r | st.total T = st.maxTotal r}.card

def Hironaka.Monomial.MonomialState.measure (st : MonomialState) (r : ℕ) : Lex (ℕ × ℕ)

Kollár's pair (m_r(E), n_r(E)) of [Kol07, 111, Step 3.2 and 3.r] in the lexicographic order ℕ ×ₗ ℕ.

Equations

• st.measure r = toLex (st.maxTotal r, st.numMax r)

def Hironaka.Monomial.MonomialState.Star (st : MonomialState) (s : ℕ) : Prop

Kollár's condition (∗_s) of [Kol07, 111, Step 3.r]: every face of size s has sum < m.

Equations

• st.Star s = ∀ T ∈ st.faces s, st.total T < st.m

theorem Hironaka.Monomial.MonomialState.total_le_maxTotal (st : MonomialState) {r : ℕ} {T : Finset ℕ} (hT : T ∈ st.faces r) : st.total T ≤ st.maxTotal r

theorem Hironaka.Monomial.MonomialState.maxTotal_le (st : MonomialState) {r b : ℕ} (h : ∀ T ∈ st.faces r, st.total T ≤ b) : st.maxTotal r ≤ b

theorem Hironaka.Monomial.MonomialState.star_zero (st : MonomialState) : st.Star 0

(∗_0) holds vacuously: faces are nonempty.

theorem Hironaka.Monomial.MonomialState.star_of_lt (st : MonomialState) {s : ℕ} (hs : st.n < s) : st.Star s

(∗_s) holds vacuously for s > n: faces have size at most n.

Kollár's choice

def Hironaka.Monomial.MonomialState.candidates (st : MonomialState) (r : ℕ) : Finset (Finset ℕ)

The candidates at phase r: the faces of size r of sum ≥ m.

Equations

• st.candidates r = {T ∈ st.faces r | st.m ≤ st.total T}

def Hironaka.Monomial.MonomialState.maximizers (st : MonomialState) (r : ℕ) : Finset (Finset ℕ)

The candidates of maximal sum.

Equations

• st.maximizers r = {T ∈ st.candidates r | st.total T = (st.candidates r).sup st.total}

def Hironaka.Monomial.MonomialState.choice (st : MonomialState) (r : ℕ) : Finset (Finset ℕ)

Kollár's choice at phase r ([Kol07, 111, Steps 3.1, 3.2 and 3.r]): the faces of size r of maximal sum among those of sum ≥ m whose label tuple is lexicographically smallest among the maximizers; empty when no r-face has sum ≥ m. With one component per label these are the faces of the lexicographically smallest (j₁ < ⋯ < j_r) with E^{j₁} ∩ ⋯ ∩ E^{j_r} ≠ ∅ and a_{j₁} + ⋯ + a_{j_r} ≥ m maximal, as in the source.

Equations

• st.choice r = {T ∈ st.maximizers r | ∀ T' ∈ st.maximizers r, st.labelTuple T ≤ st.labelTuple T'}

theorem Hironaka.Monomial.MonomialState.mem_candidates (st : MonomialState) {r : ℕ} {T : Finset ℕ} : T ∈ st.candidates r ↔ T ∈ st.faces r ∧ st.m ≤ st.total T

theorem Hironaka.Monomial.MonomialState.mem_maximizers (st : MonomialState) {r : ℕ} {T : Finset ℕ} : T ∈ st.maximizers r ↔ T ∈ st.faces r ∧ st.m ≤ st.total T ∧ ∀ T' ∈ st.faces r, st.m ≤ st.total T' → st.total T' ≤ st.total T

theorem Hironaka.Monomial.MonomialState.mem_choice (st : MonomialState) {r : ℕ} {T : Finset ℕ} : T ∈ st.choice r ↔ T ∈ st.faces r ∧ st.m ≤ st.total T ∧ (∀ T' ∈ st.faces r, st.m ≤ st.total T' → st.total T' ≤ st.total T) ∧ ∀ T' ∈ st.faces r, st.total T' = st.total T → st.labelTuple T ≤ st.labelTuple T'

The characterization of Kollár's choice: the faces of size r of sum ≥ m and of maximal sum among those, whose label tuple is lexicographically smallest among the faces of that sum.

theorem Hironaka.Monomial.MonomialState.mem_faces_of_mem_choice (st : MonomialState) {r : ℕ} {T : Finset ℕ} (h : T ∈ st.choice r) : T ∈ st.faces r

theorem Hironaka.Monomial.MonomialState.mem_nerve_of_mem_choice (st : MonomialState) {r : ℕ} {T : Finset ℕ} (h : T ∈ st.choice r) : T ∈ st.nerve

theorem Hironaka.Monomial.MonomialState.card_of_mem_choice (st : MonomialState) {r : ℕ} {T : Finset ℕ} (h : T ∈ st.choice r) : T.card = r

theorem Hironaka.Monomial.MonomialState.m_le_total_of_mem_choice (st : MonomialState) {r : ℕ} {T : Finset ℕ} (h : T ∈ st.choice r) : st.m ≤ st.total T

theorem Hironaka.Monomial.MonomialState.total_eq_of_mem_choice (st : MonomialState) {r : ℕ} {T T' : Finset ℕ} (h : T ∈ st.choice r) (h' : T' ∈ st.choice r) : st.total T = st.total T'

The faces of the center have a common sum.

theorem Hironaka.Monomial.MonomialState.labelTuple_eq_of_mem_choice (st : MonomialState) {r : ℕ} {T T' : Finset ℕ} (h : T ∈ st.choice r) (h' : T' ∈ st.choice r) : st.labelTuple T = st.labelTuple T'

The faces of the center have a common label tuple.

theorem Hironaka.Monomial.MonomialState.total_eq_maxTotal_of_mem_choice (st : MonomialState) {r : ℕ} {T : Finset ℕ} (h : T ∈ st.choice r) : st.total T = st.maxTotal r

The faces of the center are the r-faces of sum m_r, when the center is nonempty.

theorem Hironaka.Monomial.MonomialState.choice_eq_empty_iff (st : MonomialState) {r : ℕ} : st.choice r = ∅ ↔ st.Star r

Kollár's choice is empty exactly when (∗_r) holds.

theorem Hironaka.Monomial.MonomialState.choice_nonempty_iff (st : MonomialState) {r : ℕ} : (st.choice r).Nonempty ↔ ¬st.Star r

The transition

def Hironaka.Monomial.MonomialState.blowUpNerve (N S : Finset (Finset ℕ)) (c : Finset ℕ → ℕ) : Finset (Finset ℕ)

The nerve rule for the faces of a centre S, with c P the new component of the face P: the old faces containing no face of the centre, and for each P ∈ S the faces T₁ ∪ {c P} with T₁ ∪ P an old face and no face of the centre inside T₁.

Equations

• Hironaka.Monomial.MonomialState.blowUpNerve N S c = {T ∈ N | ∀ P ∈ S, ¬P ⊆ T} ∪ S.biUnion fun (P : Finset ℕ) => Finset.image (insert (c P)) ({T₁ ∈ insert ∅ N | T₁ ∪ P ∈ N ∧ ∀ Q ∈ S, ¬Q ⊆ T₁})

theorem Hironaka.Monomial.MonomialState.mem_blowUpNerve {N S : Finset (Finset ℕ)} {c : Finset ℕ → ℕ} {T : Finset ℕ} : T ∈ blowUpNerve N S c ↔ (T ∈ N ∧ ∀ P ∈ S, ¬P ⊆ T) ∨ ∃ P ∈ S, ∃ (T₁ : Finset ℕ), (T₁ = ∅ ∨ T₁ ∈ N) ∧ T₁ ∪ P ∈ N ∧ (∀ Q ∈ S, ¬Q ⊆ T₁) ∧ T = insert (c P) T₁

def Hironaka.Monomial.MonomialState.faceList (P : Finset ℕ) : List ℕ

The components of a face as an increasing list: the key ordering the faces of a center.

Equations

• Hironaka.Monomial.MonomialState.faceList P = Hironaka.Monomial.MonomialState.sortedList P

theorem Hironaka.Monomial.MonomialState.faceList_injective : Function.Injective faceList

def Hironaka.Monomial.MonomialState.rank (S : Finset (Finset ℕ)) (P : Finset ℕ) : ℕ

The rank of the face P among the faces of the center S, in the order of faceList.

Equations

• Hironaka.Monomial.MonomialState.rank S P = {Q ∈ S | Hironaka.Monomial.MonomialState.faceList Q < Hironaka.Monomial.MonomialState.faceList P}.card

theorem Hironaka.Monomial.MonomialState.rank_lt_card {S : Finset (Finset ℕ)} {P : Finset ℕ} (hP : P ∈ S) : rank S P < S.card

theorem Hironaka.Monomial.MonomialState.rank_lt_rank {S : Finset (Finset ℕ)} {P Q : Finset ℕ} (hP : P ∈ S) (h : faceList P < faceList Q) : rank S P < rank S Q

theorem Hironaka.Monomial.MonomialState.rank_injOn (S : Finset (Finset ℕ)) : Set.InjOn (rank S) ↑S

def Hironaka.Monomial.MonomialState.newComp (st : MonomialState) (S : Finset (Finset ℕ)) (P : Finset ℕ) : ℕ

The new component allocated to the face P of the center S: nextComp + rank S P.

Equations

• st.newComp S P = st.nextComp + Hironaka.Monomial.MonomialState.rank S P

theorem Hironaka.Monomial.MonomialState.nextComp_le_newComp (st : MonomialState) (S : Finset (Finset ℕ)) (P : Finset ℕ) : st.nextComp ≤ st.newComp S P

theorem Hironaka.Monomial.MonomialState.newComp_lt (st : MonomialState) {S : Finset (Finset ℕ)} {P : Finset ℕ} (hP : P ∈ S) : st.newComp S P < st.nextComp + S.card

theorem Hironaka.Monomial.MonomialState.newComp_injOn (st : MonomialState) (S : Finset (Finset ℕ)) : Set.InjOn (st.newComp S) ↑S

theorem Hironaka.Monomial.MonomialState.newComp_notMem (st : MonomialState) {S : Finset (Finset ℕ)} {P T : Finset ℕ} (hT : T ∈ st.nerve) : st.newComp S P ∉ T

def Hironaka.Monomial.MonomialState.blowUp (st : MonomialState) (S : Finset (Finset ℕ)) : MonomialState

The transition for a centre S ([Kol07, 111, Step 3.2 and 3.r]: the new divisor is put last with exponent a_{j₁} + ⋯ + a_{j_r} - m). New label nextLabel; for each P ∈ S a new component newComp S P with label nextLabel and exponent a(P) - m; the other exponents and labels unchanged; the nerve transformed by the rule of blowUpNerve.

Equations

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

The transition, read off

@[simp]

theorem Hironaka.Monomial.MonomialState.blowUp_n (st : MonomialState) (S : Finset (Finset ℕ)) : (st.blowUp S).n = st.n

@[simp]

theorem Hironaka.Monomial.MonomialState.blowUp_m (st : MonomialState) (S : Finset (Finset ℕ)) : (st.blowUp S).m = st.m

@[simp]

theorem Hironaka.Monomial.MonomialState.blowUp_nextComp (st : MonomialState) (S : Finset (Finset ℕ)) : (st.blowUp S).nextComp = st.nextComp + S.card

@[simp]

theorem Hironaka.Monomial.MonomialState.blowUp_nextLabel (st : MonomialState) (S : Finset (Finset ℕ)) : (st.blowUp S).nextLabel = st.nextLabel + 1

theorem Hironaka.Monomial.MonomialState.blowUp_nerve (st : MonomialState) (S : Finset (Finset ℕ)) : (st.blowUp S).nerve = blowUpNerve st.nerve S (st.newComp S)

theorem Hironaka.Monomial.MonomialState.blowUp_label_of_lt (st : MonomialState) (S : Finset (Finset ℕ)) {c : ℕ} (hc : c < st.nextComp) : (st.blowUp S).label c = st.label c

theorem Hironaka.Monomial.MonomialState.blowUp_a_of_lt (st : MonomialState) (S : Finset (Finset ℕ)) {c : ℕ} (hc : c < st.nextComp) : (st.blowUp S).a c = st.a c

theorem Hironaka.Monomial.MonomialState.blowUp_label_newComp (st : MonomialState) (S : Finset (Finset ℕ)) (P : Finset ℕ) : (st.blowUp S).label (st.newComp S P) = st.nextLabel

The new components carry the new label.

theorem Hironaka.Monomial.MonomialState.blowUp_a_newComp (st : MonomialState) (S : Finset (Finset ℕ)) {P : Finset ℕ} (hP : P ∈ S) : (st.blowUp S).a (st.newComp S P) = st.total P - st.m

The new component of the face P has exponent a(P) - m.

theorem Hironaka.Monomial.MonomialState.blowUp_total_of_lt (st : MonomialState) (S : Finset (Finset ℕ)) {T : Finset ℕ} (hT : ∀ c ∈ T, c < st.nextComp) : (st.blowUp S).total T = st.total T

The sum of a set of old components is unchanged.

theorem Hironaka.Monomial.MonomialState.blowUp_total_insert_newComp (st : MonomialState) (S : Finset (Finset ℕ)) {P T₁ : Finset ℕ} (hP : P ∈ S) (hT₁ : ∀ c ∈ T₁, c < st.nextComp) : (st.blowUp S).total (insert (st.newComp S P) T₁) = st.total P - st.m + st.total T₁

The sum of a new face T₁ ∪ {c_P}: a(T₁) + (a(P) - m).

def Hironaka.Monomial.MonomialState.IsCenter (st : MonomialState) (S : Finset (Finset ℕ)) : Prop

A centre: a finset of faces with a common label tuple (each face of sum ≥ m is the admissibility condition, not part of this predicate).

Equations

• st.IsCenter S = (S ⊆ st.nerve ∧ ∀ P ∈ S, ∀ Q ∈ S, st.labels P = st.labels Q)

theorem Hironaka.Monomial.MonomialState.isCenter_choice (st : MonomialState) (r : ℕ) : st.IsCenter (st.choice r)

Kollár's choice is a center.

theorem Hironaka.Monomial.MonomialState.eq_of_isCenter_of_subset (st : MonomialState) (S : Finset (Finset ℕ)) {P Q T : Finset ℕ} (hS : st.IsCenter S) (hP : P ∈ S) (hQ : Q ∈ S) (hT : T ∈ st.nerve) (hPT : P ⊆ T) (hQT : Q ⊆ T) : P = Q

Two faces of a center contained in a common face are equal (the components of a label are disjoint: a face has injective labels).

theorem Hironaka.Monomial.MonomialState.mem_blowUp_nerve (st : MonomialState) (S : Finset (Finset ℕ)) {T : Finset ℕ} (hS : st.IsCenter S) : T ∈ (st.blowUp S).nerve ↔ (T ∈ st.nerve ∧ ∀ P ∈ S, ¬P ⊆ T) ∨ ∃ P ∈ S, ∃ (T₁ : Finset ℕ), T₁ ∪ P ∈ st.nerve ∧ ¬P ⊆ T₁ ∧ T = insert (st.newComp S P) T₁

For a centre, the rule reads as stated in the module docstring: the new faces of P are the T₁ ∪ {c_P} with T₁ ∪ P ∈ N and P ⊄ T₁.

A decidable constructor (for the example computations by decide)

def Hironaka.Monomial.MonomialState.Valid (n m k L : ℕ) (label : ℕ → ℕ) (N : Finset (Finset ℕ)) : Prop

The invariants of a state with bounded quantifiers, decidable for concrete data.

Equations

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

@[instance_reducible]

instance Hironaka.Monomial.MonomialState.decidableValid (n m k L : ℕ) (label : ℕ → ℕ) (N : Finset (Finset ℕ)) : Decidable (Valid n m k L label N)

Equations

• Hironaka.Monomial.MonomialState.decidableValid n m k L label N = id inferInstance

def Hironaka.Monomial.MonomialState.ofValid (n m k L : ℕ) (label a : ℕ → ℕ) (N : Finset (Finset ℕ)) (h : Valid n m k L label N) : MonomialState

A state from checked data (the invariants by decide on concrete data).

Equations

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

theorem Hironaka.Monomial.MonomialState.valid_self (st : MonomialState) : Valid st.n st.m st.nextComp st.nextLabel st.label st.nerve

The data of a monomial state are Valid (its six invariants).