Running the monomial procedure on an analytic manifold

The combinatorial model Hironaka.Monomial.MonomialState.step3 runs Kollár's monomial procedure [Kol07, 111, Step 3] on the combinatorial state and terminates. This file realises its list of centres as a list of blow-ups on the manifold (PieceFamily.realize). Each centre of the run is Kollár's choice at its level, a centre of the state, whose locus is a closed submanifold having simple normal crossings with the boundary family (BMO/Step3Monomial/Center.lean); the transformed piece family realises the transformed boundary and its state is the combinatorial blow-up (BMO/Step3Monomial/Kernel.lean, BMO/Step3Monomial/RealizesBlowUp.lean); and the marked transform of the monomial ideal is the monomial ideal of the transformed family (BMO/Step3Monomial/Transform.lean). Hence, along the whole run (realizeAux_spec): no centre is empty ([Kol07, 32]); the sequence is a smooth blow-up sequence of order ≥ m for the monomial ideal with the family's boundary ([Kol07, Definition 66 (2′)–(4′)]); and at the last stage the marked transform of the monomial ideal is the monomial ideal of a family whose state is the final state of the combinatorial run, so its order at every point is below m ("at the end of Step 3.n we are done", [Kol07, 111, Step 3]). These are realize_noEmptyCenters, realize_isOfOrderGe and realize_ord_lt.

def Hironaka.Manifold.BMO.PieceFamily.SmoothCenters {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {N : AnalyticManifold 𝕜 E} : PieceFamily N → ℕ → List (Finset (Finset ℕ)) → Prop

A list of centres has smooth loci along the run: each locus is a closed submanifold of codimension the common cardinality of its faces, the next family being the transformed one. This is the proof-carrying invariant that the construction of the list of blow-ups needs at every step.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Manifold.BMO.PieceFamily.SmoothCenters ψ₀ x✝¹ x✝ [] = True

theorem Hironaka.Manifold.BMO.PieceFamily.smoothCenters_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} : SmoothCenters ψ₀ Φ m []

theorem Hironaka.Manifold.BMO.PieceFamily.smoothCenters_cons_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {L : List (Finset (Finset ℕ))} : SmoothCenters ψ₀ Φ m (S :: L) ↔ ∃ (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)), SmoothCenters ψ₀ (Φ.blowUpPieces S m hZ) m L

theorem Hironaka.Manifold.BMO.PieceFamily.SmoothCenters.head {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {L : List (Finset (Finset ℕ))} (h : SmoothCenters ψ₀ Φ m (S :: L)) : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)

theorem Hironaka.Manifold.BMO.PieceFamily.SmoothCenters.tail {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {L : List (Finset (Finset ℕ))} (h : SmoothCenters ψ₀ Φ m (S :: L)) : SmoothCenters ψ₀ (Φ.blowUpPieces S m ⋯) m L

noncomputable def Hironaka.Manifold.BMO.PieceFamily.realizeAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (m : ℕ) (L : List (Finset (Finset ℕ))) : SmoothCenters ψ₀ Φ m L → AnalyticManifold.BlowUpSequence ψ₀ N

The realisation of a list of centres as a list of blow-ups, by structural recursion on the list, the smoothness of each centre supplied by SmoothCenters.

Equations

• Hironaka.Manifold.BMO.PieceFamily.realizeAux ψ₀ x_1 x_2 [] x_8 = AnalyticManifold.BlowUpSequence.nil x
• Hironaka.Manifold.BMO.PieceFamily.realizeAux ψ₀ x_1 x_2 (S :: L) h = AnalyticManifold.BlowUpSequence.cons ⋯ (Hironaka.Manifold.BMO.PieceFamily.realizeAux ψ₀ (x_1.blowUpPieces S x_2 ⋯) x_2 L ⋯)

theorem Hironaka.Manifold.BMO.PieceFamily.realizeAux_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} (h : SmoothCenters ψ₀ Φ m []) : realizeAux ψ₀ Φ m [] h = AnalyticManifold.BlowUpSequence.nil N

theorem Hironaka.Manifold.BMO.PieceFamily.realizeAux_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {L : List (Finset (Finset ℕ))} (h : SmoothCenters ψ₀ Φ m (S :: L)) : realizeAux ψ₀ Φ m (S :: L) h = AnalyticManifold.BlowUpSequence.cons ⋯ (realizeAux ψ₀ (Φ.blowUpPieces S m ⋯) m L ⋯)

The run of Kollár's Step 3 has smooth loci, and its realisation's postconditions

theorem Hironaka.Manifold.BMO.PieceFamily.realizeAux_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (L : List (Finset (Finset ℕ))) {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) {st' : Monomial.MonomialState} (_hrun : (Φ.toState n m hV).IsRun L st') (h : SmoothCenters ψ₀ Φ m L) : (realizeAux ψ₀ Φ m L h).NoEmptyCenters ∧ (realizeAux ψ₀ Φ m L h).toSuccession.IsOfOrderGe (Φ.monomialIdeal hF hΦ) m F.idealSheaf ∧ ∃ (Φ' : PieceFamily ((realizeAux ψ₀ Φ m L h).toSuccession.stage (Fin.last (realizeAux ψ₀ Φ m L h).toSuccession.length))) (F' : Manifold.HypersurfaceFamily ((realizeAux ψ₀ Φ m L h).toSuccession.stage (Fin.last (realizeAux ψ₀ Φ m L h).toSuccession.length)).carrier) (e' : Fin Φ'.nextLabel ↪o F'.ι) (hF' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (hΦ' : Φ'.Realizes F' e') (hV' : Φ'.IsValid n m), Φ'.toState n m hV' = st' ∧ (realizeAux ψ₀ Φ m L h).toSuccession.markedTransformSeq (Φ.monomialIdeal hF hΦ) m (Fin.last (realizeAux ψ₀ Φ m L h).toSuccession.length) = Φ'.monomialIdeal hF' hΦ'

Along a run of the combinatorial procedure from a realising family (every centre Kollár's choice at some level), the realisation has no empty centre, is a smooth blow-up sequence of order ≥ m for the monomial ideal with the family's boundary, and ends at a family realising the last boundary whose state is the final state of the run and whose monomial ideal is the last marked transform.

theorem Hironaka.Manifold.BMO.PieceFamily.smoothCenters_step3 {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) : SmoothCenters ψ₀ Φ m (Φ.toState n m hV).step3.2

The run of the combinatorial procedure from a realising family has smooth loci.

noncomputable def Hironaka.Manifold.BMO.PieceFamily.realize {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) {m : ℕ} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) : AnalyticManifold.BlowUpSequence ψ₀ N

The realisation of Kollár's monomial procedure [Kol07, 111, Step 3] on the manifold: the run of Hironaka.Monomial.MonomialState.step3 from the family's state, realised centre by centre.

Equations

• Φ.realize hF hΦ hV = Hironaka.Manifold.BMO.PieceFamily.realizeAux ψ₀ Φ m (Φ.toState n m hV).step3.2 ⋯

theorem Hironaka.Manifold.BMO.PieceFamily.realize_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) : (Φ.realize hF hΦ hV).NoEmptyCenters ∧ (Φ.realize hF hΦ hV).toSuccession.IsOfOrderGe (Φ.monomialIdeal hF hΦ) m F.idealSheaf ∧ ∃ (Φ' : PieceFamily ((Φ.realize hF hΦ hV).toSuccession.stage (Fin.last (Φ.realize hF hΦ hV).toSuccession.length))) (F' : Manifold.HypersurfaceFamily ((Φ.realize hF hΦ hV).toSuccession.stage (Fin.last (Φ.realize hF hΦ hV).toSuccession.length)).carrier) (e' : Fin Φ'.nextLabel ↪o F'.ι) (hF' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (hΦ' : Φ'.Realizes F' e') (hV' : Φ'.IsValid n m), Φ'.toState n m hV' = (Φ.toState n m hV).step3.1 ∧ (Φ.realize hF hΦ hV).toSuccession.markedTransformSeq (Φ.monomialIdeal hF hΦ) m (Fin.last (Φ.realize hF hΦ hV).toSuccession.length) = Φ'.monomialIdeal hF' hΦ'

The postconditions of the realisation, read off the run of the combinatorial procedure.

theorem Hironaka.Manifold.BMO.PieceFamily.realize_noEmptyCenters {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) : (Φ.realize hF hΦ hV).NoEmptyCenters

No centre of the realisation is empty ([Kol07, 32]).

theorem Hironaka.Manifold.BMO.PieceFamily.realize_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) : (Φ.realize hF hΦ hV).toSuccession.IsOfOrderGe (Φ.monomialIdeal hF hΦ) m F.idealSheaf

The realisation is a smooth blow-up sequence of order ≥ m for the monomial ideal with the family's boundary ([Kol07, Definition 66 (2′)–(4′)]).

theorem Hironaka.Manifold.BMO.PieceFamily.realize_ord_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hV : Φ.IsValid n m) (x : ((Φ.realize hF hΦ hV).toSuccession.stage (Fin.last (Φ.realize hF hΦ hV).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((Φ.realize hF hΦ hV).toSuccession.markedTransformSeq (Φ.monomialIdeal hF hΦ) m (Fin.last (Φ.realize hF hΦ hV).toSuccession.length)) x < ↑m

At every point of the last stage the marked transform of the monomial ideal has order < m: its order is the exponent sum of the face through the point in the final family, whose state is the final state of the combinatorial run, all of whose faces have exponent sums < m (Hironaka.Monomial.MonomialState.step3_maxOrd_lt; "at the end of Step 3.n we are done", [Kol07, 111, Step 3]).