Functoriality under restriction: the induction along the run

Kollár's Step 3 on the monomial state commutes with restriction to a subnerve: for Sub L N (Hironaka/Resolution/Algebraic/Monomial/Restrict.lean) the run on L is the run on N pulled back, with the empty blow-ups deleted and the components and labels reindexed by order embeddings (step3_restrict). This is the second clause of [Kol07, 34.1] for the combinatorial procedure; the proof is not in the sources.

Three states are carried along the run on N: the direct state D (the run on the subnerve L), the pulled-back state P (the centres of N applied to L, dead components and unused labels included) and N itself, with Rel ρ σ D P (P is D renumbered, Hironaka/Resolution/Algebraic/Monomial/Restrict/Rename.lean) and Sub P N (Hironaka/Resolution/Algebraic/Monomial/Restrict/Invariant.lean). Along phase r of N (phase_restrict, by the functional induction principle of phase): a centre of N disjoint from P's nerve does not change P's nerve or D (Rel.of_blowUp_disjoint); a centre meeting it restricts to Kollár's centre of P (Sub.choice_eq_of_mem), which is the image of Kollár's centre of D (Rel.choice_eq), and the three states advance together with the renumbering extended (Rel.blowUp of Hironaka/Resolution/Algebraic/Monomial/Restrict/Extend.lean); when N's phase ends, D's has ended too. The phases compose (phases_restrict), and step3_restrict reads the result off with the renumberings packaged as order embeddings (exists_orderEmbedding_extend).

Together with step3_refine of Hironaka/Resolution/Algebraic/Monomial/Restrict/RefinePhase.lean this gives the functoriality of the geometric Step 3 under smooth morphisms (Hironaka/Resolution/Algebraic/Monomial/Geometric/ChainRunErase.lean).

The pulled-back run, unfolded

theorem Hironaka.Monomial.MonomialState.restrictRun_nil (st : MonomialState) : st.restrictRun [] = []

theorem Hironaka.Monomial.MonomialState.restrictRun_cons_of_eq_empty (st : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {x ∈ S | x ∈ st.nerve} = ∅) : st.restrictRun (S :: Ns) = (st.blowUp S).restrictRun Ns

theorem Hironaka.Monomial.MonomialState.restrictRun_cons_of_ne_empty (st : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {x ∈ S | x ∈ st.nerve} ≠ ∅) : st.restrictRun (S :: Ns) = {x ∈ S | x ∈ st.nerve} :: (st.blowUp S).restrictRun Ns

theorem Hironaka.Monomial.MonomialState.restrictRun_append (st : MonomialState) (L₁ L₂ : List (Finset (Finset ℕ))) : st.restrictRun (L₁ ++ L₂) = st.restrictRun L₁ ++ (List.foldl blowUp st L₁).restrictRun L₂

Counters and centers along a phase

theorem Hironaka.Monomial.MonomialState.nextComp_le_blowUp (st : MonomialState) (S : Finset (Finset ℕ)) : st.nextComp ≤ (st.blowUp S).nextComp

theorem Hironaka.Monomial.MonomialState.nextLabel_le_blowUp (st : MonomialState) (S : Finset (Finset ℕ)) : st.nextLabel ≤ (st.blowUp S).nextLabel

theorem Hironaka.Monomial.MonomialState.phase_nextComp_le {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) : st.nextComp ≤ (phase r st hs).1.nextComp

theorem Hironaka.Monomial.MonomialState.phase_nextLabel_le {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) : st.nextLabel ≤ (phase r st hs).1.nextLabel

theorem Hironaka.Monomial.MonomialState.phase_centers_lt {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) (S : Finset (Finset ℕ)) : S ∈ (phase r st hs).2 → ∀ Q ∈ S, ∀ c ∈ Q, c < (phase r st hs).1.nextComp

Every component of a centre of a phase lies below the final counter.

A center disjoint from the subnerve

theorem Hironaka.Monomial.MonomialState.Sub.star_of_star {L N : MonomialState} (h : L.Sub N) {s : ℕ} (hs : N.Star s) : L.Star s

theorem Hironaka.Monomial.MonomialState.Sub.choice_eq_empty_of {L N : MonomialState} (h : L.Sub N) {r : ℕ} (hN : N.choice r = ∅) : L.choice r = ∅

theorem Hironaka.Monomial.MonomialState.Rel.of_blowUp_disjoint {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {S : Finset (Finset ℕ)} (hS0 : ∀ Q ∈ S, Q.Nonempty) (hdis : ∀ Q ∈ S, Q ∉ P.nerve) : Rel ρ σ D (P.blowUp S)

A blow-up of P along nonempty faces none of which is a face of P keeps Rel: the nerve is unchanged and the old components keep their exponents and labels.

The induction along a phase

theorem Hironaka.Monomial.MonomialState.image_image_congr {ρ ρ' : ℕ → ℕ} {K : ℕ} (hρ : ∀ c < K, ρ' c = ρ c) {S : Finset (Finset ℕ)} (hS : ∀ Q ∈ S, ∀ c ∈ Q, c < K) : Finset.image (Finset.image ρ') S = Finset.image (Finset.image ρ) S

The image of a family of faces under a renumbering that agrees with ρ on the components involved.

theorem Hironaka.Monomial.MonomialState.phase_restrict (r : ℕ) (N : MonomialState) (hsN : ∀ s < r, N.Star s) (D P : MonomialState) (ρ σ : ℕ → ℕ) : Rel ρ σ D P → P.Sub N → ∀ (hsD : ∀ s < r, D.Star s), ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), (∀ c < D.nextComp, ρ' c = ρ c) ∧ (∀ ℓ < D.nextLabel, σ' ℓ = σ ℓ) ∧ Rel ρ' σ' (phase r D hsD).1 (List.foldl blowUp P (phase r N hsN).2) ∧ (List.foldl blowUp P (phase r N hsN).2).Sub (phase r N hsN).1 ∧ List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) (phase r D hsD).2 = P.restrictRun (phase r N hsN).2

Phase r of the run on N, with the direct state D and the pulled-back state P carried along: the renumbering extends, Rel and Sub persist, and the centres of D's phase are the nonempty restrictions of the centres of N's phase.

The phases and Step 3

theorem Hironaka.Monomial.MonomialState.phases_restrict (k r : ℕ) (N : MonomialState) (hsN : ∀ s < r, N.Star s) (D P : MonomialState) (ρ σ : ℕ → ℕ) : Rel ρ σ D P → P.Sub N → ∀ (hsD : ∀ s < r, D.Star s), ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), (∀ c < D.nextComp, ρ' c = ρ c) ∧ (∀ ℓ < D.nextLabel, σ' ℓ = σ ℓ) ∧ Rel ρ' σ' (phases k r D hsD).1 (List.foldl blowUp P (phases k r N hsN).2) ∧ (List.foldl blowUp P (phases k r N hsN).2).Sub (phases k r N hsN).1 ∧ List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) (phases k r D hsD).2 = P.restrictRun (phases k r N hsN).2

theorem Hironaka.Monomial.MonomialState.IsRun.nextComp_le {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') : st.nextComp ≤ st'.nextComp

theorem Hironaka.Monomial.MonomialState.IsRun.nextLabel_le {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') : st.nextLabel ≤ st'.nextLabel

theorem Hironaka.Monomial.MonomialState.IsRun.centers_lt {st st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : st.IsRun L st') (S : Finset (Finset ℕ)) : S ∈ L → ∀ Q ∈ S, ∀ c ∈ Q, c < st'.nextComp

Every component of a centre of a run lies below the final counter.

theorem Hironaka.Monomial.MonomialState.exists_orderEmbedding_extend (f : ℕ → ℕ) (K : ℕ) (hf : StrictMonoOn f (Set.Iio K)) : ∃ (g : ℕ ↪o ℕ), ∀ c < K, g c = f c

A map strictly monotone below K extends to an order embedding of ℕ.

theorem Hironaka.Monomial.MonomialState.step3_restrict_aux {L N : MonomialState} (h : L.Sub N) : ∃ (ρ' : ℕ → ℕ) (σ' : ℕ → ℕ), (∀ c < L.nextComp, ρ' c = c) ∧ (∀ ℓ < L.nextLabel, σ' ℓ = ℓ) ∧ Rel ρ' σ' L.step3.1 (List.foldl blowUp L N.step3.2) ∧ List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) L.step3.2 = L.restrictRun N.step3.2

theorem Hironaka.Monomial.MonomialState.step3_restrict {L N : MonomialState} (h : L.Sub N) : ∃ (ρ : ℕ ↪o ℕ), (∀ c < L.nextComp, ρ c = c) ∧ ∃ (σ : ℕ ↪o ℕ), (∀ ℓ < L.nextLabel, σ ℓ = ℓ) ∧ (∀ c < L.step3.1.nextComp, (List.foldl blowUp L N.step3.2).a (ρ c) = L.step3.1.a c ∧ (List.foldl blowUp L N.step3.2).label (ρ c) = σ (L.step3.1.label c)) ∧ (List.foldl blowUp L N.step3.2).nerve = Finset.image (Finset.image ⇑ρ) L.step3.1.nerve ∧ List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ⇑ρ) S) L.step3.2 = L.restrictRun N.step3.2

Functoriality of Step 3 under restriction to a down-closed subnerve, the second clause of [Kol07, 34.1] on the state: for Sub L N there are order embeddings ρ of components and σ of labels, the identity on those of L, such that the pulled-back run on L is the direct run on L renumbered by ρ and σ, with the same nerve up to ρ, and the centres of the direct run, renumbered, are the pulled-back centres with the empty ones deleted.