The centers of a concatenation lie over a given set

The centers of S.concat T lie over a set Z ⊆ X when those of S do and those of T do after S.composite. This is the form of forall_center_concat (Hironaka/Scheme/BlowUpSequence/ConcatApi.lean) that involves the stage maps rather than the center ideals alone; it is used when the composite of a blow-up sequence whose centers lie over the singular locus is rewritten as a single blow-up with a suitably chosen center, as in the remark following Main Theorem I in [Hir64, pp. 132–133].

theorem AlgebraicGeometry.forall_center_concat_mem {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (Z : Set ↥X) : (∀ (i : Fin S.length), ∀ z ∈ (S.center i).support, (S.stageMap i.castSucc) z ∈ Z) → (∀ (i : Fin T.length), ∀ z ∈ (T.center i).support, S.composite ((T.stageMap i.castSucc) z) ∈ Z) → ∀ (i : Fin (S.concat T).length), ∀ z ∈ ((S.concat T).center i).support, ((S.concat T).stageMap i.castSucc) z ∈ Z

The centers of a concatenation lie over Z when those of S do and those of T do after S.composite (structural recursion on S: the first center of cons X D rest is D under 𝟙 X, the others are those of rest.concat T followed by D.blowUpπ).