The monomial phase at the mark 1, by recursion

The monomial phase of the modified algorithm [Wlo09, Theorem 7.4.1] resolves (M(𝓘), 1) by the sequence of blow-ups of [Wlo09, §6, Step 2b] at µ = 1: while some member carries a component of positive exponent, blow up the positive locus of the latest-born such member (Step2bCenter.lean) and carry the triple along (Step2bStep.lean). This module defines the sequence by recursion on a fuel k: step2bPhase k T hT is the list of the first k steps, stopping early (the empty list) once no member is active, and proves the properties which hold for every fuel: no empty centre ([Kol07, 32]; the centre is nonempty by construction), the order clause of [Kol07, Definition 66] at the mark 1, the length bound and the recursion equations. The fuel is a device of the definition: the termination of the phase, i.e. that the fuel Σ_D a_D over the components exhausts the active members (the invariant of [Wlo09, §6, Step 2b] decreases), is the theorem step2bPhase_eq_of_step2bMeasure_le of Step2bMeasure.lean, and the value on a relatively compact open is read at that fuel (Step2bFamily.lean).

The rule is intrinsic (the latest-born active member, in the order of birth along the total transforms), so the phase is canonical.

def Hironaka.Manifold.BMOmod.step2bPhase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} : ℕ → {M : AnalyticManifold 𝕜 E} → (T : Manifold.AnalyticTriple ψ₀ M) → Manifold.AnalyticTriple.BMOClass 1 T → AnalyticManifold.BlowUpSequence ψ₀ M

The first k steps of the monomial phase at the mark 1 ("blow-ups at exceptional divisors for which ρ(x) is maximal", [Wlo09, Theorem 7.4.1]): while a member is active, blow up the centre of Step2bCenter.lean and continue on the triple after the step; the empty list when no member is active or the fuel is spent.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Manifold.BMOmod.step2bPhase 0 x_1 x_2 = AnalyticManifold.BlowUpSequence.nil x

The recursion equations

theorem Hironaka.Manifold.BMOmod.step2bPhase_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : step2bPhase 0 T hT = AnalyticManifold.BlowUpSequence.nil M

theorem Hironaka.Manifold.BMOmod.step2bPhase_succ_of_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (k : ℕ) (hne : (activeMembers T).Nonempty) : step2bPhase (k + 1) T hT = AnalyticManifold.BlowUpSequence.cons ⋯ (step2bPhase k (stepTriple T ⋯ hne) ⋯)

theorem Hironaka.Manifold.BMOmod.step2bPhase_succ_of_not_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (k : ℕ) (hne : ¬(activeMembers T).Nonempty) : step2bPhase (k + 1) T hT = AnalyticManifold.BlowUpSequence.nil M

theorem Hironaka.Manifold.BMOmod.step2bPhase_of_not_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hne : ¬(activeMembers T).Nonempty) (k : ℕ) : step2bPhase k T hT = AnalyticManifold.BlowUpSequence.nil M

With no active member the phase is empty at every fuel (the purely nonmonomial case I′ = N(I′) of [Wlo09, Theorem 7.4.1] has been reached).

The clauses at every fuel

theorem Hironaka.Manifold.BMOmod.noEmptyCenters_step2bPhase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : (step2bPhase k T hT).NoEmptyCenters

The phase has no empty centre [Kol07, 32]: every centre is the positive locus of an active member (step2bCenter_nonempty).

theorem Hironaka.Manifold.BMOmod.isOfOrderGe_step2bPhase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : (step2bPhase k T hT).toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf

The order clause of [Kol07, Definition 66] at the mark 1: the phase is of order ≥ 1 for (M, 𝓘, E). The two head clauses of each step hold at its centre (isOfOrderGe_cons_step_iff).

theorem Hironaka.Manifold.BMOmod.length_step2bPhase_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : (step2bPhase k T hT).length ≤ k

The phase at fuel k has at most k steps.