The total transform of the monomial part is a monomial in the transformed boundary

Let π : M' → M be the blow-up of a centre Y having simple normal crossings with the boundary family F, and let F' = F.totalTransform π Y be the transformed family (the strict transforms of the members followed by the exceptional divisor). This file proves that the total transform π^* M(𝓘) of the monomial part of an ideal sheaf 𝓘 (BMO/MonomialPart.lean) is a locally finite product of powers of the component ideals of F' (exists_comap_monomialPart_eq_monomial), so that its nonmonomial part with respect to F' is the unit ideal (nonmonomialPart_totalTransform_monomialPart_eq_top) and it is its own monomial part (monomialPart_totalTransform_monomialPart_eq_self). This is the content, for the monomial part over connected components, of the remark in [Kol07, 111, Step 1] that tensoring with an ideal sheaf of exceptional divisors changes only the monomial part.

The proof is stalkwise and has three parts.

• The general engine. The stalk of M(K) at x depends only on the stalk of K at x, since every exponent is the order of K along a component at x (monomialPart_stalkIdeal_congr, nonmonomialPart_stalkIdeal_congr). Hence the nonmonomial part ignores a locally finite product of powers of component ideals (nonmonomialPart_locallyFiniteProduct_pow_mul), and an ideal sheaf whose stalks are all monomials in the active component ideals has trivial nonmonomial part (nonmonomialPart_eq_top_of_forall_stalkIdeal_eq_prod), hence equals its own monomial part.
• The exceptional divisor. The exceptional ideal sheaf is the ideal sheaf of the closed submanifold π⁻¹(Y); at a point of one of its connected components it has the stalk of that component's ideal (stalkIdeal_componentIdeal_totalTransform_inr), so the nonmonomial part for F' ignores powers of the exceptional ideal (nonmonomialPart_exceptionalIdealSheaf_pow_mul).
• The chart computation. Off the centre the blow-up is a local analytic isomorphism, and the total transform of the ideal of a component D of F has the stalk of the component of the strict transform of D through the point. Over the centre, in a chart adapted to Y and to F at a ∈ Y and a blow-up chart of index i₀ at x over a, the total transform of the ideal of a component D through a is generated by the pull-back of the coordinate z_D of D, which is: the coordinate of the exceptional divisor, if z_D is the scaling coordinate σ i₀; that coordinate times the ratio coordinate u_{σ k}, if z_D = z_{σ k} with k ≠ i₀, the ratio coordinate being the coordinate of the strict transform of D when x lies on it and a unit otherwise; the same coordinate of the blow-up chart, if z_D is off the block of the centre, again the coordinate of the strict transform of D or a unit. In every case the stalk is a monomial in the stalks of the component ideals of F' through x.

The assembly (stalkIdeal_totalTransform_monomialPart_eq_prod) writes the stalk of π^* M(𝓘) at x as a product of such factors, with exponents depending on x (the bookkeeping of finite monomials is IsFinsetMonomial), and the engine concludes. Blow-up charts are those of [BM88, Definition 4.1]; the exponents are Kollár's cᵢ of [Kol07, Definition–Lemma 110], read at one stalk.

The general engine: stalkwise monomials have trivial non-monomial part

theorem Hironaka.Manifold.BMO.componentIdeal_pow_stalkIdeal_top_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (a : ComponentIndex G → ℕ) (i : ComponentIndex G) (x : X) (hx : x ∉ componentSet G i) : (componentIdeal G hG i ^ a i).stalkIdeal x = ⊤

Off its component, any power of the component ideal is the unit ideal: the controlling-set hypothesis of the locally finite product ∏ᵢ 𝓘ᵢ ^ aᵢ for an arbitrary exponent function a.

theorem Hironaka.Manifold.BMO.componentIdeal_isNonzeroEverywhere {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (i : ComponentIndex G) : (componentIdeal G hG i).IsNonzeroEverywhere

The ideal sheaf of a component is nonzero at every point: on the component its stalk is generated by a prime element, off it the stalk is the unit ideal.

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_finset_prod_componentIdeal_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (s : Finset (ComponentIndex G)) (a : ComponentIndex G → ℕ) : (∏ i ∈ s, componentIdeal G hG i ^ a i).IsNonzeroEverywhere

A finite product of powers of component ideals is nonzero at every point, each factor being so and the stalks being domains.

theorem Hironaka.Manifold.BMO.monomialPart_stalkIdeal_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (K K' : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E X)) (x : X) (hKK' : K.stalkIdeal x = K'.stalkIdeal x) : (monomialPart G hG K).stalkIdeal x = (monomialPart G hG K').stalkIdeal x

The stalk of the monomial part at x depends only on the stalk of the ideal sheaf at x: every exponent of an active component is the order along that component at x (componentExponent_eq_toNat_ordAlongIdeal), which sees only the stalk at x.

theorem Hironaka.Manifold.BMO.nonmonomialPart_stalkIdeal_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (K K' : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E X)) (x : X) (hKK' : K.stalkIdeal x = K'.stalkIdeal x) : (nonmonomialPart G hG K).stalkIdeal x = (nonmonomialPart G hG K').stalkIdeal x

The stalk of the nonmonomial part at x depends only on the stalk of the ideal sheaf at x: it is the colon of that stalk by the stalk of the monomial part, which depends only on it as well.

theorem Hironaka.Manifold.BMO.nonmonomialPart_locallyFiniteProduct_pow_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (a : ComponentIndex G → ℕ) (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E X)) (hJ : J.IsNonzeroEverywhere) : nonmonomialPart G hG (Manifold.IdealSheaf.locallyFiniteProduct (Manifold.structureSheaf 𝕜 E X) (fun (i : ComponentIndex G) => componentIdeal G hG i ^ a i) (componentSet G) ⋯ ⋯ * J) = nonmonomialPart G hG J

The nonmonomial part ignores a locally finite product of powers of component ideals: N((∏'ᵢ 𝓘ᵢ ^ aᵢ) · J) = N(J) for J nonzero at every point. Stalkwise the locally finite product is the finite product over the active components, for which nonmonomialPart_finprod_componentIdeal_pow_mul applies ([Kol07, 111, Step 1]: an ideal of boundary divisors changes only the monomial part).

theorem Hironaka.Manifold.BMO.isNonzeroEverywhere_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] : ⊤.IsNonzeroEverywhere

The unit ideal sheaf is nonzero at every point (the stalks are domains).

theorem Hironaka.Manifold.BMO.nonmonomialPart_eq_top_of_forall_stalkIdeal_eq_prod {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E X)) (hK : ∀ (x : ↑↧X), ∃ (b : ComponentIndex G → ℕ), K.stalkIdeal x = ∏ i ∈ Manifold.IdealSheaf.activeFinset (componentSet G) ⋯ x, (componentIdeal G hG i).stalkIdeal x ^ b i) : nonmonomialPart G hG K = ⊤

An ideal sheaf whose stalks are monomials in the component ideals has trivial nonmonomial part: if at every x the stalk of K is a product of powers of the stalks of the active component ideals (with exponents that may depend on x), then N(K) = ⊤.

theorem Hironaka.Manifold.BMO.monomialPart_eq_self_of_nonmonomialPart_eq_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : Type u} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ X] (G : Manifold.HypersurfaceFamily X) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E X)) (hN : nonmonomialPart G hG K = ⊤) : monomialPart G hG K = K

If N(K) = ⊤ then K = M(K), by the decomposition K = M(K) · N(K).

The blow-up: the exceptional divisor's ideal and its component

theorem Hironaka.Manifold.BMO.exceptionalIdealSheaf_eq_idealSheaf_preimage {𝕜 : 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 π) : Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf = ⋯.idealSheaf

The exceptional ideal sheaf of a blow-up is the ideal sheaf of the exceptional divisor π⁻¹(Y) as a closed submanifold.

theorem Hironaka.Manifold.BMO.stalkIdeal_componentIdeal_totalTransform_inr {𝕜 : 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) (α : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit)))) {x : M'} (hx : x ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inr PUnit.unit), α⟩) : (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ ⟨toLex (Sum.inr PUnit.unit), α⟩).stalkIdeal x = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal x

At a point of a connected component α of the exceptional divisor, the ideal of that component of the transformed boundary family has the stalk of the exceptional ideal sheaf: the component is cut out of the exceptional divisor by an open set, and the ideal sheaf of a closed submanifold is germ-local.

theorem Hironaka.Manifold.BMO.nonmonomialPart_exceptionalIdealSheaf_pow_mul {𝕜 : 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')) (hJ : J.IsNonzeroEverywhere) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf ^ m * J) = nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ J

The nonmonomial part with respect to the transformed boundary family ignores powers of the exceptional ideal: N_{F'}(𝓘_F^m · J) = N_{F'}(J) for J nonzero at every point. At a point of the exceptional divisor the exceptional ideal has the stalk of the component ideal of the exceptional component through the point (stalkIdeal_componentIdeal_totalTransform_inr), and off it the stalk is the unit ideal ([Kol07, 111, Step 1]).

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_notMem {𝕜 : 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) {x : M'} (hxY : π x ∉ Y) (i : ComponentIndex F) (hxi : π x ∈ componentSet F i) (hxj : x ∈ Manifold.strictTransformSet π Y (F.hyp i.fst)) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ ⟨toLex (Sum.inl i.fst), ConnectedComponents.mk ⟨x, hxj⟩⟩).stalkIdeal x

Off the centre, at x with π x ∉ Y, the total transform of the ideal of a component D of F through π x has the stalk of the ideal of the component of the strict transform of D through x: the blow-up is a local analytic isomorphism at x, the strict transform is the preimage of D there, and a chart adapted to D at π x transports along the local inverse to a chart adapted to the strict transform at x, so the two stalks are generated by a coordinate germ and by its pull-back.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_eq_span_germMap {𝕜 : 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} (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = Ideal.span {(Manifold.germMap π ⋯ x) (Manifold.coord E ψ φ ⋯ ⋯ (cidx ⟨i.fst, ⋯⟩))}

Over the centre, in a chart φ adapted to Y and to F at a ∈ Y and a blow-up chart Φ at x over a, the total transform of the ideal of a component D of F through a is the principal ideal generated by the pull-back along π of the coordinate of D.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_eq_scaling {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) (hidx : cidx ⟨i.fst, ⋯⟩ = σ i₀) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal x

The case in which the coordinate of the component D is the scaling coordinate σ i₀ of the blow-up chart: the pulled-back coordinate is the coordinate of the exceptional divisor, so the total transform of the ideal of D has the stalk of the exceptional ideal at x.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_eq_ratio {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) {k : Fin c} (hk : k ≠ i₀) (hidx : cidx ⟨i.fst, ⋯⟩ = σ k) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal x * Ideal.span {Manifold.coord E ψ Φ ⋯ hx (σ k)}

The case in which the coordinate of the component D is a coordinate σ k, k ≠ i₀, of the centre: the pulled-back coordinate is the coordinate of the exceptional divisor times the ratio coordinate u_{σ k}, so the total transform of the ideal of D is the exceptional ideal times the ideal generated by the ratio coordinate at x.

theorem Hironaka.Manifold.BMO.stalkIdeal_componentIdeal_totalTransform_inl {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) {j : F.ι} (haj : a ∈ F.hyp j) (C' : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl j)))) (hxC : x ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inl j), C'⟩) : (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ ⟨toLex (Sum.inl j), C'⟩).stalkIdeal x = Ideal.span {Manifold.coord E ψ Φ ⋯ hx (cidx ⟨j, haj⟩)}

In the same chart, the ideal of the component ⟨inl j, C'⟩ of the strict transform of E^j through x is generated by the coordinate u_{cidx j} of the blow-up chart: the blow-up chart is a chart of simple normal crossings for the transformed family at x, with the strict transform of E^j cut out by the coordinate of E^j.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_eq_ratio_of_mem {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) {k : Fin c} (hk : k ≠ i₀) (hidx : cidx ⟨i.fst, ⋯⟩ = σ k) (hxj : x ∈ Manifold.strictTransformSet π Y (F.hyp i.fst)) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal x * (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ ⟨toLex (Sum.inl i.fst), ConnectedComponents.mk ⟨x, hxj⟩⟩).stalkIdeal x

The ratio case when x lies on the strict transform of the member of D: the ratio coordinate generates the ideal of the component of the strict transform through x, so the total transform of the ideal of D is the exceptional ideal times that component ideal at x.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_eq_ratio_of_notMem {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) {k : Fin c} (hk : k ≠ i₀) (hidx : cidx ⟨i.fst, ⋯⟩ = σ k) (hxj : x ∉ Manifold.strictTransformSet π Y (F.hyp i.fst)) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal x

The ratio case when x does not lie on the strict transform of the member of D: the ratio coordinate is a unit at x (on the chart the strict transform is its zero set), so the total transform of the ideal of D has the stalk of the exceptional ideal alone.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_notMem_range {𝕜 : 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} (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) (hidx : ∀ (k : Fin c), σ k ≠ cidx ⟨i.fst, ⋯⟩) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = Ideal.span {Manifold.coord E ψ Φ ⋯ hx (cidx ⟨i.fst, ⋯⟩)}

The case in which the coordinate of the component D is off the block of the centre (D is transversal to Y): the pulled-back coordinate is the same coordinate of the blow-up chart, with no exceptional factor.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_notMem_range_of_mem {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) (hidx : ∀ (k : Fin c), σ k ≠ cidx ⟨i.fst, ⋯⟩) (hxj : x ∈ Manifold.strictTransformSet π Y (F.hyp i.fst)) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ ⟨toLex (Sum.inl i.fst), ConnectedComponents.mk ⟨x, hxj⟩⟩).stalkIdeal x

The transversal case when x lies on the strict transform of the member of D: the total transform of the ideal of D has the stalk of the ideal of the component of the strict transform through x.

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_componentIdeal_of_notMem_range_of_notMem {𝕜 : 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} (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ a cidx) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (hxa : π x = a) (i : ComponentIndex F) (hai : a ∈ componentSet F i) (hidx : ∀ (k : Fin c), σ k ≠ cidx ⟨i.fst, ⋯⟩) (hxj : x ∉ Manifold.strictTransformSet π Y (F.hyp i.fst)) : (Manifold.IdealSheaf.pullback π ⋯ (componentIdeal F hF i)).stalkIdeal x = ⊤

The transversal case when x does not lie on the strict transform of the member of D: the coordinate is a unit at x, so the total transform of the ideal of D has unit stalk.

theorem Hironaka.Manifold.BMO.stalkIdeal_componentIdeal_totalTransform_inr_eq_span_coord {𝕜 : 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) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {i₀ : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i₀ Φ) {x : M'} (hx : x ∈ Φ.source) (α : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit)))) (hxα : x ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inr PUnit.unit), α⟩) : (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ ⟨toLex (Sum.inr PUnit.unit), α⟩).stalkIdeal x = Ideal.span {Manifold.coord E ψ Φ ⋯ hx (σ i₀)}

In a blow-up chart of index i₀, the ideal of the exceptional component through x is generated by the scaling coordinate u_{σ i₀}.

The finset-monomial bookkeeping

def Hironaka.Manifold.BMO.IsFinsetMonomial {ι : Type u_2} {R : Type u_3} [CommMonoid R] (A : Finset ι) (f : ι → R) (m : R) : Prop

m is a monomial in the f k, k ∈ A: m = ∏ k ∈ A, f k ^ g k for some exponents g. The bookkeeping for the stalkwise computation of the total transform of a monomial part: at each point the stalk is a monomial in the stalks of the component ideals through it.

Equations

• Hironaka.Manifold.BMO.IsFinsetMonomial A f m = ∃ (g : ι → ℕ), m = ∏ k ∈ A, f k ^ g k

theorem Hironaka.Manifold.BMO.IsFinsetMonomial.one {ι : Type u_2} {R : Type u_3} [CommMonoid R] (A : Finset ι) (f : ι → R) : IsFinsetMonomial A f 1

1 is the monomial with all exponents 0.

theorem Hironaka.Manifold.BMO.IsFinsetMonomial.of_mem {ι : Type u_2} {R : Type u_3} [CommMonoid R] {A : Finset ι} (f : ι → R) {k₀ : ι} (hk : k₀ ∈ A) : IsFinsetMonomial A f (f k₀)

A generator f k₀, k₀ ∈ A, is a monomial (exponent 1 at k₀, 0 elsewhere).

theorem Hironaka.Manifold.BMO.IsFinsetMonomial.mul {ι : Type u_2} {R : Type u_3} [CommMonoid R] {A : Finset ι} {f : ι → R} {m₁ m₂ : R} (h₁ : IsFinsetMonomial A f m₁) (h₂ : IsFinsetMonomial A f m₂) : IsFinsetMonomial A f (m₁ * m₂)

Monomials are closed under products (the exponents add).

theorem Hironaka.Manifold.BMO.IsFinsetMonomial.pow {ι : Type u_2} {R : Type u_3} [CommMonoid R] {A : Finset ι} {f : ι → R} {m : R} (h : IsFinsetMonomial A f m) (e : ℕ) : IsFinsetMonomial A f (m ^ e)

Monomials are closed under powers (the exponents are multiplied).

theorem Hironaka.Manifold.BMO.IsFinsetMonomial.prod {ι : Type u_2} {R : Type u_3} [CommMonoid R] {A : Finset ι} {f : ι → R} {κ : Type u_4} (T : Finset κ) (P : κ → R) (hP : ∀ i ∈ T, IsFinsetMonomial A f (P i)) : IsFinsetMonomial A f (∏ i ∈ T, P i)

A finite product of monomials is a monomial (the exponents are summed).

theorem Hironaka.Manifold.BMO.IsFinsetMonomial.top {ι : Type u_2} {S : Type u_4} [CommSemiring S] (A : Finset ι) (f : ι → Ideal S) : IsFinsetMonomial A f ⊤

For ideals, the unit ideal ⊤ = 1 is a monomial (the case of a unit factor).

The assembly: the total transform of the monomial part is a monomial

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_monomialPart_eq_prod {𝕜 : 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) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (x : M') : ∃ (b : ComponentIndex (Manifold.HypersurfaceFamily.totalTransform π Y F) → ℕ), (Manifold.IdealSheaf.pullback π ⋯ (monomialPart F hF I)).stalkIdeal x = ∏ i ∈ Manifold.IdealSheaf.activeFinset (componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F)) ⋯ x, (componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ i).stalkIdeal x ^ b i

At every point x of the blow-up, the stalk of the total transform of the monomial part M(𝓘) is a product of powers of the stalks of the component ideals of the transformed family through x, with exponents depending on x. The stalk of π^* M(𝓘) is the product over the components of F through π x of the powers of the total transforms of their ideals (stalkIdeal_totalTransform_locallyFiniteProduct), and each of those is a monomial in the stalks of the component ideals of F' at x by the chart computation (off the centre stalkIdeal_totalTransform_componentIdeal_of_notMem; over the centre the case distinction on the coordinate of the component).

theorem Hironaka.Manifold.BMO.nonmonomialPart_totalTransform_monomialPart_eq_top {𝕜 : 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) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ (monomialPart F hF I)) = ⊤

The nonmonomial part, with respect to the transformed boundary family, of the total transform of the monomial part is the unit ideal: the total transform of a monomial in the components of F is a monomial in the components of F' ([Kol07, 111, Step 1]).

theorem Hironaka.Manifold.BMO.monomialPart_totalTransform_monomialPart_eq_self {𝕜 : 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) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : monomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.pullback π ⋯ (monomialPart F hF I)) = Manifold.IdealSheaf.pullback π ⋯ (monomialPart F hF I)

The total transform of the monomial part is its own monomial part with respect to the transformed boundary family.

theorem Hironaka.Manifold.BMO.exists_comap_monomialPart_eq_monomial {𝕜 : 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) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) : ∃ (a : ComponentIndex (Manifold.HypersurfaceFamily.totalTransform π Y F) → ℕ), Manifold.IdealSheaf.pullback π ⋯ (monomialPart F hF I) = Manifold.IdealSheaf.locallyFiniteProduct (Manifold.structureSheaf 𝕜 E M') (fun (i : ComponentIndex (Manifold.HypersurfaceFamily.totalTransform π Y F)) => componentIdeal (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ i ^ a i) (componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F)) ⋯ ⋯

The total transform of the monomial part M(𝓘) is a locally finite product of powers of the component ideals of the transformed boundary family F': the exponents are its own component exponents with respect to F', for which the right-hand side is its monomial part, and it equals its monomial part by monomialPart_totalTransform_monomialPart_eq_self.