The monomial phase commutes with surjective local isomorphisms

The first condition of [Kol07, 34.1] for the monomial phase at the mark 1: along a surjective local analytic isomorphism g : N → M the phase of the pulled-back triple is the pull-back of the phase, step2bPhase k (T.pullback g) = (step2bPhase k T).pullback g at every fuel k (step2bPhase_pullback_of_surjective). The rule is intrinsic: the active members of the pull-back are those of T (activeMembers_pullback_of_surjective), so the top members agree and the centre pulls back to the centre (step2bCenter_pullback of Step2bLocal.lean); one step pulls back to one step (stepTripleOf_pullback_eq: birationalTransform_comap_liftStep for the marked transform, totalTransform_comap_of_square for the boundary, along the lift liftStep g of g to the blow-ups); and the lift of a surjective local isomorphism to the blow-ups of a centre of codimension one is again surjective (liftStep_surjective, the blow-downs being isomorphisms). The two cons are compared by cons_congr_heq: the pulled-back centre and the centre of the pull-back are propositionally equal sets with different witnesses, so the step is stated at an arbitrary witness (stepTripleOf, Step2bStep.lean) and the tails are heterogeneously equal (heq_step2bPhase).

This is the first of the two halves of the functoriality of the phase; the half for open embeddings, up to the deletion of empty blow-ups, is Step2bCommute.lean.

theorem Hironaka.Manifold.BMOmod.heq_step2bPhase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M₁ M₂ : AnalyticManifold 𝕜 E} (hM : M₁ = M₂) (T₁ : Manifold.AnalyticTriple ψ₀ M₁) (T₂ : Manifold.AnalyticTriple ψ₀ M₂) (hT : T₁ ≍ T₂) (h₁ : Manifold.AnalyticTriple.BMOClass 1 T₁) (h₂ : Manifold.AnalyticTriple.BMOClass 1 T₂) : step2bPhase k T₁ h₁ ≍ step2bPhase k T₂ h₂

The phase is congruent under heterogeneous equality of triples over equal manifolds.

One step pulls back to one step

theorem Hironaka.Manifold.BMOmod.stepTripleOf_pullback_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hfin' : (activeMembers (T.pullback g hg)).Finite) (hne' : (activeMembers (T.pullback g hg)).Nonempty) (htop : topMember (T.pullback g hg) hfin' hne' = topMember T hfin hne) : stepTripleOf (T.pullback g hg) hfin' hne' ⋯ ⋯ = (stepTriple T hfin hne).pullback (AnalyticManifold.BlowUpSequence.liftStep g hg ⋯) ⋯

[Kol07, 34.1] for one step of the monomial phase: when the top members agree, the step of the pull-back (at the witness of the pulled-back centre) is the pull-back of the step along the lift of g: the marked transform by birationalTransform_comap_liftStep, the total transform by totalTransform_comap_of_square with the square blowUpπ_liftStep of the lift.

The lift of a surjective local isomorphism to codimension-one blowings-up is surjective

theorem Hironaka.Manifold.BMOmod.liftStep_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hs : Function.Surjective ⇑g) {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ₀ Y 1) : Function.Surjective ⇑(AnalyticManifold.BlowUpSequence.liftStep g hg hY)

For a centre of codimension one both blow-downs are isomorphisms, so the lift of a surjective local analytic isomorphism is surjective.

The phase commutes with surjective local isomorphisms

theorem Hironaka.Manifold.BMOmod.step2bPhase_pullback_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : Function.Surjective ⇑g → ∀ (hT' : Manifold.AnalyticTriple.BMOClass 1 (T.pullback g hg)), step2bPhase k (T.pullback g hg) hT' = (step2bPhase k T hT).pullback g hg

The first condition of [Kol07, 34.1]: along a surjective local analytic isomorphism the phase of the pull-back is the pull-back of the phase, at every fuel. The active members and the top member agree (activeMembers_pullback_of_surjective, topMember_pullback_eq), the centre pulls back to the centre, one step to one step (stepTripleOf_pullback_eq), and the lift is again a surjective local isomorphism (liftStep_surjective).