The exponents after a step of the monomial phase

A step of the monomial phase at the mark 1 blows up the positive locus Z of the top member E^j and carries the ideal by the marked transform at the mark 1 (Step2bStep.lean). The decomposition of [Kol07, Definition–Lemma 110] and the remarks after [Wlo09, Theorem 2.0.3] say what happens to the exponents a_D = ord_D 𝓘 along the boundary components: the controlled transform is (M(𝓘)/𝓘(D)) · N(𝓘) with the blow-down an isomorphism, so the exponent along the exceptional divisor D' = π⁻¹(Z) (the new last member) is one less than the exponent along Z, the exponents along the other members are unchanged, and the strict transform of E^j carries only its components of exponent 0. This module proves these facts:

• the stalks: off Z the ideal after the step is the pull-back of 𝓘 (stalkIdeal_stepIdeal_of_notMem, from birationalTransform_stalkIdeal_of_notMem); everywhere it is the colon of the pulled-back stalk by the pulled-back stalk of 𝓘_Z (stalkIdeal_stepIdeal, from isDivExceptional_birationalTransform at the mark 1, the transform (60.1) of [Kol07, Definition 60]);
• the ideal sheaves of the members: the new member's is the pull-back of 𝓘_Z (isIdealSheafOf_exceptionalIdealSheaf), the other members' are the pull-backs of theirs (the identification of the strict transforms in Step2bTools.lean, comap_idealSheaf_of_isLocalDiffeomorph);
• the orders along the members, through the bijective germ map of the blow-up (an isomorphism, isLocalDiffeomorph_blowUpπ_of_codimOne) and the algebra of ColonPrincipal.lean on the prime, pairwise non-dividing coordinates of a chart with simple normal crossings (IsSncChartAt.prime_coord, IsSncChartAt.not_coord_dvd): ordAlong_stepIdeal_inr_add_one (ord_{D'} 𝓘' + 1 = ord_Z 𝓘), ordAlong_stepIdeal_inl_of_ne (ord_{E'^k} 𝓘' = ord_{E^k} 𝓘 for k ≠ j), ordAlong_stepIdeal_inl_top (the strict transform of E^j: ord_{E'^j} 𝓘' = ord_{E^j} 𝓘 = 0, the point lying off Z).

These feed the termination measure of the phase (Step2bMeasure.lean).

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_span_singleton {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} (hY : IsClosedSubmanifold ψ Y 1) {a : M} (ha : a ∈ Y) {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) (haφ : a ∈ φ.source) : hY.idealSheaf.stalkIdeal a = Ideal.span {coord E ψ φ ⋯ haφ (σ 0)}

The stalk of the ideal sheaf of a codimension-one submanifold at a point of the submanifold is the principal ideal of the adapted coordinate (the span form of the stalk on Fin 1).

The stalks of the step ideal

theorem Hironaka.Manifold.BMOmod.stalkIdeal_stepIdeal_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : (stepπ T hfin hne) x' ∉ step2bCenter T hfin hne) : Manifold.IdealSheaf.stalkIdeal (stepIdeal T hfin hne) x' = (Manifold.IdealSheaf.pullback ⇑(stepπ T hfin hne) ⋯ T.I).stalkIdeal x'

Off the exceptional divisor the ideal after the step is the pull-back of 𝓘 (birationalTransform_stalkIdeal_of_notMem).

theorem Hironaka.Manifold.BMOmod.stalkIdeal_stepIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (x' : (stepStage T hfin hne).carrier) : Manifold.IdealSheaf.stalkIdeal (stepIdeal T hfin hne) x' = Submodule.colon ((Manifold.IdealSheaf.pullback ⇑(stepπ T hfin hne) ⋯ T.I).stalkIdeal x') ↑((Manifold.IdealSheaf.pullback ⇑(stepπ T hfin hne) ⋯ ⋯.idealSheaf).stalkIdeal x')

The transform (60.1) of [Kol07, Definition 60] at the mark 1 (isDivExceptional_birationalTransform): the stalk of the ideal after the step is the colon of the pulled-back stalk of 𝓘 by the pulled-back stalk of 𝓘_Z.

The members' ideal sheaves after the step

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

The ideal sheaf of the new member D' = π⁻¹(Z) is the pull-back of 𝓘_Z (isIdealSheafOf_exceptionalIdealSheaf).

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

For k ≠ j the ideal sheaf of the strict transform E'^k = π⁻¹(E^k) is the pull-back of 𝓘_{E^k} (stepFamily_hyp_inl_of_ne, comap_idealSheaf_of_isLocalDiffeomorph).

theorem Hironaka.Manifold.BMOmod.stalkIdeal_idealSheaf_stepFamily_inl_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : x' ∈ (stepFamily T hfin hne).hyp (toLex (Sum.inl (topMember T hfin hne)))) : ⋯.idealSheaf.stalkIdeal x' = (Manifold.IdealSheaf.pullback ⇑(stepπ T hfin hne) ⋯ ⋯.idealSheaf).stalkIdeal x'

At a point of the strict transform of the top member (which lies off Z), the stalk of its ideal sheaf is the stalk of the pull-back of 𝓘_{E^j} (stalkIdeal_idealSheaf_congr_nhds on the open π⁻¹(Zᶜ), where the strict transform is the preimage).

The germ map of the blow-down and the transported stalks

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.stepGermMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (x' : (stepStage T hfin hne).carrier) : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk ((stepπ T hfin hne) x')) →+* ↑((Manifold.structureSheaf 𝕜 E (stepStage T hfin hne).carrier).presheaf.stalk x')

The germ map of the blow-down of the step at x'.

Equations

• Hironaka.Manifold.BMOmod.stepGermMap T hfin hne x' = Manifold.germMap ⇑(Hironaka.Manifold.BMOmod.stepπ T hfin hne) ⋯ x'

theorem Hironaka.Manifold.BMOmod.stepGermMap_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (x' : (stepStage T hfin hne).carrier) : Function.Bijective ⇑(stepGermMap T hfin hne x')

theorem Hironaka.Manifold.BMOmod.stalkIdeal_comap_stepπ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (J : M.IdealSheaf) (x' : (stepStage T hfin hne).carrier) : (Manifold.IdealSheaf.pullback ⇑(stepπ T hfin hne) ⋯ J).stalkIdeal x' = Ideal.map (stepGermMap T hfin hne x') (Manifold.IdealSheaf.stalkIdeal J ((stepπ T hfin hne) x'))

The exponent along the new member drops by one

theorem Hironaka.Manifold.BMOmod.ordAlong_stepIdeal_inr_add_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : (stepπ T hfin hne) x' ∈ step2bCenter T hfin hne) : ⋯.idealSheaf.ordAlongIdeal (stepIdeal T hfin hne) x' + 1 = ⋯.idealSheaf.ordAlongIdeal T.I ((stepπ T hfin hne) x')

Along the new member D' = π⁻¹(Z) the order of the ideal after the step is one less than the order of 𝓘 along Z: ord_{D'} 𝓘' + 1 = ord_Z 𝓘 at every point over Z ([Kol07, Definition–Lemma 110]; the remarks after [Wlo09, Theorem 2.0.3]).

The exponents along the other members are unchanged

theorem Hironaka.Manifold.BMOmod.ordAlong_stepIdeal_inl_of_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {k : T.F.ι} (hk : k ≠ topMember T hfin hne) {x' : (stepStage T hfin hne).carrier} (hxk : (stepπ T hfin hne) x' ∈ T.F.hyp k) : ⋯.idealSheaf.ordAlongIdeal (stepIdeal T hfin hne) x' = ⋯.idealSheaf.ordAlongIdeal T.I ((stepπ T hfin hne) x')

For a member k ≠ j, the order of the ideal after the step along E'^k = π⁻¹(E^k) equals the order of 𝓘 along E^k at the point below (the other exponents are untouched, [Kol07, Definition–Lemma 110]). Off Z the ideal after the step is the pull-back; over Z its stalk is the colon by the coordinate of Z = E^j (locally), which does not change the order along the transversal prime coordinate of E^k (ordAlongIdeal_colon_of_prime).

theorem Hironaka.Manifold.BMOmod.ordAlong_stepIdeal_inl_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : x' ∈ (stepFamily T hfin hne).hyp (toLex (Sum.inl (topMember T hfin hne)))) : ⋯.idealSheaf.ordAlongIdeal (stepIdeal T hfin hne) x' = ⋯.idealSheaf.ordAlongIdeal T.I ((stepπ T hfin hne) x')

The strict transform of the top member carries only components of exponent 0: at each of its points the order of the ideal after the step along it is the order of 𝓘 along E^j at the point below, which lies off the positive locus, so it is 0.

theorem Hironaka.Manifold.BMOmod.ordAlong_eq_zero_of_notMem_positiveLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {j : T.F.ι} {y : M.carrier} (hyj : y ∈ T.F.hyp j) (hy : y ∉ positiveLocus T j) : ⋯.idealSheaf.ordAlongIdeal T.I y = 0

The order of 𝓘 along E^j vanishes off the positive locus (the locality of Step2bLocal.lean).