The run of a partially refining state as an explicit chain with skips

The second clause of [Kol07, 34.1] compares the run of Step 3 on Y with the run on X when h : Y ⟶ X is not surjective: a centre of X none of whose faces has a face of Y over it is an empty blow-up of Y and is skipped. The combinatorial modules describe this in two steps: step3_restrict of Hironaka/Resolution/Algebraic/Monomial/Restrict/Phase.lean (the run on the restricted state D is the run on X with the empty steps deleted and the surviving centres filtered, up to a renumbering Rel ρ' σ' D P against a state P that is Sub the state of X with the same counters) and step3_refine of Hironaka/Resolution/Algebraic/Monomial/Restrict/RefinePhase.lean (the run on Y is the ρ-preimage run of the run on D). The geometric fold of Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackErase.lean needs the composite parent map Y → X explicitly at every stage, so this module re-runs both lockstep inductions at once, with the explicit chain:

• chainRunE ρ Y N Ns: the run on Y induced by the run Ns on N along ρ, with the empty steps skipped; chainMapE, chainStateYE the parent map and the state of Y after the chain;
• IsChainE ρ Y N Ns: the run Ns on N is a chain run for (ρ, Y), every step being a skip (no face of Y over the centre) or a blow-up of Y along the faces over the centre, a centre of Y;
• phase_chainE, phases_chainE, step3_chainE: the run of Step 3 on Y is the chain run with skips of the run of Step 3 on N, given Refines ρ_Y Y D, Rel ρ' σ' D P, Sub P N with ρ = ρ' ∘ ρ_Y on the components of Y.

The proofs are phase_restrict and phase_chain (Hironaka/Resolution/Algebraic/Monomial/Geometric/ChainRun.lean) run side by side. Not in the sources; bookkeeping for the deletion of empty blow-ups of [Kol07, 32] and [Kol07, 34.1].

The chain run with skips

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

The run on Y induced by a run on N along the parent map ρ, with the empty steps deleted: a centre S of N with no face of Y over it is skipped (Y unchanged, N blown up); otherwise the faces of Y over S are blown up and the parent map extended by extendComp.

Equations

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

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

The parent map after the chain with skips.

Equations

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

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

The state of Y after the chain with skips.

Equations

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

theorem Hironaka.Monomial.MonomialState.chainRunE_nil (ρ : ℕ → ℕ) (Y N : MonomialState) : chainRunE ρ Y N [] = []

theorem Hironaka.Monomial.MonomialState.chainRunE_cons_of_eq_empty (ρ : ℕ → ℕ) (Y N : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} = ∅) : chainRunE ρ Y N (S :: Ns) = chainRunE ρ Y (N.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainRunE_cons_of_ne_empty (ρ : ℕ → ℕ) (Y N : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} ≠ ∅) : chainRunE ρ Y N (S :: Ns) = {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} :: chainRunE (extendComp ρ Y N ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (N.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainMapE_nil (ρ : ℕ → ℕ) (Y N : MonomialState) : chainMapE ρ Y N [] = ρ

theorem Hironaka.Monomial.MonomialState.chainMapE_cons_of_eq_empty (ρ : ℕ → ℕ) (Y N : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} = ∅) : chainMapE ρ Y N (S :: Ns) = chainMapE ρ Y (N.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainMapE_cons_of_ne_empty (ρ : ℕ → ℕ) (Y N : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} ≠ ∅) : chainMapE ρ Y N (S :: Ns) = chainMapE (extendComp ρ Y N ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (N.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainStateYE_nil (ρ : ℕ → ℕ) (Y N : MonomialState) : chainStateYE ρ Y N [] = Y

theorem Hironaka.Monomial.MonomialState.chainStateYE_cons_of_eq_empty (ρ : ℕ → ℕ) (Y N : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} = ∅) : chainStateYE ρ Y N (S :: Ns) = chainStateYE ρ Y (N.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainStateYE_cons_of_ne_empty (ρ : ℕ → ℕ) (Y N : MonomialState) {S : Finset (Finset ℕ)} (Ns : List (Finset (Finset ℕ))) (h : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} ≠ ∅) : chainStateYE ρ Y N (S :: Ns) = chainStateYE (extendComp ρ Y N ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (N.blowUp S) Ns

theorem Hironaka.Monomial.MonomialState.chainRunE_append (ρ : ℕ → ℕ) (Y N : MonomialState) (N₁ N₂ : List (Finset (Finset ℕ))) : chainRunE ρ Y N (N₁ ++ N₂) = chainRunE ρ Y N N₁ ++ chainRunE (chainMapE ρ Y N N₁) (chainStateYE ρ Y N N₁) (List.foldl blowUp N N₁) N₂

The chain with skips along a concatenation.

theorem Hironaka.Monomial.MonomialState.chainMapE_append (ρ : ℕ → ℕ) (Y N : MonomialState) (N₁ N₂ : List (Finset (Finset ℕ))) : chainMapE ρ Y N (N₁ ++ N₂) = chainMapE (chainMapE ρ Y N N₁) (chainStateYE ρ Y N N₁) (List.foldl blowUp N N₁) N₂

theorem Hironaka.Monomial.MonomialState.chainStateYE_append (ρ : ℕ → ℕ) (Y N : MonomialState) (N₁ N₂ : List (Finset (Finset ℕ))) : chainStateYE ρ Y N (N₁ ++ N₂) = chainStateYE (chainMapE ρ Y N N₁) (chainStateYE ρ Y N N₁) (List.foldl blowUp N N₁) N₂

The chain predicate

inductive Hironaka.Monomial.MonomialState.IsChainE : (ℕ → ℕ) → MonomialState → MonomialState → List (Finset (Finset ℕ)) → Prop

The run Ns on N is a chain run with skips for (ρ, Y): every step is a skip (no face of Y over the centre, Y unchanged) or a blow-up of Y along the (nonempty) set of faces over the centre, which is a centre of Y, with the parent map extended. The geometric fold consumes exactly these facts.

• nil (ρ : ℕ → ℕ) (Y N : MonomialState) : IsChainE ρ Y N []
• skip {ρ : ℕ → ℕ} {Y N : MonomialState} (S : Finset (Finset ℕ)) {Ns : List (Finset (Finset ℕ))} (hno : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S} = ∅) (hnext : IsChainE ρ Y (N.blowUp S) Ns) : IsChainE ρ Y N (S :: Ns)
• step {ρ : ℕ → ℕ} {Y N : MonomialState} (S : Finset (Finset ℕ)) {Ns : List (Finset (Finset ℕ))} (hne : {Q ∈ Y.nerve | Finset.image ρ Q ∈ S}.Nonempty) (hY : Y.IsCenter ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (hnext : IsChainE (extendComp ρ Y N ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S}) S) (Y.blowUp ({Q ∈ Y.nerve | Finset.image ρ Q ∈ S})) (N.blowUp S) Ns) : IsChainE ρ Y N (S :: Ns)

theorem Hironaka.Monomial.MonomialState.IsChainE.append {ρ : ℕ → ℕ} {Y N : MonomialState} {N₁ N₂ : List (Finset (Finset ℕ))} (h₁ : IsChainE ρ Y N N₁) (h₂ : IsChainE (chainMapE ρ Y N N₁) (chainStateYE ρ Y N N₁) (List.foldl blowUp N N₁) N₂) : IsChainE ρ Y N (N₁ ++ N₂)

A renumbering is injective on the faces

theorem Hironaka.Monomial.MonomialState.Rel.image_mem_image_iff {ρ σ : ℕ → ℕ} {D P : MonomialState} (h : Rel ρ σ D P) {T : Finset ℕ} (hT : ∀ c ∈ T, c < D.nextComp) {A : Finset (Finset ℕ)} (hA : A ⊆ D.nerve) : Finset.image ρ T ∈ Finset.image (Finset.image ρ) A ↔ T ∈ A

The image under a renumbering of a face of D lies in the image of a family of faces of D iff the face does (the renumbering is injective on the components of D).

The lockstep with skips

theorem Hironaka.Monomial.MonomialState.phase_chainE (r : ℕ) (N : MonomialState) (hsN : ∀ s < r, N.Star s) (Y D P : MonomialState) (ρY ρ' σ' ρ : ℕ → ℕ) : Refines ρY Y D → Rel ρ' σ' D P → P.Sub N → (∀ c < Y.nextComp, ρ c = ρ' (ρY c)) → ∀ (hsD : ∀ s < r, D.Star s) (hsY : ∀ s < r, Y.Star s), ∃ (ρY' : ℕ → ℕ) (ρ'' : ℕ → ℕ) (σ'' : ℕ → ℕ), Refines ρY' (phase r Y hsY).1 (phase r D hsD).1 ∧ 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 ∧ (∀ c < (phase r Y hsY).1.nextComp, chainMapE ρ Y N (phase r N hsN).2 c = ρ'' (ρY' c)) ∧ IsChainE ρ Y N (phase r N hsN).2 ∧ (phase r Y hsY).2 = chainRunE ρ Y N (phase r N hsN).2 ∧ (phase r Y hsY).1 = chainStateYE ρ Y N (phase r N hsN).2

phase_restrict and phase_chain together, with the explicit chain with skips: along the phase-r run of N, the restricted state D and the state Y refining it advance exactly at the centres with a face of Y over them; the phase-r run of Y is the chain run with skips, and the composite parent map Y → N is the chain map.

theorem Hironaka.Monomial.MonomialState.phases_chainE (k r : ℕ) (N : MonomialState) (hsN : ∀ s < r, N.Star s) (Y D P : MonomialState) (ρY ρ' σ' ρ : ℕ → ℕ) : Refines ρY Y D → Rel ρ' σ' D P → P.Sub N → (∀ c < Y.nextComp, ρ c = ρ' (ρY c)) → ∀ (hsD : ∀ s < r, D.Star s) (hsY : ∀ s < r, Y.Star s), ∃ (ρY' : ℕ → ℕ) (ρ'' : ℕ → ℕ) (σ'' : ℕ → ℕ), Refines ρY' (phases k r Y hsY).1 (phases k r D hsD).1 ∧ 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 ∧ (∀ c < (phases k r Y hsY).1.nextComp, chainMapE ρ Y N (phases k r N hsN).2 c = ρ'' (ρY' c)) ∧ IsChainE ρ Y N (phases k r N hsN).2 ∧ (phases k r Y hsY).2 = chainRunE ρ Y N (phases k r N hsN).2 ∧ (phases k r Y hsY).1 = chainStateYE ρ Y N (phases k r N hsN).2

The phases, with the chain with skips.

theorem Hironaka.Monomial.MonomialState.step3_chainE {Y D P N : MonomialState} {ρY ρ' σ' ρ : ℕ → ℕ} (hrefY : Refines ρY Y D) (hrel : Rel ρ' σ' D P) (hsub : P.Sub N) (hρ : ∀ c < Y.nextComp, ρ c = ρ' (ρY c)) : IsChainE ρ Y N N.step3.2 ∧ Y.step3.2 = chainRunE ρ Y N N.step3.2

The run of Step 3 on Y is the chain run with skips of the run of Step 3 on N: for Y refining the restricted state D (Refines ρ_Y Y D), D renumbered against P (Rel ρ' σ' D P), P a sub-state of N (Sub P N), and ρ = ρ' ∘ ρ_Y on the components of Y.