The appended member of a divisor family is its last member

In the maximal contact case of the proof of Theorem 103, Kollár declares E^0 := H to be the first divisor of H + E and applies Lemma 102 with j = 0 [Kol07, 104, Step 2.2]. In this library DivisorFamily.append E J puts the new member last (its index set is E.ι ⊕ₗ PUnit, every inl before the inr), and DivisorFamily.nth counts positions from 0 in the linear order of the index set. So Kollár's position 0 is the position card E.ι here: (E.append J).nth ⟨card E.ι, _⟩ = J (nth_append_last). The finite-order fact behind it is that the last position of a lexicographic sum with a one-element right summand is that summand (monoEquivOfFin_lex_inr_last), the counterpart for inr of monoEquivOfFin_lex_inl.

theorem Hironaka.Sequence.monoEquivOfFin_lex_top {α : Type u_1} {β : Type u_2} [Fintype α] [LinearOrder α] [Fintype β] [LinearOrder β] [OrderTop β] (hpos : 0 < Fintype.card (α ⊕ₗ β)) : (monoEquivOfFin (α ⊕ₗ β) ⋯) ⟨Fintype.card (α ⊕ₗ β) - 1, ⋯⟩ = ⊤

The last position of a lexicographic sum of finite linear orders whose right summand has a top is the top: an order isomorphism Fin k ≃o α ⊕ₗ β sends the last index to the greatest element.

theorem Hironaka.Sequence.card_lex_punit (α : Type u_1) [Fintype α] : Fintype.card (α ⊕ₗ PUnit.{v + 1}) = Fintype.card α + 1

card (α ⊕ₗ PUnit) = card α + 1.

theorem Hironaka.Sequence.monoEquivOfFin_lex_inr_last {α : Type u_1} [Fintype α] [LinearOrder α] (h : Fintype.card α < Fintype.card (α ⊕ₗ PUnit.{v + 1})) : (monoEquivOfFin (α ⊕ₗ PUnit.{v + 1}) ⋯) ⟨Fintype.card α, h⟩ = toLex (Sum.inr PUnit.unit)

In α ⊕ₗ PUnit the element at position card α, the last one, is the inr; the counterpart for inr of monoEquivOfFin_lex_inl.

theorem Hironaka.Sequence.card_lt_card_ι_append {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (J : X.IdealSheafData) : Fintype.card E.ι < Fintype.card (E.append J).ι

One member is appended: card E.ι < card (E.append J).ι.

theorem Hironaka.Sequence.nth_append_last {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (J : X.IdealSheafData) (h : Fintype.card E.ι < Fintype.card (E.append J).ι) : (E.append J).nth ⟨Fintype.card E.ι, h⟩ = J

The appended member J of E.append J sits at the last position card E.ι (positions are counted from 0, new members come last). Kollár's instruction to "declare E^0 := H to be the first divisor in H + E" and apply Lemma 102 with j = 0 [Kol07, 104, Step 2.2] therefore reads j := card E.ι here.