The marked transform of the monomial ideal under the blow-up of a centre

The marked transform π_*^{-1}(M(𝓘), m) of the monomial ideal along a centre of the monomial procedure is the monomial ideal of the transformed piece family (Realizes.birationalTransform_monomialIdeal): the old pieces keep their exponents on their strict transforms, and the new piece of each face P carries total P − m, as in [Kol07, 111, Step 3]. Stalk by stalk, the marked transform is the exact quotient of the total transform by the m-th power of the exceptional ideal ([Kol07, Definition 60, (60.1)]): off the exceptional divisor both ideals agree with the total transform; over the locus of P the total transform is 𝓘_F^{total P} times the strict transforms (BMO/Step3Monomial/TransformStalk.lean), so dividing by 𝓘_F^m leaves 𝓘_F^{total P − m}, the colon of a principal power in the regular analytic stalk, a domain. The identification uses the uniqueness of the exact quotient.

theorem Ideal.colon_mul_span_singleton_pow {R : Type u_1} [CommRing R] [IsDomain R] (J : Ideal R) {u : R} (hu : u ≠ 0) {m t : ℕ} (hmt : m ≤ t) : Submodule.colon (J * span {u ^ t}) ↑(span {u ^ m}) = J * span {u ^ (t - m)}

In a domain, the colon of a principal power out of a product with a larger principal power: (J · (u^t)) : (u^m) = J · (u^{t−m}) for m ≤ t and u ≠ 0.

theorem Hironaka.Manifold.BMO.PieceFamily.Realizes.birationalTransform_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.ι} {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)) (hge : ∀ P ∈ S, m ≤ Φ.total P) : (Manifold.MarkedIdealSheaf.birationalTransform hZ ⋯ { I := Φ.monomialIdeal hF hΦ, m := m }).I = (Φ.blowUpPieces S m hZ).monomialIdeal ⋯ ⋯

The marked transform of the monomial ideal along the locus of a centre is the monomial ideal of the transformed family ([Kol07, 111, Step 3], [Kol07, Definition 60]): the old pieces keep their exponents on their strict transforms, and the new piece of each face P carries total P − m.