The stalks of the monomial ideals after a blow-up

The stalk at a point x of the monomial ideal ∏_c 𝓘_{piece c}^{a c} is the product, over the pieces through x, of the powers of the vanishing stalks of their members (stalkIdeal_monomialIdeal). After the blow-up of a centre, the stalk at p of the monomial ideal of the transformed family is the product, over the old pieces through π p, of the powers of the vanishing stalks of their strict transforms, times, over the locus of a face P, the vanishing stalk of the exceptional divisor to the power total P − m (stalkIdeal_monomialIdeal_blowUpPieces_of_notMem, …_of_mem_faceSet); and the stalk of the total transform π^* M is the same product with the exceptional power total P instead (stalkIdeal_totalTransform_monomialIdeal_of_notMem, …_of_mem_faceSet). The last statement is the identity π^* 𝓘_D = 𝓘_{D'} · 𝓘_F for a member D containing the centre and π^* 𝓘_D = 𝓘_{D'} for the others, read at every stalk: each member's vanishing stalk pulls back to 𝓘_F^ε times that of its strict transform, with ε = 1 exactly for the pieces of the face, and the pieces of P through π p are all of P. The exponent total P is Kollár's coefficient of the new divisor before the division by m in [Kol07, 111, Step 3] and [Kol07, Definition 60].

The stalk of the monomial ideal

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.vanishingStalk_piece_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hΦ : Φ.Realizes F e) {c : Fin Φ.nextComp} {x : N.carrier} (hx : x ∈ Φ.piece ↑c) : Manifold.vanishingStalk (Φ.piece ↑c) x = Manifold.vanishingStalk (F.hyp (e ⟨Φ.label ↑c, ⋯⟩)) x

At one of its points, the vanishing stalk of a piece is that of its member.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_pieceIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (c : Fin Φ.nextComp) (x : N.carrier) : (Φ.pieceIdeal hF hΦ c).stalkIdeal x = Manifold.vanishingStalk (Φ.piece ↑c) x

The stalk of the ideal sheaf of a piece is the vanishing stalk of the piece.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_monomialIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (x : N.carrier) : (Φ.monomialIdeal hF hΦ).stalkIdeal x = ∏ c : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c }, Manifold.vanishingStalk (F.hyp (e ⟨Φ.label ↑↑c, ⋯⟩)) x ^ Φ.a ↑↑c

The stalk of the monomial ideal at x is the product, over the pieces through x, of the powers of the vanishing stalks of their members.

The stalks after the blow-up

theorem Hironaka.Manifold.BMO.PieceFamily.isSnc_totalTransform_centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (Manifold.HypersurfaceFamily.totalTransform (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) F)

The boundary family after the blow-up of a centre has simple normal crossings, the centre having simple normal crossings with the family.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.vanishingStalk_strictTransformSet_piece_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) {r : ℕ} (hZ' : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) r) {c : Fin Φ.nextComp} {p : (Manifold.blowUp ψ₀ hZ').carrier} (hp : (Manifold.blowUpπ ψ₀ hZ') p ∈ Φ.piece ↑c) : Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ')) (Φ.centerOf S) (Φ.piece ↑c)) p = Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ')) (Φ.centerOf S) (F.hyp (e ⟨Φ.label ↑c, ⋯⟩))) p

At a point over a piece, the vanishing stalk of the strict transform of the piece is that of the strict transform of its member: the strict transform of a clopen part of a set is the corresponding clopen part of the strict transform.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_monomialIdeal_blowUpPieces_eq_prod_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) (p : (Manifold.blowUp ψ₀ hZ).carrier) : ((Φ.blowUpPieces S m hZ).monomialIdeal ⋯ ⋯).stalkIdeal p = ∏ c ∈ Finset.range (Φ.nextComp + S.card), Manifold.vanishingStalk ((Φ.blowUpPieces S m hZ).piece c) p ^ (Φ.blowUpPieces S m hZ).a c

The stalk of the monomial ideal of the transformed family at p, as a product over all indices below nextComp + |S| of the powers of the vanishing stalks of the new pieces.

theorem Hironaka.Manifold.BMO.PieceFamily.prod_range_nextComp_vanishingStalk_blowUpPieces {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) (p : (Manifold.blowUp ψ₀ hZ).carrier) : ∏ c ∈ Finset.range Φ.nextComp, Manifold.vanishingStalk ((Φ.blowUpPieces S m hZ).piece c) p ^ (Φ.blowUpPieces S m hZ).a c = ∏ c : { c : Fin Φ.nextComp // (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.piece ↑c }, Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) (F.hyp (e ⟨Φ.label ↑↑c, ⋯⟩))) p ^ Φ.a ↑↑c

The old part of the product: the strict transforms of the old pieces through π p.

theorem Hironaka.Manifold.BMO.PieceFamily.prod_range_card_vanishingStalk_blowUpPieces_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {m : ℕ} {S : Finset (Finset ℕ)} (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hp : (Manifold.blowUpπ ψ₀ hZ) p ∉ Φ.centerOf S) : ∏ c ∈ Finset.range S.card, Manifold.vanishingStalk ((Φ.blowUpPieces S m hZ).piece (Φ.nextComp + c)) p ^ (Φ.blowUpPieces S m hZ).a (Φ.nextComp + c) = 1

Off the exceptional divisor the new part of the product is trivial: no new piece passes through p.

theorem Hironaka.Manifold.BMO.PieceFamily.prod_range_card_vanishingStalk_blowUpPieces_of_mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {P : Finset ℕ} (hP : P ∈ S) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hxP : (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.faceSet P) : ∏ c ∈ Finset.range S.card, Manifold.vanishingStalk ((Φ.blowUpPieces S m hZ).piece (Φ.nextComp + c)) p ^ (Φ.blowUpPieces S m hZ).a (Φ.nextComp + c) = Manifold.vanishingStalk (⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' Φ.centerOf S) p ^ (Φ.total P - m)

Over the locus of P, only the new piece of P passes through p; its vanishing stalk is that of the exceptional divisor and its exponent is total P − m.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_monomialIdeal_blowUpPieces_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hp : (Manifold.blowUpπ ψ₀ hZ) p ∉ Φ.centerOf S) : ((Φ.blowUpPieces S m hZ).monomialIdeal ⋯ ⋯).stalkIdeal p = ∏ c : { c : Fin Φ.nextComp // (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.piece ↑c }, Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) (F.hyp (e ⟨Φ.label ↑↑c, ⋯⟩))) p ^ Φ.a ↑↑c

The stalk of the monomial ideal of the transformed family at a point off the exceptional divisor: the strict transforms of the old pieces through π p, with their exponents.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_monomialIdeal_blowUpPieces_of_mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {P : Finset ℕ} (hP : P ∈ S) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hxP : (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.faceSet P) : ((Φ.blowUpPieces S m hZ).monomialIdeal ⋯ ⋯).stalkIdeal p = (∏ c : { c : Fin Φ.nextComp // (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.piece ↑c }, Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) (F.hyp (e ⟨Φ.label ↑↑c, ⋯⟩))) p ^ Φ.a ↑↑c) * Manifold.vanishingStalk (⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' Φ.centerOf S) p ^ (Φ.total P - m)

The stalk of the monomial ideal of the transformed family at a point over the locus of the face P: the strict transforms of the old pieces through π p, times the exceptional divisor to the power total P − m.

The stalks of the total transform

theorem Hironaka.Manifold.BMO.PieceFamily.sum_ite_mem_eq_total {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {P : Finset ℕ} (hPn : ∀ c ∈ P, c < Φ.nextComp) {x : N.carrier} (hxP : x ∈ Φ.faceSet P) : (∑ c : { c : Fin Φ.nextComp // x ∈ Φ.piece ↑c }, if ↑↑c ∈ P then Φ.a ↑↑c else 0) = Φ.total P

The exponent sum over the pieces of P through a point of its locus is total P.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_totalTransform_monomialIdeal_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hp : (Manifold.blowUpπ ψ₀ hZ) p ∉ Φ.centerOf S) : (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hZ) ⋯ (Φ.monomialIdeal hF hΦ)).stalkIdeal p = ∏ c : { c : Fin Φ.nextComp // (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.piece ↑c }, Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) (F.hyp (e ⟨Φ.label ↑↑c, ⋯⟩))) p ^ Φ.a ↑↑c

The stalk of the total transform of the monomial ideal at a point off the exceptional divisor: the pull-back of the vanishing stalk of a member not containing the centre is that of its strict transform.

theorem Hironaka.Manifold.BMO.PieceFamily.stalkIdeal_totalTransform_monomialIdeal_of_mem_faceSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {Φ : PieceFamily N} {F : Manifold.HypersurfaceFamily N.carrier} {e : Fin Φ.nextLabel ↪o F.ι} {m : ℕ} {hV : Φ.IsValid n m} {S : Finset (Finset ℕ)} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hΦ : Φ.Realizes F e) (hS : (Φ.toState n m hV).IsCenter S) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Φ.centerOf S) (faceCard S)) {P : Finset ℕ} (hP : P ∈ S) {p : (Manifold.blowUp ψ₀ hZ).carrier} (hxP : (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.faceSet P) : (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hZ) ⋯ (Φ.monomialIdeal hF hΦ)).stalkIdeal p = (∏ c : { c : Fin Φ.nextComp // (Manifold.blowUpπ ψ₀ hZ) p ∈ Φ.piece ↑c }, Manifold.vanishingStalk (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ₀ hZ)) (Φ.centerOf S) (F.hyp (e ⟨Φ.label ↑↑c, ⋯⟩))) p ^ Φ.a ↑↑c) * Manifold.vanishingStalk (⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' Φ.centerOf S) p ^ Φ.total P

The stalk of the total transform of the monomial ideal at a point over the locus of the face P: the strict transforms of the old pieces through π p, times the exceptional divisor to the power total P. The pieces of P are exactly the pieces through π p whose coordinates lie in the block of the centre, and only for those does the pull-back of the member's vanishing stalk acquire the exceptional factor.