The last stage of a prefix is a stage of the sequence

The truncation S.take n (Hironaka/Scheme/BlowUpSequence/Truncate.lean) has the stages and the induced data of S up to n, stated there index by index as heterogeneous equalities (stage_take_mk, markedTransformSeq_take_heq_mk, …). The embedded resolution reads a prefix run.take n₀ of a run of the order reduction functor (the blow-up sequence the functor assigns to a triple) at its last stage (Fin.last), while the clauses about the run (the order condition of [Kol07, Definition 66], the stop rule CenterContains, the behaviour off the centers) are stated at the run's stage ⟨n₀, _⟩. This module restates the truncation lemmas at the last stage of the prefix, for n ≤ S.length: (S.take n).last = S.stage ⟨n, _⟩, and the heterogeneous equalities of the marked, strict and total transforms and of the stage map there. A proposition is transported across them by generalizing the scheme, as in ord_cast_of_heq of Truncate.lean.

theorem AlgebraicGeometry.lt_length_take_succ {X : Scheme} (S : X.BlowUpSequence) {n : ℕ} (hn : n ≤ S.length) : n < (S.take n).length + 1

The length of the prefix S.take n, n ≤ S.length, is n; hence n < (S.take n).length + 1.

theorem AlgebraicGeometry.fin_last_take_eq {X : Scheme} (S : X.BlowUpSequence) {n : ℕ} (hn : n ≤ S.length) : Fin.last (S.take n).length = ⟨n, ⋯⟩

The last index of the prefix, as the index ⟨n, _⟩.

theorem AlgebraicGeometry.stage_take_last {X : Scheme} (S : X.BlowUpSequence) {n : ℕ} (hn : n ≤ S.length) : (S.take n).last = S.stage ⟨n, ⋯⟩

The last stage of the prefix S.take n is the stage n of S.

theorem AlgebraicGeometry.markedTransformSeq_take_last_heq {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (c : ℕ) {n : ℕ} (hn : n ≤ S.length) : (S.take n).markedTransformSeq J c (Fin.last (S.take n).length) ≍ S.markedTransformSeq J c ⟨n, ⋯⟩

The marked transform at the last stage of the prefix is the marked transform at stage n.

theorem AlgebraicGeometry.strictTransformSeq_take_last_heq {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) {n : ℕ} (hn : n ≤ S.length) : (S.take n).strictTransformSeq J (Fin.last (S.take n).length) ≍ S.strictTransformSeq J ⟨n, ⋯⟩

The strict transform at the last stage of the prefix is the strict transform at stage n.

theorem AlgebraicGeometry.totalTransformSeq_take_last_heq {X : Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) {n : ℕ} (hn : n ≤ S.length) : (S.take n).totalTransformSeq E (Fin.last (S.take n).length) ≍ S.totalTransformSeq E ⟨n, ⋯⟩

The total transform of a family at the last stage of the prefix is the one at stage n.

theorem AlgebraicGeometry.composite_take_heq {X : Scheme} (S : X.BlowUpSequence) {n : ℕ} (hn : n ≤ S.length) : (S.take n).composite ≍ S.stageMap ⟨n, ⋯⟩

The composite of the prefix is the stage map at stage n.