CP3 along Step 2.1

Step 2.1 of the proof of [Kol07, Theorem 103] (item 104, Step 2.1) passes over the members Eʲ of the boundary in order, each pass being the output BD_{N,1,j} of [Kol07, Lemma 102] on the triple induced at the end of the previous ones (step21Seq, Hironaka.Resolution.Algebraic.OrderReduction.Step21BoundaryClearing). For the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): CP3 along each pass is cp3For_rawSeq_member (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Raw), since the value of the functor bdData at the mark 1 is rawSeq on the tuned triple with its empty blow-ups deleted (dataFunctor_seq_of_maxOrd_eq, functor_seq, cp3For_eraseEmpty; below the mark the output is empty), and the passes concatenate (cp3For_concat). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower.

theorem Hironaka.Resolution.cp3For_rawSeq_member_of_eq_one {k : Type u} [Field k] [CharZero k] {N : ℕ} {Dom' : MarkedTriple k → Prop} (B' : OrderGeSeqAssignment k Dom') (T : AlgebraicGeometry.Triple k) (j : T.E.ι) (m : ℕ) (hm1 : m = 1) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m) (hmax : T.I.maxOrd = ↑m) (hn : T.HasDimLE N) (hDom' : ∀ (T' : MarkedTriple k), T'.HasDimLE (N - 1) → T'.m = m → Dom' T') (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom' T'), T'.m = 1 → CP3For (B'.seq T' hT') T'.I T'.E) : CP3For (BD.rawSeq T m j hI hmax hn B' hDom') T.I T.E

cp3For_rawSeq_member with the mark carried as a variable equal to 1: the form the tuned triple of bdData produces (its mark is tuningParam 1).

theorem Hironaka.Resolution.cp3For_bdData_seq {k : Type u} [Field k] [CharZero k] {N : ℕ} (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (N - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) {j : ℕ} (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass N 1 j T) (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → CP3For ((B k).seq T' hT') T'.I T'.E) : CP3For (((BD.bdData N 1 j Dom B ⋯ hB hsm hbc).functor k).seq T hT) T.I T.E

CP3 along the output of BD_{N,1,j} on a triple of its class ([Kol07, Lemma 102] with the data bdData at the mark 1; the deletion of empty blow-ups of [Kol07, 32]): below the mark the output is empty; at the mark the tuning is the identity (W_tuningParam_one) and the value is rawSeq on the tuned triple with its empty blow-ups deleted (cp3For_eraseEmpty).

theorem Hironaka.Resolution.cp3For_step21Seq {k : Type u} [Field k] [CharZero k] {N : ℕ} (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (N - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE N) (hmax : T.I.maxOrd ≤ 1) (hcp3 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → CP3For ((B k).seq T' hT') T'.I T'.E) (j : ℕ) : CP3For (↑(BO.step21Seq T hn hmax (fun (j : ℕ) => BD.bdData N 1 j Dom B ⋯ hB hsm hbc) j)) T.I T.E

CP3 along Step 2.1 ([Kol07, 104, Step 2.1]): the passes over the members in order, each the output of Lemma 102 on the triple induced at the end of the previous passes (bdClass_induced_last), concatenated (cp3For_concat; the ideal of the induced triple is the weak transform, which is the marked transform at the mark 1, [Kol07, Remark 67]).