The run of a refining state as an explicit chain

step3_refine of Hironaka/Resolution/Algebraic/Monomial/Restrict/RefinePhase.lean describes the run of Step 3 on a refining state Y as the ρ'-preimage run of the run on L, for some extension ρ' of the parent map to the new components. The geometric fold of Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackRun.lean needs the extension explicitly, the new component of a face Q of Y's centre being the child of the new component of ρ(Q), so this module re-runs the lockstep induction with the parent map carried as the explicit chain of extendComps (Hironaka/Resolution/Algebraic/Monomial/Restrict/Extend.lean):

• chainRun ρ Y L Ns: the run on Y induced by the run Ns on L. Each centre of L is replaced by the faces of the current nerve of Y mapping into it, and the parent map is extended by extendComp at each step;
• chainMap, chainStateY: the parent map and the state of Y after the chain;
• phase_chain, phases_chain, step3_chain: the run of Step 3 on Y is the chain run of the run on L, with Refines between the final states along the chain map.

The proofs are those of phase_refine and phases_refine with the stronger conclusion. Not in the sources; bookkeeping for the first clause of [Kol07, 34.1].

The chain run

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

The run on Y induced by a run on L along the parent map ρ: each centre S of L is replaced by the faces of the current nerve of Y mapping into S, and the parent map is extended across the blow-up by extendComp.

Equations

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

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

The parent map after the chain.

Equations

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

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

The state of Y after the chain.

Equations

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

theorem Hironaka.Monomial.MonomialState.chainRun_nil (ρ : ℕ → ℕ) (Y L : MonomialState) : chainRun ρ Y L [] = []

theorem Hironaka.Monomial.MonomialState.chainRun_cons (ρ : ℕ → ℕ) (Y L : MonomialState) (S : Finset (Finset ℕ)) (Ns : List (Finset (Finset ℕ))) : chainRun ρ Y L (S :: Ns) = {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} :: chainRun (extendComp ρ Y L ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (L.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainMap_nil (ρ : ℕ → ℕ) (Y L : MonomialState) : chainMap ρ Y L [] = ρ

theorem Hironaka.Monomial.MonomialState.chainMap_cons (ρ : ℕ → ℕ) (Y L : MonomialState) (S : Finset (Finset ℕ)) (Ns : List (Finset (Finset ℕ))) : chainMap ρ Y L (S :: Ns) = chainMap (extendComp ρ Y L ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (L.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainStateY_nil (ρ : ℕ → ℕ) (Y L : MonomialState) : chainStateY ρ Y L [] = Y

theorem Hironaka.Monomial.MonomialState.chainStateY_cons (ρ : ℕ → ℕ) (Y L : MonomialState) (S : Finset (Finset ℕ)) (Ns : List (Finset (Finset ℕ))) : chainStateY ρ Y L (S :: Ns) = chainStateY (extendComp ρ Y L ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (L.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainStateY_eq_foldl (ρ : ℕ → ℕ) (Y L : MonomialState) (Ns : List (Finset (Finset ℕ))) : chainStateY ρ Y L Ns = List.foldl blowUp Y (chainRun ρ Y L Ns)

The state after the chain is the fold of the chain run.

theorem Hironaka.Monomial.MonomialState.chainRun_append (ρ : ℕ → ℕ) (Y L : MonomialState) (N₁ N₂ : List (Finset (Finset ℕ))) : chainRun ρ Y L (N₁ ++ N₂) = chainRun ρ Y L N₁ ++ chainRun (chainMap ρ Y L N₁) (chainStateY ρ Y L N₁) (List.foldl blowUp L N₁) N₂

The chain along a concatenation.

theorem Hironaka.Monomial.MonomialState.chainMap_append (ρ : ℕ → ℕ) (Y L : MonomialState) (N₁ N₂ : List (Finset (Finset ℕ))) : chainMap ρ Y L (N₁ ++ N₂) = chainMap (chainMap ρ Y L N₁) (chainStateY ρ Y L N₁) (List.foldl blowUp L N₁) N₂

theorem Hironaka.Monomial.MonomialState.chainStateY_append (ρ : ℕ → ℕ) (Y L : MonomialState) (N₁ N₂ : List (Finset (Finset ℕ))) : chainStateY ρ Y L (N₁ ++ N₂) = chainStateY (chainMap ρ Y L N₁) (chainStateY ρ Y L N₁) (List.foldl blowUp L N₁) N₂

The lockstep, with the chain

theorem Hironaka.Monomial.MonomialState.phase_chain (r : ℕ) (L : MonomialState) (hsL : ∀ s < r, L.Star s) (Y : MonomialState) (ρ : ℕ → ℕ) : Refines ρ Y L → ∀ (hsY : ∀ s < r, Y.Star s), Refines (chainMap ρ Y L (phase r L hsL).2) (phase r Y hsY).1 (phase r L hsL).1 ∧ (phase r Y hsY).2 = chainRun ρ Y L (phase r L hsL).2 ∧ (phase r Y hsY).1 = chainStateY ρ Y L (phase r L hsL).2

phase_refine with the explicit chain: the phase-r run on Y is the chain run of the phase-r run on L, and the final states refine along the chain map.

theorem Hironaka.Monomial.MonomialState.phases_chain (k r : ℕ) (L : MonomialState) (hsL : ∀ s < r, L.Star s) (Y : MonomialState) (ρ : ℕ → ℕ) : Refines ρ Y L → ∀ (hsY : ∀ s < r, Y.Star s), Refines (chainMap ρ Y L (phases k r L hsL).2) (phases k r Y hsY).1 (phases k r L hsL).1 ∧ (phases k r Y hsY).2 = chainRun ρ Y L (phases k r L hsL).2 ∧ (phases k r Y hsY).1 = chainStateY ρ Y L (phases k r L hsL).2

phases_refine with the explicit chain.

theorem Hironaka.Monomial.MonomialState.step3_chain {ρ : ℕ → ℕ} {Y L : MonomialState} (h : Refines ρ Y L) : Refines (chainMap ρ Y L L.step3.2) Y.step3.1 L.step3.1 ∧ Y.step3.2 = chainRun ρ Y L L.step3.2 ∧ Y.step3.1 = chainStateY ρ Y L L.step3.2

The run of Step 3 on a refining state Y is the chain run of the run of Step 3 on L, and the final states refine along the chain map.