Concatenation of blow-up sequences: the marked order condition and the end data

The marked order condition of [Kol07, Definition 66] (a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), IsOrderGeSeq) along a concatenation: a sequence of order ≥ m for (X, I, m, E) followed by one of order ≥ m for the induced marked triple (X_r, Π^{-1}_*(I, m), m, Π^{-1}_{tot} E) is a sequence of order ≥ m for (X, I, m, E). This is the marked analogue of isOrderSeq_concat (Hironaka/Scheme/BlowUpSequence/ConcatApi.lean). In the proof of Theorem 107 [Kol07, 111, Step 1] the order reduction of the nonmonomial part is a concatenation of rounds, each of order ≥ m for the marked ideal, and the second step concatenates likewise.

• isOrderGeSeq_concat: the conditions (1′)–(4′) of Definition 66 concatenate.
• markedEnd_concat_iff: a property of the induced marked ideal and boundary at the end of a concatenation is the same property at the end of the second sequence for the first sequence's induced data, Π^{-1}_{S ++ T *}(I, m) = Π^{-1}_{T *}(Π^{-1}_{S *}(I, m), m) and (S ++ T)^{-1}_{tot} E = T^{-1}_{tot}(S^{-1}_{tot} E), stated without a transport of the end results (the two ends are definitionally equal along the recursion on S), so that no eqToHom appears, as in disjoint_cosupp_concat_iff of Hironaka/Scheme/BlowUpSequence/ConcatTransforms.lean.

theorem AlgebraicGeometry.isOrderGeSeq_concat {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) {I : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} (hS : S.IsOrderGeSeq f I m E) (hT : T.IsOrderGeSeq (CategoryTheory.CategoryStruct.comp S.composite f) (S.markedTransformSeq I m (Fin.last S.length)) m (S.totalTransformSeq E (Fin.last S.length))) : (S.concat T).IsOrderGeSeq f I m E

A smooth blow-up sequence of order ≥ m for (X, I, m, E) followed by one of order ≥ m for the induced marked data at its end is a smooth blow-up sequence of order ≥ m for (X, I, m, E) [Kol07, Definition 66, conditions (1′)–(4′)]; the marked analogue of isOrderSeq_concat.

theorem AlgebraicGeometry.markedEnd_concat_iff {X : Scheme} (P : {Y : Scheme} → Y.IdealSheafData → Y.DivisorFamily → Prop) (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) : P ((S.concat T).markedTransformSeq I m (Fin.last (S.concat T).length)) ((S.concat T).totalTransformSeq E (Fin.last (S.concat T).length)) ↔ P (T.markedTransformSeq (S.markedTransformSeq I m (Fin.last S.length)) m (Fin.last T.length)) (T.totalTransformSeq (S.totalTransformSeq E (Fin.last S.length)) (Fin.last T.length))

A property of the induced marked ideal and boundary at the end of S ++ T is the same property at the end of T for the data induced by S [Kol07, Definition 66, condition (1′)], stated without a transport of the end results, by recursion on S (nil: the two sides coincide; cons: the recursive call on the tail with the one-step transforms).