The marked transform of a product

The marked transform (π_j)_*^{-1}(J, m) divides F^m out of the total transform π_j^* J [Kol07, Definition 60]. When the sequence has order ≥ m for (J, m), so that F_j^m divides the pull-back of the marked transform at every step, the marked transform of a product J · K is the marked transform of J times the plain pull-back of K: the one exceptional factor F^m is taken from the pull-back of J, and the colon by the invertible F^m cancels it exactly (colon_pow_eq_of_mul_eq). The proof of [Wlo05, Theorem 4.7.1] uses this when the strict transforms of some components of the subvariety are isolated and ignored by the rest of the resolution: the marked ideal I' · I_Γ transforms as the marked transform of I' times the pull-back of the ideal of the isolated components.

theorem Hironaka.Sequence.markedTransformSeq_mul_comap_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J K : X.IdealSheafData) (m : ℕ) (h : ∀ (i : Fin S.length), S.exceptionalAt i ^ m ∣ (S.markedTransformSeq J m i.castSucc).comap (S.step i)) (j : ℕ) (hj : j < S.length + 1) : S.markedTransformSeq (J * K) m ⟨j, hj⟩ = S.markedTransformSeq J m ⟨j, hj⟩ * K.comap (S.stageMap ⟨j, hj⟩)

The marked transform of [Kol07, Definition 60] for a product: along a sequence whose every step has F_j^m ∣ π_j^*(J_j), the marked transform of J · K at stage j is the marked transform of J times the pull-back of K to stage j, in the ⟨j, h⟩ form of the indices.

theorem Hironaka.Sequence.markedTransformSeq_mul_comap {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J K : X.IdealSheafData) (m : ℕ) (h : ∀ (i : Fin S.length), S.exceptionalAt i ^ m ∣ (S.markedTransformSeq J m i.castSucc).comap (S.step i)) (i : Fin (S.length + 1)) : S.markedTransformSeq (J * K) m i = S.markedTransformSeq J m i * K.comap (S.stageMap i)

markedTransformSeq_mul_comap_mk at an arbitrary stage index.

theorem Hironaka.Sequence.exceptionalAt_pow_dvd_comap_step_of_isOrderGeSeq {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (J : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (hS : S.IsOrderGeSeq f J m E) (i : Fin S.length) : S.exceptionalAt i ^ m ∣ (S.markedTransformSeq J m i.castSucc).comap (S.step i)

The divisibility hypothesis of markedTransformSeq_mul_comap holds along a smooth blow-up sequence of order ≥ m for (J, m) [Kol07, Definition 66] (exceptionalAt_pow_dvd_comap_step_of_leOrdAlong).

theorem Hironaka.Sequence.markedTransformSeq_mul_comap_last_of_isOrderGeSeq {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (J K : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (hS : S.IsOrderGeSeq f J m E) : S.markedTransformSeq (J * K) m (Fin.last S.length) = S.markedTransformSeq J m (Fin.last S.length) * K.comap (S.stageMap (Fin.last S.length))

Along a smooth blow-up sequence of order ≥ m for (J, m), the marked transform of J · K at the end is the marked transform of J times the pull-back of K along the composite [Kol07, Definition 60].