Total transforms, marked transforms and pull-backs of ideals along a concatenation

concat glues a blow-up sequence S on X to a sequence T on its end result; Hironaka/Scheme/BlowUpSequence/ConcatApi.lean transports the composite, the weak transforms and the boundaries along it, and Hironaka/Scheme/BlowUpSequence/ConcatTransforms.lean the strict transforms. The embedded desingularization sequence of [Wlo05, Theorem 1.0.2] is a concatenation of truncated runs of the marked order reduction functor, one per round, and its clauses (c) and (e) read the final total transform of the boundary and the pull-back of the ideal of the subvariety to the end result, so three more transports are needed:

• totalTransformSeq_concat_last: the total transform of a divisor family along S.concat T is the total transform along T of the total transform along S ([Kol07, Definition 25], iterated), read at T.last through the cast eqToHom (last_concat S T), by the structural induction of weakTransformSeq_concat_last;
• markedTransformSeq_concat_last: likewise for the marked transform of [Kol07, Definition 66];
• comap_composite_concat: the pull-back of an ideal sheaf along the composite of S.concat T is the pull-back along T of the pull-back along S (composite_concat and the functoriality of comap).

Nothing here goes beyond the recursive definitions; the composition of the passes of the resolution algorithm is in [Wlo05, Theorem 4.7.1].

theorem AlgebraicGeometry.Scheme.BlowUpSequence.totalTransformSeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (E : X.DivisorFamily) : (S.concat T).totalTransformSeq E (Fin.last (S.concat T).length) = (T.totalTransformSeq (S.totalTransformSeq E (Fin.last S.length)) (Fin.last T.length)).comap (CategoryTheory.eqToHom ⋯)

The total transform of a divisor family along a concatenation is the iterated total transform [Kol07, Definition 25], read at the end result of the second sequence through the cast eqToHom (last_concat S T).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.markedTransformSeq_concat_last {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) : (S.concat T).markedTransformSeq I m (Fin.last (S.concat T).length) = (T.markedTransformSeq (S.markedTransformSeq I m (Fin.last S.length)) m (Fin.last T.length)).comap (CategoryTheory.eqToHom ⋯)

The marked transform along a concatenation is the iterated marked transform [Kol07, Definition 66, condition (1′)], read at the end result of the second sequence through the cast eqToHom (last_concat S T); the analogue of strictTransformSeq_concat_last for marked transforms.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.comap_composite_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) : I.comap (S.concat T).composite = ((I.comap S.composite).comap T.composite).comap (CategoryTheory.eqToHom ⋯)

The pull-back of an ideal sheaf along the composite of a concatenation is the pull-back along the second sequence of the pull-back along the first, read at T.last through the cast eqToHom (last_concat S T).