Charts at a point of a centre of the monomial procedure

The nerve after the blow-up of a centre (BMO/Step3Monomial/Kernel.lean) is computed in coordinates. At a point x of the locus of a face P of the centre, this file provides a chart of simple normal crossings for the boundary family, shrunk so that every piece through x is a coordinate hyperplane {z_{κ c} = 0} (a piece is a clopen part of its member), every piece not through x misses the chart, and the centre is the coordinate subspace cut out by the coordinates of the pieces of P; the chart is then adapted to the centre with block σ the coordinates of the pieces of P (Realizes.exists_chart_of_mem_faceSet). Over such a chart the blow-up has its charts of every index i ([BM88, Definition 4.1]), and the point of the chart of index i with the same coordinates as x lies over x (IsBlowUpChart.exists_mem_source_of_mem_center): this is the point at which the intersections after the blow-up, "E^{i₁} ∩ ⋯ ∩ E^{i_{r-1}} ∩ E^{jℓ} for certain values of i" in [Kol07, 111, Step 3], are read off.

theorem Manifold.IsBlowUpChart.exists_mem_source_of_mem_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {Y : Set M} {c : ℕ} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {π : M' → M} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {x : M} (hxY : x ∈ Y) (hxφ : x ∈ φ.source) : ∃ p ∈ Φ.source, π p = x ∧ ψ (↑Φ p) = ψ (↑φ x)

Over a chart adapted to the centre, the point of the blow-up chart of index i with the same coordinates as a point x of the centre lies over x ([BM88, Definition 4.1 (2)]).

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.exists_chart_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) {P : Finset ℕ} (hP : P ∈ S) {x : N.carrier} (hxP : x ∈ Φ.faceSet P) : ∃ (φ : OpenPartialHomeomorph N.carrier E) (σ : Fin (faceCard S) ↪ Fin n) (κ : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c } → Fin n), x ∈ φ.source ∧ Manifold.IsAdaptedChart ψ₀ (Φ.centerOf S) φ σ ∧ Function.Injective κ ∧ (∀ (c : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c }), ∀ y ∈ φ.source, y ∈ Φ.piece ↑↑c ↔ ψ₀ (↑φ y) (κ c) = 0) ∧ (∀ (c : Fin Φ.nextComp), x ∉ Φ.piece ↑c → ∀ y ∈ φ.source, y ∉ Φ.piece ↑c) ∧ (∀ (c : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c }), ↑↑c ∈ P ↔ κ c ∈ Set.range ⇑σ) ∧ (∀ (k : Fin (faceCard S)), ∃ (c : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c }), ↑↑c ∈ P ∧ κ c = σ k) ∧ ∃ (cidx : { j : F.ι // x ∈ F.hyp j } → Fin n), Manifold.HypersurfaceFamily.IsSncChartAt ψ₀ F φ x cidx ∧ ∀ (c : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c }), κ c = cidx ⟨e ⟨Φ.label ↑↑c, ⋯⟩, ⋯⟩

At a point x of the locus of the face P ∈ S of a centre there is a chart φ of simple normal crossings for the boundary family ([Kol07, Definition 24]) with coordinates κ for the pieces through x, such that on the chart every piece through x is its coordinate hyperplane, every piece not through x misses the chart, the coordinates of distinct pieces through x are distinct, and the chart is adapted to the centre with block σ the coordinates of the pieces of P; κ is the index function of the chart on the members of the pieces.