A refinement persists across the blow-up of a centre

The run of the monomial procedure on a piece family Ψ refining a piece family Φ along a local analytic isomorphism ρ is compared with the run on Φ one step at a time (BMO/Step3Monomial/RealizePullback.lean). This file proves the step in which Φ blows up a centre S some of whose faces have preimages: Ψ blows up the faces mapping into S (preimageFaces), and the two transformed families again refine one another along any local analytic isomorphism ℓ between the two blow-ups lying over ρ (RefinesAlong.blowUpPieces). The parent map is extended so that the new piece of a face Q of Ψ goes to the new piece of its image Q.image p (extendParent), and the label map sends the new label to the new label (extendLabel). The strict transforms of the old pieces correspond because the square commutes; the new pieces of Ψ over a face P of S are the preimages of the loci of the faces of Ψ over P, whose union is the preimage of the locus of P (preimage_faceSet); and two faces of Ψ over one face of Φ with a common point coincide (eq_of_image_eq_of_mem), so the new children are disjoint. The other case of the step, a centre none of whose faces has a preimage, is RefinesAlong.of_empty_step in BMO/Step3Monomial/RealizePullback.lean.

The bookkeeping of the new pieces uses the rank of a face in the centre (Hironaka.Monomial.MonomialState.rank): every index in [nextComp, nextComp + |S|) is the new piece of exactly one face. Two general facts on strict transforms, of a finite union and of disjoint closed sets, sit here beside their use.

Bookkeeping of the new pieces

theorem Hironaka.Manifold.BMO.PieceFamily.exists_newComp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) {c : ℕ} (h1 : Φ.nextComp ≤ c) (h2 : c < Φ.nextComp + S.card) : ∃ P ∈ S, Φ.newComp S P = c

Every index in [nextComp, nextComp + |S|) is the new piece of exactly one face of S: the rank is a bijection of S onto range |S|.

theorem Hironaka.Manifold.BMO.PieceFamily.newComp_lt' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) {P : Finset ℕ} (hP : P ∈ S) : Φ.newComp S P < Φ.nextComp + S.card

The new piece of a face of S has index below nextComp + |S|.

theorem Hironaka.Manifold.BMO.PieceFamily.nextComp_le_newComp' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) (P : Finset ℕ) : Φ.nextComp ≤ Φ.newComp S P

The new piece of a face has index at least nextComp.

theorem Hironaka.Manifold.BMO.PieceFamily.newComp_injOn' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} (Φ : PieceFamily N) (S : Finset (Finset ℕ)) {P Q : Finset ℕ} (hP : P ∈ S) (hQ : Q ∈ S) (h : Φ.newComp S P = Φ.newComp S Q) : P = Q

Distinct faces of S get distinct new pieces.

General facts on strict transforms

theorem Hironaka.Manifold.BMO.strictTransformSet_biUnion_finset {A B : Type u} [TopologicalSpace B] {π : B → A} (Z : Set A) {ι : Type u_2} (s : Finset ι) (H : ι → Set A) : Manifold.strictTransformSet π Z (⋃ i ∈ s, H i) = ⋃ i ∈ s, Manifold.strictTransformSet π Z (H i)

The strict transform of a finite union is the union of the strict transforms.

theorem Hironaka.Manifold.BMO.strictTransformSet_disjoint {A B : Type u} [TopologicalSpace A] [TopologicalSpace B] {π : B → A} (Z : Set A) (hπ : Continuous π) {H₁ H₂ : Set A} (h₁ : IsClosed H₁) (h₂ : IsClosed H₂) (hd : Disjoint H₁ H₂) : Disjoint (Manifold.strictTransformSet π Z H₁) (Manifold.strictTransformSet π Z H₂)

Strict transforms of disjoint closed sets are disjoint.

noncomputable def Hironaka.Manifold.BMO.PieceFamily.extendParent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (Φ : PieceFamily Y) (p : ℕ → ℕ) (S' S : Finset (Finset ℕ)) (c : ℕ) : ℕ

The parent map extended to the new pieces: the new piece of a face Q of Ψ goes to the new piece of its image Q.image p.

Equations

• Ψ.extendParent Φ p S' S c = if c < Ψ.nextComp then p c else {Q ∈ S' | Ψ.newComp S' Q = c}.sup fun (Q : Finset ℕ) => Φ.newComp S (Finset.image p Q)

def Hironaka.Manifold.BMO.PieceFamily.extendLabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (Φ : PieceFamily Y) (σ : ℕ → ℕ) (ℓ : ℕ) : ℕ

The label map extended by the new label: the new label of Ψ goes to the new label of Φ.

Equations

• Ψ.extendLabel Φ σ ℓ = if ℓ < Ψ.nextLabel then σ ℓ else Φ.nextLabel

noncomputable def Hironaka.Manifold.BMO.PieceFamily.preimageFaces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (p : ℕ → ℕ) (S : Finset (Finset ℕ)) : Finset (Finset ℕ)

The faces of Ψ mapping into the centre S of Φ.

Equations

• Ψ.preimageFaces p S = {Q ∈ Ψ.nerve | Finset.image p Q ∈ S}

theorem Hironaka.Manifold.BMO.PieceFamily.mem_preimageFaces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {p : ℕ → ℕ} {S : Finset (Finset ℕ)} {Q : Finset ℕ} : Q ∈ Ψ.preimageFaces p S ↔ Q ∈ Ψ.nerve ∧ Finset.image p Q ∈ S

theorem Hironaka.Manifold.BMO.PieceFamily.extendParent_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {p : ℕ → ℕ} (S' S : Finset (Finset ℕ)) {c : ℕ} (hc : c < Ψ.nextComp) : Ψ.extendParent Φ p S' S c = p c

theorem Hironaka.Manifold.BMO.PieceFamily.extendParent_newComp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {p : ℕ → ℕ} (S' S : Finset (Finset ℕ)) {Q : Finset ℕ} (hQ : Q ∈ S') : Ψ.extendParent Φ p S' S (Ψ.newComp S' Q) = Φ.newComp S (Finset.image p Q)

theorem Hironaka.Manifold.BMO.PieceFamily.extendLabel_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {σ : ℕ → ℕ} {ℓ : ℕ} (hℓ : ℓ < Ψ.nextLabel) : Ψ.extendLabel Φ σ ℓ = σ ℓ

theorem Hironaka.Manifold.BMO.PieceFamily.extendLabel_nextLabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {σ : ℕ → ℕ} : Ψ.extendLabel Φ σ Ψ.nextLabel = Φ.nextLabel

theorem Hironaka.Manifold.AnalyticMap.surjective_castDom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U U' N : AnalyticManifold 𝕜 E} (e : U = U') {f : AnalyticMap U' N} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(castDom e f)

Transporting an analytic map along an equality of its domain keeps surjectivity.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.total_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {Q : Finset ℕ} (hQ : Q ∈ Ψ.nerve) : Φ.total (Finset.image p Q) = Ψ.total Q

The image of a face of Ψ under the parent map has the exponent sum of the face.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.preimage_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {P : Finset ℕ} (hP : P ∈ Φ.nerve) : ⇑ρ ⁻¹' Φ.faceSet P = ⋃ Q ∈ {Q ∈ Ψ.nerve | Finset.image p Q = P}, Ψ.faceSet Q

The preimage of the locus of a face is the union of the loci of the faces mapping onto it.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.eq_of_image_eq_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) {Q₁ Q₂ : Finset ℕ} (hQ₁ : Q₁ ∈ Ψ.nerve) (hQ₂ : Q₂ ∈ Ψ.nerve) (hQ : Finset.image p Q₁ = Finset.image p Q₂) {x : X.carrier} (hx₁ : x ∈ Ψ.faceSet Q₁) (hx₂ : x ∈ Ψ.faceSet Q₂) : Q₁ = Q₂

Two faces of Ψ with the same image and a common point coincide.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.exists_lift_over {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) (S : Finset (Finset ℕ)) (hS : ∀ P ∈ S, P ∈ Φ.nerve) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) (hZ' : Manifold.IsClosedSubmanifold ψ₀ (Ψ.centerOf (Ψ.preimageFaces p S)) r) : ∃ (ℓ : AnalyticMap (Manifold.blowUp ψ₀ hZ') (Manifold.blowUp ψ₀ hZ)), IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ℓ ∧ (∀ (q : (Manifold.blowUp ψ₀ hZ').carrier), (Manifold.blowUpπ ψ₀ hZ) (ℓ q) = ρ ((Manifold.blowUpπ ψ₀ hZ') q)) ∧ (Function.Surjective ⇑ρ → Function.Surjective ⇑ℓ)

The lift of ρ to the blow-ups of the preimage centre, transported to the centre of Ψ by the set equality of preimage_centerOf, is a local analytic isomorphism lying over ρ, surjective when ρ is.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X Y : AnalyticManifold 𝕜 E} {Ψ : PieceFamily X} {Φ : PieceFamily Y} {ρ : AnalyticMap X Y} {p σ : ℕ → ℕ} (h : Ψ.RefinesAlong ρ p σ Φ) (S : Finset (Finset ℕ)) (hS : ∀ P ∈ S, P ∈ Φ.nerve) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) (hZ' : Manifold.IsClosedSubmanifold ψ₀ (Ψ.centerOf (Ψ.preimageFaces p S)) r) (ℓ : AnalyticMap (Manifold.blowUp ψ₀ hZ') (Manifold.blowUp ψ₀ hZ)) (hℓ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ℓ) (hsq : ∀ (q : (Manifold.blowUp ψ₀ hZ').carrier), (Manifold.blowUpπ ψ₀ hZ) (ℓ q) = ρ ((Manifold.blowUpπ ψ₀ hZ') q)) : (Ψ.blowUpPieces (Ψ.preimageFaces p S) m hZ').RefinesAlong ℓ (Ψ.extendParent Φ p (Ψ.preimageFaces p S) S) (Ψ.extendLabel Φ σ) (Φ.blowUpPieces S m hZ)

The step of the comparison in which Φ blows up a centre S and Ψ blows up the faces mapping into S: the transformed families refine one another along any local analytic isomorphism ℓ of the blow-ups lying over ρ, with the extended parent and label maps.