The invariant of the restriction argument

The invariant carried along the pair of runs in the proof that Kollár's Step 3 commutes with restriction to a subnerve (Sub of Hironaka/Resolution/Algebraic/Monomial/Restrict.lean; the second clause of [Kol07, 34.1]). Not in the sources. Sub L N is preserved by a blow-up along any finset of faces (Sub.blowUp: the nerve rule is monotone in the nerve); if a face of Kollár's centre of N lies in L, the centre of L is the centre of N restricted to the faces of L (Sub.choice_eq_of_mem: L's maximum is N's and the lexicographically smallest label tuple is the same); a blow-up along nonempty faces none of which is a face of L does not change the nerve of L (blowUp_nerve_of_forall_notMem); and the pulled-back run ends in a state Sub the final state of N (Sub.foldl, sub_foldl_step3). The induction that uses these is Hironaka/Resolution/Algebraic/Monomial/Restrict/Phase.lean.

theorem Hironaka.Monomial.MonomialState.blowUpNerve_mono {N N' S : Finset (Finset ℕ)} {c : Finset ℕ → ℕ} (h : N ⊆ N') : blowUpNerve N S c ⊆ blowUpNerve N' S c

theorem Hironaka.Monomial.MonomialState.Sub.total_eq {L N : MonomialState} (h : L.Sub N) (T : Finset ℕ) : L.total T = N.total T

theorem Hironaka.Monomial.MonomialState.Sub.newComp_eq {L N : MonomialState} (h : L.Sub N) (S : Finset (Finset ℕ)) (P : Finset ℕ) : L.newComp S P = N.newComp S P

theorem Hironaka.Monomial.MonomialState.Sub.blowUp {L N : MonomialState} (h : L.Sub N) (S : Finset (Finset ℕ)) : (L.blowUp S).Sub (N.blowUp S)

The invariant L_i ⊆ N_i with equal exponents and labels is preserved by a blow-up along any S: the rule is monotone in the nerve.

theorem Hironaka.Monomial.MonomialState.Sub.mem_faces {L N : MonomialState} (h : L.Sub N) {r : ℕ} {T : Finset ℕ} (hT : T ∈ L.faces r) : T ∈ N.faces r

theorem Hironaka.Monomial.MonomialState.Sub.labelTuple_eq {L N : MonomialState} (h : L.Sub N) (T : Finset ℕ) : L.labelTuple T = N.labelTuple T

theorem Hironaka.Monomial.MonomialState.Sub.choice_eq_of_mem {L N : MonomialState} (h : L.Sub N) {r : ℕ} {P : Finset ℕ} (hP : P ∈ N.choice r) (hPL : P ∈ L.nerve) : L.choice r = {x ∈ N.choice r | x ∈ L.nerve}

If a face of Kollár's centre of N lies in L, the centre of L is the centre of N restricted to the faces of L.

theorem Hironaka.Monomial.MonomialState.blowUp_nerve_of_forall_notMem (L : MonomialState) {S : Finset (Finset ℕ)} (hS0 : ∀ P ∈ S, P.Nonempty) (hS : ∀ P ∈ S, P ∉ L.nerve) : (L.blowUp S).nerve = L.nerve

A blow-up along faces none of which is a face of L does not change the nerve of L: no face of L contains such a face, and no new face is created.

theorem Hironaka.Monomial.MonomialState.Sub.foldl {L N : MonomialState} (h : L.Sub N) (Ns : List (Finset (Finset ℕ))) : (List.foldl MonomialState.blowUp L Ns).Sub (List.foldl MonomialState.blowUp N Ns)

Sub is preserved along a list of centres.

theorem Hironaka.Monomial.MonomialState.sub_foldl_step3 {L N : MonomialState} (h : L.Sub N) : (List.foldl blowUp L N.step3.2).Sub N.step3.1

The pulled-back run ends in a state Sub the final state of N.