Concatenation of blow-up sequences: the stages and transforms at a shifted index

The stage of S.concat T at an index S.length + i is the stage i of T, and the center and the transforms of an ideal sheaf or a boundary there are those of T at i for the transforms along S; below S.length they are those of S. These are the analogues, for the suffix, of the truncation lemmas stage_take_mk and markedTransformSeq_take_heq_mk of Hironaka/Scheme/BlowUpSequence/Truncate.lean for the prefix (Kollár's Π_{ij} bookkeeping, [Kol07, Definition 29]). The embedded resolution reads a run of the marked order reduction functor (the blow-up sequence the functor assigns to a triple), which is a concatenation of rounds, round by round with these lemmas.

theorem AlgebraicGeometry.stage_concat_mk {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (j i : ℕ) (hj : j < (S.concat T).length + 1) (hi : i < T.length + 1) : j = S.length + i → (S.concat T).stage ⟨j, hj⟩ = T.stage ⟨i, hi⟩

The stage of a concatenation at an index j = S.length + i is the stage i of the second sequence.

theorem AlgebraicGeometry.center_concat_heq_mk {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (j i : ℕ) (hj : j < (S.concat T).length) (hi : i < T.length) : j = S.length + i → (S.concat T).center ⟨j, hj⟩ ≍ T.center ⟨i, hi⟩

The centre of a concatenation at an index j = S.length + i is the centre i of the second sequence, heterogeneously.

theorem AlgebraicGeometry.markedTransformSeq_concat_heq_mk {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (m j i : ℕ) (hj : j < (S.concat T).length + 1) (hi : i < T.length + 1) : j = S.length + i → (S.concat T).markedTransformSeq I m ⟨j, hj⟩ ≍ T.markedTransformSeq (S.markedTransformSeq I m (Fin.last S.length)) m ⟨i, hi⟩

The marked transform along a concatenation at an index j = S.length + i is the marked transform along the second sequence at i of the marked transform along the first, heterogeneously.

theorem AlgebraicGeometry.strictTransformSeq_concat_heq_mk {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (j i : ℕ) (hj : j < (S.concat T).length + 1) (hi : i < T.length + 1) : j = S.length + i → (S.concat T).strictTransformSeq I ⟨j, hj⟩ ≍ T.strictTransformSeq (S.strictTransformSeq I (Fin.last S.length)) ⟨i, hi⟩

The strict transform along a concatenation at an index j = S.length + i, heterogeneously.

theorem AlgebraicGeometry.totalTransformSeq_concat_heq_mk {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (E : X.DivisorFamily) (j i : ℕ) (hj : j < (S.concat T).length + 1) (hi : i < T.length + 1) : j = S.length + i → (S.concat T).totalTransformSeq E ⟨j, hj⟩ ≍ T.totalTransformSeq (S.totalTransformSeq E (Fin.last S.length)) ⟨i, hi⟩

The total transform along a concatenation at an index j = S.length + i, heterogeneously.

Below the first sequence's length

theorem AlgebraicGeometry.stage_concat_mk_of_le {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (j : ℕ) (hj : j < (S.concat T).length + 1) (hj' : j < S.length + 1) : (S.concat T).stage ⟨j, hj⟩ = S.stage ⟨j, hj'⟩

The stage of a concatenation at an index j ≤ S.length is the stage j of the first sequence.

theorem AlgebraicGeometry.center_concat_heq_mk_of_lt {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (j : ℕ) (hj : j < (S.concat T).length) (hj' : j < S.length) : (S.concat T).center ⟨j, hj⟩ ≍ S.center ⟨j, hj'⟩

The centre of a concatenation at an index j < S.length is the centre j of the first sequence, heterogeneously.

theorem AlgebraicGeometry.markedTransformSeq_concat_heq_mk_of_le {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (m j : ℕ) (hj : j < (S.concat T).length + 1) (hj' : j < S.length + 1) : (S.concat T).markedTransformSeq I m ⟨j, hj⟩ ≍ S.markedTransformSeq I m ⟨j, hj'⟩

The marked transform along a concatenation at an index j ≤ S.length is the marked transform along the first sequence, heterogeneously.

theorem AlgebraicGeometry.strictTransformSeq_concat_heq_mk_of_le {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (j : ℕ) (hj : j < (S.concat T).length + 1) (hj' : j < S.length + 1) : (S.concat T).strictTransformSeq I ⟨j, hj⟩ ≍ S.strictTransformSeq I ⟨j, hj'⟩

The strict transform along a concatenation at an index j ≤ S.length, heterogeneously.

theorem AlgebraicGeometry.totalTransformSeq_concat_heq_mk_of_le {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (E : X.DivisorFamily) (j : ℕ) (hj : j < (S.concat T).length + 1) (hj' : j < S.length + 1) : (S.concat T).totalTransformSeq E ⟨j, hj⟩ ≍ S.totalTransformSeq E ⟨j, hj'⟩

The total transform along a concatenation at an index j ≤ S.length, heterogeneously.