The nerve after the blow-up of a centre

Kollár describes the intersections after a blow-up of the monomial procedure as "E^{i₁} ∩ ⋯ ∩ E^{i_{r-1}} ∩ E^{jℓ} for certain values of i" [Kol07, 111, Step 3]. The combinatorial model Hironaka.Monomial.MonomialState makes the rule exact (MonomialState.blowUpNerve) and proves the procedure on it; this file proves that the rule holds on an analytic manifold, so that the nerve of the piece family after the blow-up of a centre of the state is the combinatorial one (Realizes.nerve_blowUpPieces). Consequently the transported family satisfies the invariants of the state (valid_blowUpPieces) and its state is the combinatorial blow-up of the state (toState_blowUpPieces), which is how the run, its termination and its postconditions, proved on the combinatorial model, transfer to the analytic run.

The rule consists of three facts about the loci, read in the blow-up charts over the chart of BMO/Step3Monomial/Chart.lean at a point x of the centre:

• the strict transforms of the pieces of a face of the centre have no common point (faceSet_blowUpPieces_of_mem): at a point over x in the blow-up chart of index i, the strict transform of the piece whose coordinate is the scaling coordinate σ i misses the chart;
• a set of old pieces has a common point after the blow-up if and only if it had one before and contains no face of the centre (faceSet_blowUpPieces_nonempty_iff): off the centre the blow-up is an isomorphism, and over a point of the centre in the locus of P₀, a piece c₀ ∈ P₀ outside the set gives a chart whose origin lies on the strict transforms of all the other pieces through x;
• the new piece of a face P together with old pieces T₁ has a common point if and only if T₁ ∪ P had one and P ⊄ T₁ (faceSet_blowUpPieces_insert_newComp_nonempty_iff), by the same origin.

Points of the new pieces

theorem Hironaka.Manifold.BMO.PieceFamily.mem_blowUpPieces_piece_of_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} (hc : Φ.nextComp ≤ c) {p : (Manifold.blowUp ψ₀ hZ).carrier} : p ∈ (Φ.blowUpPieces S m hZ).piece c ↔ ∃ P ∈ S, Φ.newComp S P = c ∧ (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.faceSet P

A point of a new piece lies over the locus of the unique face of the centre allocated to that piece.

theorem Hironaka.Manifold.BMO.PieceFamily.π_mem_piece_of_mem_blowUpPieces_piece {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : ℕ} (hc : c < Φ.nextComp) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hp : p ∈ (Φ.blowUpPieces S m hZ).piece c) : (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.piece c

The blow-down of a point of the strict transform of an old piece lies on the piece.

theorem Hironaka.Manifold.BMO.PieceFamily.π_mem_faceSet_of_mem_faceSet_blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {T : Finset ℕ} (hT : ∀ c ∈ T, c < Φ.nextComp) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hp : p ∈ (Φ.blowUpPieces S m hZ).faceSet T) : (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.faceSet T

The blow-down of a common point of the strict transforms of old pieces is a common point of the pieces.

The origin of the chart of a piece of the face

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.exists_origin_of_mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {P : Finset ℕ} (hP : P ∈ S) {x : N.carrier} (hxP : x ∈ Φ.faceSet P) {c₀ : ℕ} (hc₀ : c₀ ∈ P) : ∃ (p : (Manifold.blowUp ψ₀ hZ).carrier), (Manifold.blowUpπ ψ₀ hZ) p = x ∧ (∀ c < Φ.nextComp, c ≠ c₀ → x ∈ Φ.piece c → p ∈ (Φ.blowUpPieces S m hZ).piece c) ∧ p ∉ (Φ.blowUpPieces S m hZ).piece c₀

Kollár's coordinates at a point x of the locus of P ∈ S, in the blow-up chart of index σ i = κ c₀ for a piece c₀ ∈ P: the origin p of that chart over x lies on the strict transform of every old piece through x other than c₀, and not on that of c₀.

The three set facts

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.faceSet_blowUpPieces_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {P : Finset ℕ} (hP : P ∈ S) : (Φ.blowUpPieces S m hZ).faceSet P = ∅

The strict transforms of the pieces of a face of the centre have no common point: at a point over x in a blow-up chart of index i, the strict transform of the piece whose coordinate is the scaling coordinate σ i misses the chart.

theorem Hironaka.Manifold.BMO.PieceFamily.exists_mem_faceSet_blowUpPieces_of_notMem_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {T : Finset ℕ} (hT : ∀ c ∈ T, c < Φ.nextComp) {x : N.carrier} (hxT : x ∈ Φ.faceSet T) (hxZ : x ∉ Φ.centerOf S) : ∃ (p : (Manifold.blowUp ψ₀ hZ).carrier), (Manifold.blowUpπ ψ₀ hZ) p = x ∧ p ∈ (Φ.blowUpPieces S m hZ).faceSet T

Off the centre the blow-down is onto and the strict transform of a piece is its preimage, so a common point of old pieces off the centre lifts to a common point of their strict transforms.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.faceSet_blowUpPieces_nonempty_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {T : Finset ℕ} (hT : ∀ c ∈ T, c < Φ.nextComp) : ((Φ.blowUpPieces S m hZ).faceSet T).Nonempty ↔ (Φ.faceSet T).Nonempty ∧ ∀ P ∈ S, ¬P ⊆ T

A set of old pieces has a common point after the blow-up if and only if it had one before and contains no face of the centre.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.faceSet_blowUpPieces_insert_newComp_nonempty_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {P : Finset ℕ} (hP : P ∈ S) {T₁ : Finset ℕ} (hT₁ : ∀ c ∈ T₁, c < Φ.nextComp) : ((Φ.blowUpPieces S m hZ).faceSet (insert (Φ.newComp S P) T₁)).Nonempty ↔ (Φ.faceSet (T₁ ∪ P)).Nonempty ∧ ¬P ⊆ T₁

The new piece of the face P together with old pieces T₁ has a common point if and only if T₁ ∪ P had one and P ⊄ T₁. These are the intersections E^{i₁} ∩ ⋯ ∩ E^{i_{r-1}} ∩ E^{jℓ} after a blow-up in [Kol07, 111, Step 3].

The nerve rule

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.nerve_blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) : (Φ.blowUpPieces S m hZ).nerve = Monomial.MonomialState.blowUpNerve Φ.nerve S (Φ.newComp S)

The nerve after the blow-up of a centre of the state is the combinatorial nerve Hironaka.Monomial.MonomialState.blowUpNerve of the nerve: a face of the new family contains at most one new piece (two new pieces lie over disjoint loci), and the two preceding lemmas identify the faces without and with a new piece.

The transported family is valid and its state is the transition

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.valid_blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) : (Φ.blowUpPieces S m hZ).IsValid n m

The family after the blow-up satisfies the invariants of the state: its data are those of the combinatorial blow-up of the state, whose invariants are proved on the combinatorial model.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.toState_blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) (hV' : (Φ.blowUpPieces S m hZ).IsValid n m) : (Φ.blowUpPieces S m hZ).toState n m hV' = (Φ.toState n m hV).blowUp S

The state of the family after the blow-up is the combinatorial blow-up of the state.