The original components inside the total transform

The total transform at stage i of a blow-up sequence ([Kol07, Definition 25], with the exceptional divisors appended last as in [Kol07, Definition 65]) lists the birational transforms (π_0 ⋯ π_{i-1})^{-1}_* E_a of the original components followed by the exceptional divisors; BlowUpSequence.originalIdx S E i is the index of the transform of E_a. Two facts about it, both by the recursion that defines totalTransformSeq: distinct components have distinct indices, and the component at the index of E_a is the strict transform of E_a along the sequence (strictTransformSeq, the birational transform of [Kol07, 30.2]).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.originalIdx_injective {X : Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (i : Fin (S.length + 1)) : Function.Injective (S.originalIdx E i)

Distinct components have distinct indices in the total transform.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.component_originalIdx {X : Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (i : Fin (S.length + 1)) (a : E.ι) : (S.totalTransformSeq E i).component (S.originalIdx E i a) = S.strictTransformSeq (E.component a) i

The component of the total transform at the index of E_a is the birational transform (π_0 ⋯ π_{i-1})^{-1}_* E_a [Kol07, Definition 25].