Composites, transforms and order conditions along a concatenation

Kollár's Π_{ij} bookkeeping [Kol07, Definition 29] for the concatenation S.concat T of Hironaka/Scheme/BlowUpSequence/Concat.lean: the end result is that of T (last_concat), the composite is Π_T ≫ Π_S (composite_concat), the weak transforms and boundaries after the whole sequence are those of T computed from those of S (weakTransformSeq_concat_last, boundarySeq_concat_last), a predicate holding on every center of S and of T holds on every center of S.concat T (forall_center_concat), and a smooth blow-up sequence of order d followed by one of order d for the induced triple is one of order d (isOrderSeq_concat, [Kol07, Definition 66]). The transport statements carry the identification eqToHom (last_concat S T) of the end results, an identity up to the definitional unfolding of last.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.last_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) : (S.concat T).last = T.last

The end result of a concatenation is the end result of the second sequence.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.composite_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) : (S.concat T).composite = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp T.composite S.composite)

The composite of a concatenation, Π_{S ++ T} = Π_T ≫ Π_S [Kol07, Definition 29].

theorem AlgebraicGeometry.Scheme.BlowUpSequence.weakTransformSeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (J : X.IdealSheafData) : (S.concat T).weakTransformSeq J (Fin.last (S.concat T).length) = (T.weakTransformSeq (S.weakTransformSeq J (Fin.last S.length)) (Fin.last T.length)).comap (CategoryTheory.eqToHom ⋯)

The weak transform at the end of a concatenation is the weak transform along T of the weak transform along S.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.boundarySeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (E₀ : X.IdealSheafData) : (S.concat T).boundarySeq E₀ (Fin.last (S.concat T).length) = (T.boundarySeq (S.boundarySeq E₀ (Fin.last S.length)) (Fin.last T.length)).comap (CategoryTheory.eqToHom ⋯)

The boundary (the reduced total transform of the boundary divisor) at the end of a concatenation is the boundary along T of the boundary along S.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.forall_center_concat {X : Scheme} (P : {Y : Scheme} → Y.IdealSheafData → Prop) (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (hS : ∀ (i : Fin S.length), P (S.center i)) (hT : ∀ (j : Fin T.length), P (T.center j)) (i : Fin (S.concat T).length) : P ((S.concat T).center i)

A predicate on closed subschemes that holds on every centre of S and of T holds on every centre of S.concat T.

theorem AlgebraicGeometry.isOrderSeq_concat {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) {J : X.IdealSheafData} {E : X.DivisorFamily} {d : ℕ} (hS : S.IsOrderSeq f J E d) (hT : T.IsOrderSeq (CategoryTheory.CategoryStruct.comp S.composite f) (S.weakTransformSeq J (Fin.last S.length)) (S.totalTransformSeq E (Fin.last S.length)) d) : (S.concat T).IsOrderSeq f J E d

A smooth blow-up sequence of order d for (X, J, E) followed by one of order d for the induced triple at its end result is a smooth blow-up sequence of order d for (X, J, E) [Kol07, Definition 66].