The marked transform of a sum of powers along a sequence of its own order

In the proof of Theorem 107 [Kol07, 111, Step 2], order reduction is applied to the ideal N(I)^m + I^s, of order ≥ ms, and every smooth blow-up sequence of order ms for it "is also a smooth blow-up sequence of order s" for N(I) and one of order m for I. For J := A^m + B^s and a blow-up of order exactly ms for J with center Z: ord_Z A ≥ s and ord_Z B ≥ m (Kollár's observation ord_Z J_1 ≥ s ∧ ord_Z J_2 ≥ m ⇔ ord_Z (J_1^m + J_2^s) ≥ ms, Hironaka/Resolution/Algebraic/Order/SupPow.lean), so F^s ∣ π^* A and F^m ∣ π^* B, and π^{-1}_*(J, ms) = π^{-1}_*(A, s)^m + π^{-1}_*(B, m)^s: both sides, multiplied by F^{ms}, are π^* J = (F^s π^{-1}_*(A, s))^m + (F^m π^{-1}_*(B, m))^s, and the quotient by the invertible F^{ms} is unique. Along the sequence the identity propagates (the birational transform at the exact order is the marked transform, weakTransform_eq_markedTransform_of_smooth), and the order clause of [Kol07, Definition 66] for J at each center gives the clauses for (A, s) and (B, m) by the same observation, with the same centers and the same boundaries.

• markedTransform_pow_sup_pow: one blow-up.
• weakTransformSeq_pow_sup_pow: the identity at every stage of a smooth blow-up sequence of order ms for A^m + B^s.
• isOrderGeSeq_of_isOrderSeq_pow_sup_pow_left/_right: the sequence is of order ≥ s for (A, s) and of order ≥ m for (B, m).

theorem Hironaka.Sequence.markedTransform_pow_sup_pow {X : AlgebraicGeometry.Scheme} (D A B : X.IdealSheafData) (m s : ℕ) (hA : D.exceptionalDivisor ^ s ∣ A.comap D.blowUpπ) (hB : D.exceptionalDivisor ^ m ∣ B.comap D.blowUpπ) : (A ^ m ⊔ B ^ s).markedTransform D (m * s) = A.markedTransform D s ^ m ⊔ B.markedTransform D m ^ s

When F^s ∣ π^* A and F^m ∣ π^* B (Kollár's ord_Z A ≥ s, ord_Z B ≥ m), the marked transform of A^m + B^s at the mark ms is π^{-1}_*(A, s)^m + π^{-1}_*(B, m)^s: both are the unique K with F^{ms} · K = π^*(A^m + B^s) [Kol07, 111, Step 2]. This is an identity of ideal sheaves on the blow-up of any scheme along D, given the two divisibilities; no smoothness enters.

theorem Hironaka.Sequence.weakTransformSeq_pow_sup_pow {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {A B : X.IdealSheafData} {E : X.DivisorFamily} {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) {S : X.BlowUpSequence} (hS : S.IsOrderSeq f (A ^ m ⊔ B ^ s) E (m * s)) (i : Fin (S.length + 1)) : S.weakTransformSeq (A ^ m ⊔ B ^ s) i = S.markedTransformSeq A s i ^ m ⊔ S.markedTransformSeq B m i ^ s

Along a smooth blow-up sequence of order ms for A^m + B^s (m, s ≥ 1), at every stage the induced birational transform of A^m + B^s is π^{-1}_*(A, s)_i^m + π^{-1}_*(B, m)_i^s [Kol07, 111, Step 2]. By recursion on the sequence: at each center the order clause gives ord_Z A_i ≥ s and ord_Z B_i ≥ m, the birational transform at the exact order ms is the marked transform, and markedTransform_pow_sup_pow applies.

theorem Hironaka.Sequence.isOrderGeSeq_of_isOrderSeq_pow_sup_pow_left {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {A B : X.IdealSheafData} {E : X.DivisorFamily} {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) {S : X.BlowUpSequence} (hS : S.IsOrderSeq f (A ^ m ⊔ B ^ s) E (m * s)) : S.IsOrderGeSeq f A s E

"Also a smooth blow-up sequence of order s starting with N(I)" [Kol07, 111, Step 2]: a smooth blow-up sequence of order ms for A^m + B^s is a smooth blow-up sequence of order ≥ s for the marked ideal (A, s); same centers, same boundaries, and the order clause at every stage from ord_Z (A^m + B^s) ≥ ms.

theorem Hironaka.Sequence.isOrderGeSeq_of_isOrderSeq_pow_sup_pow_right {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {A B : X.IdealSheafData} {E : X.DivisorFamily} {m s : ℕ} (hm : 1 ≤ m) (hs : 1 ≤ s) {S : X.BlowUpSequence} (hS : S.IsOrderSeq f (A ^ m ⊔ B ^ s) E (m * s)) : S.IsOrderGeSeq f B m E

"And a smooth blow-up sequence of order m starting with I" [Kol07, 111, Step 2]: a smooth blow-up sequence of order ms for A^m + B^s is a smooth blow-up sequence of order ≥ m for the marked ideal (B, m).