Concatenation of blow-up sequences: empty centers, strict transforms, disjointness at the end

The empty blow-up convention of [Kol07, 32] along a concatenation: a concatenation of two sequences without empty centers has none. The boundary-clearing sequence of [Kol07, 104, Step 2.1] is a concatenation of values of the functors BD_{n,m,j} of [Kol07, Lemma 102], each without empty centers, and this lemma places the induced triple in the class of Lemma 102 again. The module also transports the strict transform of an ideal sheaf through a concatenation (strictTransformSeq_concat_last) and the disjointness of Lemma 102 (1), between the points of order ≥ m of the weak transform and the strict transform of a divisor, at the end of a concatenation (disjoint_cosupp_concat_iff).

theorem AlgebraicGeometry.noEmptyCenters_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (hS : S.NoEmptyCenters) (hT : T.NoEmptyCenters) : (S.concat T).NoEmptyCenters

The empty blow-up convention [Kol07, 32] through a concatenation: no empty center on either part, none on the whole.

theorem AlgebraicGeometry.strictTransformSeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (D : X.IdealSheafData) : (S.concat T).strictTransformSeq D (Fin.last (S.concat T).length) = (T.strictTransformSeq (S.strictTransformSeq D (Fin.last S.length)) (Fin.last T.length)).comap (CategoryTheory.eqToHom ⋯)

The strict transform along a concatenation is the strict transform along the second part of the strict transform along the first; the analogue of weakTransformSeq_concat_last for strict transforms.

theorem AlgebraicGeometry.disjoint_cosupp_concat_iff {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (J D : X.IdealSheafData) (m : ℕ) : Disjoint {x : ↥((S.concat T).stage (Fin.last (S.concat T).length)) | ↑m ≤ ((S.concat T).weakTransformSeq J (Fin.last (S.concat T).length)).ord x} ↑((S.concat T).strictTransformSeq D (Fin.last (S.concat T).length)).support ↔ Disjoint {x : ↥(T.stage (Fin.last T.length)) | ↑m ≤ (T.weakTransformSeq (S.weakTransformSeq J (Fin.last S.length)) (Fin.last T.length)).ord x} ↑(T.strictTransformSeq (S.strictTransformSeq D (Fin.last S.length)) (Fin.last T.length)).support

The disjointness of [Kol07, Lemma 102, conclusion (1)] (the points of order ≥ m of the weak transform against the strict transform of a divisor) at the end of a concatenation is the disjointness at the end of the second part for the transforms along the first, by the same induction as the transport lemmas, without the eqToHom of last_concat.