The nonmonomial part of a marked transform, one blow-up at a time

Step 1 of the proof of [Kol07, Theorem 107] (item 111) applies order reduction to the nonmonomial part N(𝓘) and observes that the transform of N(𝓘) and the marked transform of (𝓘, m) differ by a product of powers of the exceptional divisors, hence only in their monomial part, so that along the whole sequence Π one has N(Π_*^{-1}(𝓘, m)) = Π_*^{-1} N(𝓘). This file proves the blow-up-by-blow-up content of that remark, in the form N(π_*^{-1}(𝓘, m)) = N(π^* N(𝓘)) with the total transform on the right, for a blow-up π with centre Y having simple normal crossings with the boundary family F and for the transformed family F' = F.totalTransform π Y (the strict transforms of the members followed by the exceptional divisor):

• the total transform π^* 𝓘 and the marked transform π_*^{-1}(𝓘, m) have the same nonmonomial part with respect to F', because they differ by a power of the exceptional ideal (BMO/Step1BlowUp.lean), which the nonmonomial part ignores;
• the total transform of 𝓘 = M(𝓘) · N(𝓘) is π^*(M(𝓘)) · π^*(N(𝓘)), and the factor π^*(M(𝓘)) is a monomial in the components of F' (BMO/Step1ExistsComap.lean), so π^* 𝓘 and π^* N(𝓘) have the same nonmonomial part;
• hence N_{F'}(π_*^{-1}(𝓘, m)) = N_{F'}(π^* N(𝓘)), the one-step form of Kollár's remark.

The file also records that the nonmonomial part and the total transform of an ideal sheaf that is nonzero at every point are nonzero at every point, and that the monomial part is the unit ideal when every component exponent vanishes.

theorem Hironaka.Manifold.BMO.nonmonomialPart_totalTransform_eq_nonmonomialPart_birationalTransform {𝕜 : 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} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) (m : ℕ) {J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (hk : ∀ x ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J x) (hJmt : (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I.IsNonzeroEverywhere) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ J) = nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I

For m ≤ ord_Y J along the centre, the total transform π^* J and the marked transform π_*^{-1}(J, m) have the same nonmonomial part with respect to the transformed boundary family F': the total transform is the m-th power of the exceptional ideal times the marked transform (totalTransform_eq_exc_pow_mul_birationalTransform), and the nonmonomial part ignores powers of the exceptional ideal (nonmonomialPart_exceptionalIdealSheaf_pow_mul), the marked transform being nonzero at every point.

theorem Hironaka.Manifold.BMO.totalTransform_eq_totalTransform_monomialPart_mul_nonmonomialPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : Manifold.IdealSheaf.pullback π ⋯ I = Manifold.IdealSheaf.pullback π ⋯ (monomialPart F hF I) * Manifold.IdealSheaf.pullback π ⋯ (nonmonomialPart F hF I)

The total transform of 𝓘 is the product of the total transforms of its monomial and nonmonomial parts, π^* 𝓘 = π^*(M(𝓘)) · π^*(N(𝓘)): from 𝓘 = M(𝓘) · N(𝓘) and the multiplicativity of the total transform.

theorem Hironaka.Manifold.BMO.nonmonomialPart_totalTransform_eq_nonmonomialPart_totalTransform_nonmonomialPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hNnz : (Manifold.IdealSheaf.pullback π ⋯ (nonmonomialPart F hF I)).IsNonzeroEverywhere) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ I) = nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ (nonmonomialPart F hF I))

The total transforms of 𝓘 and of its nonmonomial part N(𝓘) have the same nonmonomial part with respect to the transformed boundary family F': writing π^* 𝓘 = π^*(M(𝓘)) · π^*(N(𝓘)), the factor π^*(M(𝓘)) is a locally finite product of powers of the component ideals of F' (exists_comap_monomialPart_eq_monomial), which the nonmonomial part ignores (nonmonomialPart_locallyFiniteProduct_pow_mul) as long as the other factor is nonzero at every point.

theorem Hironaka.Manifold.BMO.nonmonomialPart_birationalTransform_eq_nonmonomialPart_totalTransform_nonmonomialPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) (m : ℕ) {J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (hk : ∀ x ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J x) (hJmt : (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I.IsNonzeroEverywhere) (hNnz : (Manifold.IdealSheaf.pullback π ⋯ (nonmonomialPart F hF J)).IsNonzeroEverywhere) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I = nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ (nonmonomialPart F hF J))

For m ≤ ord_Y J along the centre, the nonmonomial part of the marked transform of (J, m) equals the nonmonomial part of the total transform of N(J), both with respect to the transformed boundary family: N_{F'}(π_*^{-1}(J, m)) = N_{F'}(π^* N(J)). This is the one-blow-up form of the remark in Kol07, 111, Step 1 that the two transforms differ only in their monomial part, obtained by composing nonmonomialPart_totalTransform_eq_nonmonomialPart_birationalTransform with nonmonomialPart_totalTransform_eq_nonmonomialPart_totalTransform_nonmonomialPart.

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_totalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) {J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (hJ : J.IsNonzeroEverywhere) : (Manifold.IdealSheaf.pullback π ⋯ J).IsNonzeroEverywhere

The total transform along a blow-up of an ideal sheaf that is nonzero at every point is nonzero at every point: its stalk is the image of a nonzero stalk under the injective germ map of the blow-up.

theorem Hironaka.Manifold.BMO.monomialPart_eq_top_of_forall_componentExponent_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hzero : ∀ (i : ComponentIndex F), componentExponent F hF I i = 0) : monomialPart F hF I = ⊤

The monomial part is the unit ideal when every component exponent vanishes: each factor is then 𝓘_D ^ 0 = 1.