One step of the monomial phase at the mark 1

One blow-up of the monomial phase of the modified algorithm [Wlo09, Theorem 7.4.1]: the blow-up of the centre of Step2bCenter.lean (the positive locus of the latest-born active member, Kollár's Z_{-1} at the mark 1), with the triple carried along it as the sequences of the library carry it: the ideal by the marked transform at the mark 1 (the transform (60.1) of [Kol07, Definition 60], clause (1′) of [Kol07, Definition 66]; birationalTransform, the transform of markedTransformSeq, cons_markedTransformSeq_one), the boundary by the total transform ([Kol07, Definition 25], the new member last). This is the controlled transform (M(𝓘)/𝓘(D)) · N(𝓘) of the remarks after [Wlo09, Theorem 2.0.3], the blow-down being an isomorphism ([Kol07, Definition–Lemma 110]); the identity of the two, the exponents after the step and the termination of the phase are proved in Step2bExponent.lean and Step2bMeasure.lean. Here the step is made a triple of the class of BMO_{n,1}:

• the marked transform of an ideal sheaf nonzero everywhere, along a centre of order ≥ m, is nonzero everywhere (isNonzeroEverywhere_birationalTransform, the one-step form of isNonzeroEverywhere_markedTransformSeq);
• the total transform of the boundary along a centre with simple normal crossings has simple normal crossings (isSnc_totalTransform at hasSncWith_Zminus1);
• finitely many members stay nonempty (finite_nonempty_totalTransform).

The two bridges to the recursions of AnalyticManifold.FiniteSuccession are proved on the constructor form: a list starting with the blow-up of the step is of order ≥ 1 for (M, 𝓘, E) iff its tail is of order ≥ 1 for the triple after the step (isOfOrderGe_cons_step_iff, from isOfOrderGe_cons_iff with the two head clauses of Step2bCenter.lean, cons_markedTransformSeq_one and reducedTransform_eq_idealSheaf_totalTransform), and it has no empty centre iff its tail has none (noEmptyCenters_cons_step_iff, the centre being nonempty).

A general tool: the marked transform of a nonzero ideal sheaf is nonzero

theorem Hironaka.Manifold.isNonzeroEverywhere_birationalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) {π : N.carrier → M.carrier} (h : Manifold.IsBlowUp ψ₀ Y c π) (J : Manifold.MarkedIdealSheaf (Manifold.structureSheaf 𝕜 E M.carrier)) (hm : ∀ a ∈ Y, ↑J.m ≤ hY.idealSheaf.ordAlongIdeal J.I a) (hJ : J.I.IsNonzeroEverywhere) : (Manifold.MarkedIdealSheaf.birationalTransform hY h J).I.IsNonzeroEverywhere

Along a blow-up whose centre has order ≥ m for (J, m), the marked transform of a J nonzero everywhere is nonzero everywhere (the one-step form of isNonzeroEverywhere_markedTransformSeq): the stalk of the marked transform is the colon of the stalk of the total transform by a power of the exceptional ideal, which contains the stalk of the total transform, the image of the nonzero stalk of J under the injective germ map of the blow-up ((60.1) of [Kol07, Definition 60]).

The blowing-up of the Step 2b centre and the transformed triple

@[reducible, inline]

abbrev Hironaka.Manifold.BMOmod.stepCenter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.IsClosedSubmanifold ψ₀ (step2bCenter T hfin hne) 1

The closed-submanifold witness of the centre of the step (the head of the step's BlowUpSequence.cons).

Equations

• ⋯ = ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.stepStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : AnalyticManifold 𝕜 E

The stage after one blow-up of the monomial phase: the blow-up of the centre (an isomorphism, cons_codimOne_exists_diffeomorph).

Equations

• Hironaka.Manifold.BMOmod.stepStage T hfin hne = Manifold.blowUp ψ₀ ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.stepπ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : AnalyticMap (stepStage T hfin hne) M

The blow-down of the step.

Equations

• Hironaka.Manifold.BMOmod.stepπ T hfin hne = Manifold.blowUpπ ψ₀ ⋯

noncomputable def Hironaka.Manifold.BMOmod.stepIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : (stepStage T hfin hne).IdealSheaf

The ideal after the step: the marked transform π_*^{-1}(𝓘, 1) along the blow-up of the centre ((60.1) of [Kol07, Definition 60] at the mark 1; birationalTransform, the transform of markedTransformSeq, cons_markedTransformSeq_one). It is the controlled transform of the remarks after [Wlo09, Theorem 2.0.3].

Equations

• Hironaka.Manifold.BMOmod.stepIdeal T hfin hne = (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := T.I, m := 1 }).I

theorem Hironaka.Manifold.BMOmod.isNonzeroEverywhere_stepIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.IdealSheaf.IsNonzeroEverywhere (stepIdeal T hfin hne)

The ideal after the step is nonzero everywhere (the centre has order ≥ 1, one_le_ordAlong_step2bCenter).

noncomputable def Hironaka.Manifold.BMOmod.stepFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.HypersurfaceFamily (stepStage T hfin hne).carrier

The boundary after the step: the total transform of E [Kol07, Definition 25], the strict transforms of the members followed by the exceptional divisor π⁻¹(D) ≅ D as the last member (the order of birth).

Equations

• Hironaka.Manifold.BMOmod.stepFamily T hfin hne = Manifold.HypersurfaceFamily.totalTransform (⇑(Hironaka.Manifold.BMOmod.stepπ T hfin hne)) (Hironaka.Manifold.BMOmod.step2bCenter T hfin hne) T.F

theorem Hironaka.Manifold.BMOmod.isSnc_stepFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (stepFamily T hfin hne)

The boundary after the step has simple normal crossings (isSnc_totalTransform; the centre has simple normal crossings with E, hasSncWith_step2bCenter).

noncomputable def Hironaka.Manifold.BMOmod.stepTripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ₀ Y 1) (hYeq : Y = step2bCenter T hfin hne) : Manifold.AnalyticTriple ψ₀ (Manifold.blowUp ψ₀ hY)

The step of the monomial phase written at an arbitrary closed-submanifold witness of a set equal to the centre (the witness of the pulled-back centre differs from that of the pull-back's own centre).

Equations

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

theorem Hironaka.Manifold.BMOmod.heq_stepTripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {Y₁ Y₂ : Set M.carrier} (h₁ : Manifold.IsClosedSubmanifold ψ₀ Y₁ 1) (h₂ : Manifold.IsClosedSubmanifold ψ₀ Y₂ 1) (e₁ : Y₁ = step2bCenter T hfin hne) (e₂ : Y₂ = step2bCenter T hfin hne) : stepTripleOf T hfin hne h₁ e₁ ≍ stepTripleOf T hfin hne h₂ e₂

Two witnesses of the centre give heterogeneously equal steps.

noncomputable def Hironaka.Manifold.BMOmod.stepTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.AnalyticTriple ψ₀ (stepStage T hfin hne)

The triple after one blow-up of the monomial phase, (Bl_D M, π_*^{-1}(𝓘, 1), E_1): stepTripleOf at the centre's own witness.

Equations

• Hironaka.Manifold.BMOmod.stepTriple T hfin hne = Hironaka.Manifold.BMOmod.stepTripleOf T hfin hne ⋯ ⋯

@[simp]

theorem Hironaka.Manifold.BMOmod.stepTriple_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : (stepTriple T hfin hne).I = stepIdeal T hfin hne

@[simp]

theorem Hironaka.Manifold.BMOmod.stepTriple_F {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : (stepTriple T hfin hne).F = stepFamily T hfin hne

theorem Hironaka.Manifold.BMOmod.bmoClass_stepTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : Manifold.AnalyticTriple.BMOClass 1 (stepTriple T hfin hne)

The triple after the step lies in the class of BMO_{n,1} (finitely many nonempty members, finite_nonempty_totalTransform).

theorem Hironaka.Manifold.BMOmod.bmoClass_stepTripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ₀ Y 1) (hYeq : Y = step2bCenter T hfin hne) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : Manifold.AnalyticTriple.BMOClass 1 (stepTripleOf T hfin hne hY hYeq)

The triple after the step, at any witness of the centre, lies in the class of BMO_{n,1}.

The bridges to the recursions of the library, on the constructor form

theorem Hironaka.Manifold.BMOmod.cons_markedTransformSeq_one_step {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (rest : AnalyticManifold.BlowUpSequence ψ₀ (stepStage T hfin hne)) : (AnalyticManifold.BlowUpSequence.cons ⋯ rest).toSuccession.markedTransformSeq T.I 1 (Fin.succ 0) = stepIdeal T hfin hne

The marked transform at the stage 1 of any list starting with the blow-up of the step is the ideal after the step (cons_markedTransformSeq_one).

theorem Hironaka.Manifold.BMOmod.reducedTransform_step {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : AnalyticManifold.IdealSheaf.reducedTransform (stepπ T hfin hne) T.F.idealSheaf ⋯.idealSheaf = (stepFamily T hfin hne).idealSheaf

The reduced transform of the boundary ideal along the step is the ideal sheaf of the boundary after the step (reducedTransform_eq_idealSheaf_totalTransform).

theorem Hironaka.Manifold.BMOmod.isOfOrderGe_cons_step_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (rest : AnalyticManifold.BlowUpSequence ψ₀ (stepStage T hfin hne)) : (AnalyticManifold.BlowUpSequence.cons ⋯ rest).toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf ↔ rest.toSuccession.IsOfOrderGe (stepTriple T hfin hne).I 1 (stepTriple T hfin hne).F.idealSheaf

[Kol07, Definition 66] on the constructor form (isOfOrderGe_cons_iff): a list starting with the blow-up of the step is of order ≥ 1 for (M, 𝓘, E) iff its tail is of order ≥ 1 for the triple after the step, the two head clauses holding at the centre (hasOnlyNormalCrossingsWith_step2bCenter, one_le_ordAlong_step2bCenter).

theorem Hironaka.Manifold.BMOmod.noEmptyCenters_cons_step_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (rest : AnalyticManifold.BlowUpSequence ψ₀ (stepStage T hfin hne)) : (AnalyticManifold.BlowUpSequence.cons ⋯ rest).NoEmptyCenters ↔ rest.NoEmptyCenters

[Kol07, 32] on the constructor form: a list starting with the blow-up of the step has no empty centre iff its tail has none (the centre is nonempty, step2bCenter_nonempty).