The monomial procedure commutes with local analytic isomorphisms up to empty blow-ups

For a piece family Ψ on X refining a piece family Φ on Y along a local analytic isomorphism ρ : X → Y (BMO/Step3Monomial/RefinesAlong.lean), the run of the monomial procedure on Ψ is the pull-back along ρ of the run on Φ with its empty blow-ups erased (RefinesAlong.realize_pullback_eraseEmpty), and step for step when ρ is surjective (realize_pullback_of_surjective). This is the functoriality of [Kol07, 111, Step 3] under smooth morphisms in the sense of [Kol07, 34.1], with empty blow-ups deleted as in [Kol07, 32]; on manifolds it is the compatibility of [Wlo09, Theorem 3.5.1 (1)–(2)]. The three properties of the value of the procedure on an open set (BMO/Step3Monomial/Naturality.lean) are instances of it.

The proof has a combinatorial half and a geometric half.

• The combinatorial half. The state of Ψ is related to the state of Φ by a renaming of labels (the relabelling relabel Ψ σ), a refinement of the state of the pull-back family pullbackFamily Φ ρ, and the inclusion of that state in the state of Φ. The combinatorial model (Hironaka.Monomial.MonomialState.step3_chainE) then writes the run of the relabelled state as the run of the state of Φ with skips (MonomialState.chainRunE): the steps whose centre has no face over X are skipped, the others are performed on the faces over them. The run of the state of Ψ itself is the same list, since a renaming of the labels does not change the run (step3_snd_eq_of_rel_id).
• The geometric half. realizeAux_pullback_eraseEmpty is an induction along the run on Y, carrying a shadow state with the pieces and nerve of Ψ: at a centre with no face of Ψ over it the preimage of the centre is empty, the pulled-back blow-up is erased, and Ψ refines the transformed family along the lift composed with the identification of the empty blow-up with its base (RefinesAlong.of_empty_step); at a centre with faces over it both sides blow up the same centre, the transformed families refine one another along the transported lift (RefinesAlong.blowUpPieces, BMO/Step3Monomial/RefineStep.lean), and the two tails are identified through the equality of the centres. The nerve rule of BMO/Step3Monomial/Kernel.lean keeps the shadow state in step with the transitions of Ψ.

The statements assume no relation between the member embeddings of the two families and the label map σ: the run depends on the pieces, their exponents and the order of the labels alone. Two general facts on the combinatorial relations (Refines.refl, Sub.refl) and two transports of blow-ups along equal centres of possibly differently stated codimensions (blowUp_congr', blowUpπ_castDom_liftStep') sit here beside their use.

Transport along equal centres of possibly different stated codimensions

theorem AnalyticManifold.BlowUpSequence.cons_congr_heq_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y₁ Y₂ : Set M.carrier} {c₁ c₂ : ℕ} (e : Y₁ = Y₂) (hc : c₁ = c₂) (h₁ : Manifold.IsClosedSubmanifold ψ₀ Y₁ c₁) (h₂ : Manifold.IsClosedSubmanifold ψ₀ Y₂ c₂) (r₁ : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ h₁)) (r₂ : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ h₂)) (hr : r₁ ≍ r₂) : cons h₁ r₁ = cons h₂ r₂

cons_congr_heq with the codimensions identified by an equation as well.

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_heq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ : AnalyticManifold 𝕜 E} (e : M₁ = M₂) (L₁ : BlowUpSequence ψ₀ M₁) (L₂ : BlowUpSequence ψ₀ M₂) (h : L₁ ≍ L₂) : L₁.eraseEmpty ≍ L₂.eraseEmpty

Erasing the empty blow-ups respects heterogeneous equality over equal manifolds.

theorem AnalyticManifold.BlowUpSequence.blowUp_congr' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z Z' : Set M.carrier} {c c' : ℕ} (hZZ' : Z = Z') (hc : c = c') (hZ : Manifold.IsClosedSubmanifold ψ₀ Z c) (hZ' : Manifold.IsClosedSubmanifold ψ₀ Z' c') : Manifold.blowUp ψ₀ hZ = Manifold.blowUp ψ₀ hZ'

blowUp_congr with the codimensions identified by an equation as well; the same statement as blowUp_congr with an extra hypothesis, used where the codimension is given by an equation.

theorem AnalyticManifold.BlowUpSequence.blowUpπ_castDom_liftStep' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {Z : Set N.carrier} {c c' : ℕ} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hZ : Manifold.IsClosedSubmanifold ψ₀ Z c') (hZg : Z = ⇑g ⁻¹' Y) (hc : c' = c) (q : (Manifold.blowUp ψ₀ hZ).carrier) : (Manifold.blowUpπ ψ₀ hY) ((Hironaka.Manifold.AnalyticMap.castDom ⋯ (liftStep g hg hY)) q) = g ((Manifold.blowUpπ ψ₀ hZ) q)

blowUpπ_castDom_liftStep with the codimensions identified by an equation as well.

The combinatorial glue: a renaming of labels alone does not change the run

theorem Hironaka.Monomial.MonomialState.Refines.refl (D : MonomialState) : Refines id D D

Every state refines itself along the identity.

theorem Hironaka.Monomial.MonomialState.Sub.refl (D : MonomialState) : D.Sub D

Every state is a sub-state of itself.

theorem Hironaka.Monomial.MonomialState.chainRunE_eq_self {N st' : MonomialState} {L : List (Finset (Finset ℕ))} (h : N.IsRun L st') (ρ : ℕ → ℕ) (D : MonomialState) : (∀ c < D.nextComp, ρ c = c) → D.nextComp = N.nextComp → D.nerve = N.nerve → chainRunE ρ D N L = L

The run with skips of a run, along a parent map that is the identity on the pieces, from a state with the same pieces and nerve, is the run itself: no step is skipped and every centre is its own set of faces over itself.

theorem Hironaka.Monomial.MonomialState.step3_snd_eq_of_rel_id {σ : ℕ → ℕ} {D P : MonomialState} (h : Rel id σ D P) (hnc : D.nextComp = P.nextComp) : D.step3.2 = P.step3.2

A renaming of the labels alone does not change the run of the monomial procedure: two states related by Rel id σ with the same pieces have the same list of centres.

Relabelling, centres over a centre, the parent maps

theorem Hironaka.Manifold.BMO.PieceFamily.isValid_relabel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (σ : ℕ → ℕ) (L : ℕ) (hσ : ∀ ℓ < Ψ.nextLabel, σ ℓ < L) (hinj : Set.InjOn σ (Set.Iio Ψ.nextLabel)) {n m : ℕ} (hV : Ψ.IsValid n m) : (Ψ.relabel σ L hσ).IsValid n m

The relabelled family satisfies the invariants of the state when the label map is injective on the labels in use.

theorem Hironaka.Manifold.BMO.PieceFamily.extendComp_eq_extendParent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X Y : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (Φ : PieceFamily Y) (p : ℕ → ℕ) (D : Monomial.MonomialState) (hnc : D.nextComp = Ψ.nextComp) {n m : ℕ} (hVΦ : Φ.IsValid n m) (S' S : Finset (Finset ℕ)) : Monomial.MonomialState.extendComp p D (Φ.toState n m hVΦ) S' S = Ψ.extendParent Φ p S' S

The extension of the parent map on the combinatorial model, from a shadow state with the pieces of Ψ, is extendParent.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.isCenter_preimageFaces {𝕜 : 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 σ Φ) {n m : ℕ} (hVΨ : Ψ.IsValid n m) (hVΦ : Φ.IsValid n m) (S : Finset (Finset ℕ)) (hS : (Φ.toState n m hVΦ).IsCenter S) : (Ψ.toState n m hVΨ).IsCenter (Ψ.preimageFaces p S)

The faces of Ψ over a centre of the state of Φ form a centre of the state of Ψ: they are faces, and two of them have equal label sets because their images do and σ is injective on the labels.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.faceCard_preimageFaces {𝕜 : 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 σ Φ) {F : Manifold.HypersurfaceFamily Y.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {n m : ℕ} {hVΦ : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hS : (Φ.toState n m hVΦ).IsCenter S) (hne : (Ψ.preimageFaces p S).Nonempty) : faceCard (Ψ.preimageFaces p S) = faceCard S

The faces over a centre have the centre's face size: the parent map is injective on a face and all faces of a centre have the same size.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.of_empty_step {𝕜 : 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) (hno : ∀ Q ∈ Ψ.nerve, Finset.image p Q ∉ S) (m : ℕ) {r : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) (ℓ : AnalyticMap X (Manifold.blowUp ψ₀ hZ)) (hsq : ∀ (x : X.carrier), (Manifold.blowUpπ ψ₀ hZ) (ℓ x) = ρ x) : Ψ.RefinesAlong ℓ p σ (Φ.blowUpPieces S m hZ)

The step of the comparison in which no face of Ψ maps into the centre S of Φ: the preimage of the centre is empty, the corresponding blow-up is deleted from the run over X ([Kol07, 32]), and Ψ itself refines the transformed family of Φ along any map over ρ, with the same parent and label maps (the label map now into the larger label range).

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 r' : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) (hZ' : Manifold.IsClosedSubmanifold ψ₀ (Ψ.centerOf (Ψ.preimageFaces p S)) r') (hr : r' = 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)

RefinesAlong.blowUpPieces with the codimension of the centre of Ψ given by an equation.

The realisation of equal lists

theorem Hironaka.Manifold.BMO.PieceFamily.realizeAux_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (m : ℕ) {L₁ L₂ : List (Finset (Finset ℕ))} (e : L₁ = L₂) (h₁ : SmoothCenters ψ₀ Ψ m L₁) : realizeAux ψ₀ Ψ m L₁ h₁ = realizeAux ψ₀ Ψ m L₂ ⋯

The realisation depends on the list of centres, not on the smoothness proof.

theorem Hironaka.Manifold.BMO.PieceFamily.realizeAux_congr' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} (Ψ : PieceFamily X) (m : ℕ) {L₁ L₂ : List (Finset (Finset ℕ))} (e : L₁ = L₂) (h₁ : SmoothCenters ψ₀ Ψ m L₁) (h₂ : SmoothCenters ψ₀ Ψ m L₂) : realizeAux ψ₀ Ψ m L₁ h₁ = realizeAux ψ₀ Ψ m L₂ h₂

realizeAux_congr with both smoothness proofs given.

The induction along the run

theorem Hironaka.Manifold.BMO.PieceFamily.realizeAux_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (L : List (Finset (Finset ℕ))) {X Y : AnalyticManifold 𝕜 E} (Φ : PieceFamily Y) {F : Manifold.HypersurfaceFamily Y.carrier} {e : Fin Φ.nextLabel ↪o F.ι} : Manifold.HypersurfaceFamily.IsSnc ψ₀ F → Φ.Realizes F e → ∀ {m : ℕ} (hV : Φ.IsValid n m) {st' : Monomial.MonomialState}, (Φ.toState n m hV).IsRun L st' → ∀ (Ψ : PieceFamily X) {F' : Manifold.HypersurfaceFamily X.carrier} {e' : Fin Ψ.nextLabel ↪o F'.ι}, Manifold.HypersurfaceFamily.IsSnc ψ₀ F' → Ψ.Realizes F' e' → Ψ.IsValid n m → ∀ (ρ : AnalyticMap X Y) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) {p σ : ℕ → ℕ}, Ψ.RefinesAlong ρ p σ Φ → ∀ (D : Monomial.MonomialState), D.nextComp = Ψ.nextComp → D.nerve = Ψ.nerve → ∀ (hL : SmoothCenters ψ₀ Φ m L) (hL' : SmoothCenters ψ₀ Ψ m (Monomial.MonomialState.chainRunE p D (Φ.toState n m hV) L)), realizeAux ψ₀ Ψ m (Monomial.MonomialState.chainRunE p D (Φ.toState n m hV) L) hL' = ((realizeAux ψ₀ Φ m L hL).pullback ρ hρ).eraseEmpty

The induction along a run L of the state of Φ: for Ψ refining Φ along ρ and a shadow state D carrying the pieces and nerve of Ψ, the realisation on Ψ of the run with skips is the pull-back of the realisation on Φ with its empty blow-ups erased.

The pull-back of the run

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.realize_pullback_eraseEmpty {𝕜 : 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 σ : ℕ → ℕ} {F : Manifold.HypersurfaceFamily Y.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) {m : ℕ} (hVΦ : Φ.IsValid n m) {F' : Manifold.HypersurfaceFamily X.carrier} {e' : Fin Ψ.nextLabel ↪o F'.ι} (hF' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (hΨ : Ψ.Realizes F' e') (hVΨ : Ψ.IsValid n m) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) (h : Ψ.RefinesAlong ρ p σ Φ) : Ψ.realize hF' hΨ hVΨ = ((Φ.realize hF hΦ hVΦ).pullback ρ hρ).eraseEmpty

The run of the monomial procedure on a refining family is the pull-back of the run, with its empty blow-ups erased ([Kol07, 34.1], [Kol07, 32]). The statement holds for any boundary family realised by Ψ: the run depends on the pieces, their exponents and the order of the labels alone.

theorem Hironaka.Manifold.BMO.PieceFamily.RefinesAlong.realize_pullback_of_surjective {𝕜 : 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 σ : ℕ → ℕ} {F : Manifold.HypersurfaceFamily Y.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) {m : ℕ} (hVΦ : Φ.IsValid n m) {F' : Manifold.HypersurfaceFamily X.carrier} {e' : Fin Ψ.nextLabel ↪o F'.ι} (hF' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (hΨ : Ψ.Realizes F' e') (hVΨ : Ψ.IsValid n m) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) (hs : Function.Surjective ⇑ρ) (h : Ψ.RefinesAlong ρ p σ Φ) : Ψ.realize hF' hΨ hVΨ = (Φ.realize hF hΦ hVΦ).pullback ρ hρ

Along a surjective local analytic isomorphism the run of a refining family is the pull-back of the run step for step, no blow-up being empty.