Functoriality under refinement: the run on Y is the preimage of the run on L

Kollár's Step 3 on the monomial state commutes with refinement (Refines ρ Y L of Hironaka/Resolution/Algebraic/Monomial/Restrict.lean), the first clause of [Kol07, 34.1], commutation with smooth surjections, for the combinatorial procedure. The two runs advance in lockstep: at every step Kollár's choice on Y is the ρ-preimage of the choice on L (Refines.choice_eq of Hironaka/Resolution/Algebraic/Monomial/Restrict/Refine.lean), both are nonempty or both empty, and the extended ρ keeps Refines (Refines.blowUp). refineRun ρ' Y Ls is the preimage run, the centres of L pulled back to Y in order, each replaced by the faces of the current nerve of Y whose image lies in it, and step3_refine says the run on Y is refineRun of the run on L (read index by index through refineRun_getElem?), the run on L is the image of the run on Y, and Refines holds between the final states. Not in the sources. The geometric consequence is in Hironaka/Resolution/Algebraic/Monomial/Geometric/ChainRun.lean and Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackRun.lean.

def Hironaka.Monomial.MonomialState.refineRun (ρ : ℕ → ℕ) : MonomialState → List (Finset (Finset ℕ)) → List (Finset (Finset ℕ))

The ρ-preimage run: the centres of L pulled back to Y in order, each replaced by the faces of the current nerve of Y whose image lies in it.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Monomial.MonomialState.refineRun ρ x✝ [] = []

theorem Hironaka.Monomial.MonomialState.refineRun_nil (ρ : ℕ → ℕ) (st : MonomialState) : refineRun ρ st [] = []

theorem Hironaka.Monomial.MonomialState.refineRun_cons (ρ : ℕ → ℕ) (st : MonomialState) (S' : Finset (Finset ℕ)) (Ls : List (Finset (Finset ℕ))) : refineRun ρ st (S' :: Ls) = {Q ∈ st.nerve | Finset.image ρ Q ∈ S'} :: refineRun ρ (st.blowUp ({Q ∈ st.nerve | Finset.image ρ Q ∈ S'})) Ls

theorem Hironaka.Monomial.MonomialState.refineRun_getElem? (ρ : ℕ → ℕ) (st : MonomialState) (Ls : List (Finset (Finset ℕ))) (k : ℕ) : (refineRun ρ st Ls)[k]? = Option.map (fun (S' : Finset (Finset ℕ)) => {Q ∈ (List.foldl blowUp st (List.take k (refineRun ρ st Ls))).nerve | Finset.image ρ Q ∈ S'}) Ls[k]?

The preimage run, index by index.

theorem Hironaka.Monomial.MonomialState.nextComp_le_foldl (st : MonomialState) (Ls : List (Finset (Finset ℕ))) : st.nextComp ≤ (List.foldl blowUp st Ls).nextComp

theorem Hironaka.Monomial.MonomialState.refineRun_congr {ρ ρ' : ℕ → ℕ} (st : MonomialState) (Ls : List (Finset (Finset ℕ))) : (∀ c < (List.foldl blowUp st (refineRun ρ st Ls)).nextComp, ρ' c = ρ c) → refineRun ρ' st Ls = refineRun ρ st Ls

The preimage run depends on ρ only below the final counter of the run.

theorem Hironaka.Monomial.MonomialState.refineRun_append (ρ : ℕ → ℕ) (st : MonomialState) (L₁ L₂ : List (Finset (Finset ℕ))) : refineRun ρ st (L₁ ++ L₂) = refineRun ρ st L₁ ++ refineRun ρ (List.foldl blowUp st (refineRun ρ st L₁)) L₂

theorem Hironaka.Monomial.MonomialState.phase_fst_eq_foldl {r : ℕ} (st : MonomialState) (hs : ∀ s < r, st.Star s) : (phase r st hs).1 = List.foldl blowUp st (phase r st hs).2

The final state of a phase is the fold of its centres.

The lockstep induction

theorem Hironaka.Monomial.MonomialState.phase_refine (r : ℕ) (L : MonomialState) (hsL : ∀ s < r, L.Star s) (Y : MonomialState) (ρ : ℕ → ℕ) : Refines ρ Y L → ∀ (hsY : ∀ s < r, Y.Star s), ∃ (ρ' : ℕ → ℕ), (∀ c < Y.nextComp, ρ' c = ρ c) ∧ Refines ρ' (phase r Y hsY).1 (phase r L hsL).1 ∧ (phase r L hsL).2 = List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) (phase r Y hsY).2 ∧ (phase r Y hsY).2 = refineRun ρ' Y (phase r L hsL).2

theorem Hironaka.Monomial.MonomialState.phases_refine (k r : ℕ) (L : MonomialState) (hsL : ∀ s < r, L.Star s) (Y : MonomialState) (ρ : ℕ → ℕ) : Refines ρ Y L → ∀ (hsY : ∀ s < r, Y.Star s), ∃ (ρ' : ℕ → ℕ), (∀ c < Y.nextComp, ρ' c = ρ c) ∧ Refines ρ' (phases k r Y hsY).1 (phases k r L hsL).1 ∧ (phases k r L hsL).2 = List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) (phases k r Y hsY).2 ∧ (phases k r Y hsY).2 = refineRun ρ' Y (phases k r L hsL).2

theorem Hironaka.Monomial.MonomialState.step3_refine_aux {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) : ∃ (ρ' : ℕ → ℕ), (∀ c < Y.nextComp, ρ' c = ρ c) ∧ Refines ρ' Y.step3.1 L.step3.1 ∧ L.step3.2 = List.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) Y.step3.2 ∧ Y.step3.2 = refineRun ρ' Y L.step3.2

theorem Hironaka.Monomial.MonomialState.step3_refine {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) : ∃ (ρ' : ℕ → ℕ), (∀ c < Y.nextComp, ρ' c = ρ c) ∧ Refines ρ' Y.step3.1 L.step3.1 ∧ (∀ (k : ℕ), L.step3.2[k]? = Option.map (fun (S : Finset (Finset ℕ)) => Finset.image (Finset.image ρ') S) Y.step3.2[k]?) ∧ ∀ (k : ℕ), Y.step3.2[k]? = Option.map (fun (S' : Finset (Finset ℕ)) => {Q ∈ (List.foldl blowUp Y (List.take k Y.step3.2)).nerve | Finset.image ρ' Q ∈ S'}) L.step3.2[k]?

Functoriality of Step 3 under refinement, the first clause of [Kol07, 34.1] on the state: the run on Y is the ρ-preimage of the run on L, with ρ extended to the new components and Refines between the final states.