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

The second condition of [Kol07, 34.1] and the compatibility of [Wlo09, Theorem 2.0.3 (4)] (in the sense of [Wlo09, Definition 3.2.6]) for the monomial phase at the mark 1: along a local analytic isomorphism g : N → M the complete phase of the pulled-back triple is the pull-back of the complete phase of T with its empty blow-ups deleted, step2bPhase k' (T.pullback g) = ((step2bPhase k T).pullback g).eraseEmpty for every k ≥ step2bMeasure T and k' ≥ step2bMeasure (T.pullback g) (step2bPhase_pullback_eraseEmpty). This gives the compatibility of the family of the phase and the half of its commutation with local isomorphisms for open embeddings.

Induction on the fuel of T. At a step with centre Z (the positive locus of the top member j) either g⁻¹(Z) is nonempty, and then j is the top member of the pull-back too, the centre pulls back to the centre and the step to the step (Step2bPullback.lean), and the induction continues along the lift of g; or g⁻¹(Z) is empty: the pulled-back blow-up is the empty one, which the deletion of empty blow-ups removes by carrying the tail back along the isomorphism Bl_∅ N ≃ N (eraseEmpty_cons_of_eq_empty, map_eq_pullback_symm); the triple of the tail carried back is the pull-back with one empty member appended (emptyStepTriple_I, isEmptyExtension_emptyStepTriple: the marked transform along an empty blow-up is the total transform, birationalTransform_I_of_eq_empty), so the phase is indifferent to it (Step2bEmpty.lean) and the carried-back phase is the pull-back's own (Step2bPullback.lean, the isomorphism being surjective). The fuels are reconciled by the stabilisation of Step2bMeasure.lean: the measure does not increase under pull-back (step2bMeasure_pullback_le) nor under the deletion of empty members (step2bMeasure_le_of_isEmptyExtension).

The measure under pull-back and under empty extensions

theorem Hironaka.Manifold.BMOmod.memberSup_pullback_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (k : T.F.ι) : memberSup (T.pullback g hg) k ≤ memberSup T k

The supremum along a pulled-back member is at most the supremum along the member (the order along the member transports along g, ordAlongIdeal_comap_of_isLocalDiffeomorphAt).

theorem Hironaka.Manifold.BMOmod.nonemptyFinset_pullback_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hT' : Manifold.AnalyticTriple.BMOClass 1 (T.pullback g hg)) : (T.pullback g hg).F.nonemptyFinset ⋯ ⊆ T.F.nonemptyFinset ⋯

A nonempty member of the pull-back lies over a nonempty member.

theorem Hironaka.Manifold.BMOmod.step2bMeasure_pullback_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (hT' : Manifold.AnalyticTriple.BMOClass 1 (T.pullback g hg)) : step2bMeasure (T.pullback g hg) hT' ≤ step2bMeasure T hT

The measure does not increase under pull-back along a local isomorphism.

theorem Hironaka.Manifold.BMOmod.memberSup_le_of_hyp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T₁ T₂ : Manifold.AnalyticTriple ψ₀ M) (hI : T₁.I = T₂.I) {k₁ : T₁.F.ι} {k₂ : T₂.F.ι} (hk : T₂.F.hyp k₂ = T₁.F.hyp k₁) : memberSup T₁ k₁ ≤ memberSup T₂ k₂

Members with the same underlying set (and the same ideal sheaf) have the same sup.

theorem Hironaka.Manifold.BMOmod.step2bMeasure_le_of_isEmptyExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T₁ T₂ : Manifold.AnalyticTriple ψ₀ M) (hI : T₁.I = T₂.I) (e : T₁.F.ι ↪o T₂.F.ι) (hext : Manifold.HypersurfaceFamily.IsEmptyExtension e) (h₁ : Manifold.AnalyticTriple.BMOClass 1 T₁) (h₂ : Manifold.AnalyticTriple.BMOClass 1 T₂) : step2bMeasure T₁ h₁ ≤ step2bMeasure T₂ h₂

The measure does not increase under an empty extension of the boundary.

Fuels above the measure give the same phase

theorem Hironaka.Manifold.BMOmod.step2bPhase_eq_of_step2bMeasure_le' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) {k k' : ℕ} (hk : step2bMeasure T hT ≤ ↑k) (hk' : step2bMeasure T hT ≤ ↑k') : step2bPhase k T hT = step2bPhase k' T hT

theorem Hironaka.Manifold.BMOmod.step2bMeasure_congr_heq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {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₂) : step2bMeasure T₁ h₁ = step2bMeasure T₂ h₂

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

The empty case: the tail carried back along Bl_∅ N ≃ N

@[reducible, inline]

abbrev Hironaka.Manifold.BMOmod.emptyPre {𝕜 : 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) : Manifold.IsClosedSubmanifold ψ₀ (⇑g ⁻¹' step2bCenter T hfin hne) 1

The preimage of the centre, as a closed submanifold of N.

Equations

• ⋯ = ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.emptyIso {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (Manifold.blowUp ψ₀ ⋯).carrier N.carrier ⊤

The isomorphism Bl_∅ N ≃ N of the empty blow-up (emptyBlowUpDiffeomorph).

Equations

• Hironaka.Manifold.BMOmod.emptyIso T hfin hne g hg hZe = AnalyticManifold.BlowUpSequence.emptyBlowUpDiffeomorph ⋯ hZe

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.emptyBack {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) : AnalyticMap N (Manifold.blowUp ψ₀ ⋯)

Its inverse as an analytic map N → Bl_∅ N.

Equations

• Hironaka.Manifold.BMOmod.emptyBack T hfin hne g hg hZe = (Hironaka.Manifold.BMOmod.emptyIso T hfin hne g hg hZe).symm.toAnalyticMap

theorem Hironaka.Manifold.BMOmod.blowUpπ_emptyBack {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) (x : N.carrier) : (Manifold.blowUpπ ψ₀ ⋯) ((emptyBack T hfin hne g hg hZe) x) = x

theorem Hironaka.Manifold.BMOmod.emptyBack_surjective {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) : Function.Surjective ⇑(emptyBack T hfin hne g hg hZe)

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.emptyStepTriple {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) : Manifold.AnalyticTriple ψ₀ N

The step pulled back along the lift and carried back to N.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BMOmod.emptyStepTriple_I {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) : (emptyStepTriple T hfin hne g hg hZe).I = (T.pullback g hg).I

Along the empty blow-up the marked transform is the total transform (birationalTransform_I_of_eq_empty), so the carried-back ideal sheaf is the pull-back's own.

theorem Hironaka.Manifold.BMOmod.isEmptyExtension_emptyStepTriple {𝕜 : 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) (hZe : ⇑g ⁻¹' step2bCenter T hfin hne = ∅) : Manifold.HypersurfaceFamily.IsEmptyExtension (Manifold.HypersurfaceFamily.inlLexEmb T.F.ι)

The carried-back boundary is the pull-back's boundary with one empty member appended.

The commutation theorem

theorem Hironaka.Manifold.BMOmod.step2bPhase_pullback_eraseEmpty {𝕜 : 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) (hT' : Manifold.AnalyticTriple.BMOClass 1 (T.pullback g hg)) : step2bMeasure T hT ≤ ↑k → ∀ (k' : ℕ), step2bMeasure (T.pullback g hg) hT' ≤ ↑k' → step2bPhase k' (T.pullback g hg) hT' = ((step2bPhase k T hT).pullback g hg).eraseEmpty

The second condition of [Kol07, 34.1] and the compatibility of [Wlo09, Theorem 2.0.3 (4)]: along a local analytic isomorphism g, the complete phase of the pull-back is the pull-back of the complete phase with its empty blow-ups deleted.