Positions of the original members in the total transform

In the total transform of a divisor family along a blow-up [Kol07, Definition 65] the exceptional divisor is "added as the last divisor": here the index set becomes Lex (ι ⊕ PUnit). So the first card E.ι positions of totalTransformSeq E i are the birational transforms of the original members, position by position (nth_totalTransformSeq_of_lt): the j-th member of the total transform (in the order of the index set, through monoEquivOfFin; DivisorFamily.nth) at a position j < card E.ι is the strict transform of the j-th member of E. The one fact about finite linear orders this needs: in a lexicographic sum α ⊕ₗ β the j-th element, for j < card α, is inl of the j-th element of α (monoEquivOfFin_lex_inl). Every inl precedes every inr, so an inr at position j would leave only j < card α positions for the card α elements inl a; the resulting map Fin (card α) → α is strictly monotone into α, hence Mathlib's unique increasing enumeration (Finset.orderEmbOfFin_unique).

This is what lets the boundary-clearing step of the proof of Theorem 103 [Kol07, 104, Step 2.1] speak of the transform of the j-th original member at every stage.

theorem Hironaka.Sequence.monoEquivOfFin_lex_inl {α : Type u_1} {β : Type u_2} [Fintype α] [LinearOrder α] [Fintype β] [LinearOrder β] {j : ℕ} (hj : j < Fintype.card α) (hj' : j < Fintype.card (α ⊕ₗ β)) : (monoEquivOfFin (α ⊕ₗ β) ⋯) ⟨j, hj'⟩ = toLex (Sum.inl ((monoEquivOfFin α ⋯) ⟨j, hj⟩))

In a lexicographic sum of finite linear orders, the j-th element for j < card α is inl of the j-th element of α; the finite-order fact behind "new divisors come after old ones" [Kol07, Definition 65].

theorem Hironaka.Sequence.card_le_card_ι_totalTransform {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (D : X.IdealSheafData) : Fintype.card E.ι ≤ Fintype.card (E.totalTransform D).ι

card E.ι ≤ card (E.totalTransform D).ι: one member is appended [Kol07, Definition 65].

theorem Hironaka.Sequence.nth_totalTransform_inl {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (D : X.IdealSheafData) {j : ℕ} (hj : j < Fintype.card E.ι) (hj' : j < Fintype.card (E.totalTransform D).ι) : (E.totalTransform D).nth ⟨j, hj'⟩ = (E.nth ⟨j, hj⟩).strictTransform D

The exceptional divisor is added as the last member [Kol07, Definition 65], so for one blow-up the j-th member of the total transform, j < card E.ι, is the strict transform of the j-th member of E.

theorem Hironaka.Sequence.nth_totalTransformSeq_of_lt {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (i : Fin (S.length + 1)) {j : ℕ} (hj : j < Fintype.card E.ι) : (S.totalTransformSeq E i).nth ⟨j, ⋯⟩ = S.strictTransformSeq (E.nth ⟨j, hj⟩) i

The first card E.ι positions of the total transform at any stage are the birational transforms of the original members, position by position [Kol07, Definition 65].