CP1 along Step 2, and the Step 2 descent along the tower

Step 2 of the proof of [Kol07, Theorem 103] on a triple with a smooth hypersurface of maximal contact is Step 2.1 followed by Step 2.2 (step2Seq, Hironaka.Resolution.Algebraic.OrderReduction.Step22RestrictToHypersurface). The statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along it (cp1For_step2Seq) is cp1For_concat of CP1 along Step 2.1 (cp1For_step21Seq; no centre there contains c̃) and CP1 along Step 2.2 at the lifted generic point (cp1For_step22). The tower step (cp1BOAt_succ_of_cp1BMOAt): BO_{n+1,1} is evaluated through the local cover of [Kol07, Theorem 105], on whose pieces a hypersurface of maximal contact exists and the run is Step 2 on the tuned triple (functor_seq_localClass, maxContactCase at max-ord I = 1, the tuning at the mark 1 being the identity); CP1 on the pieces descends to the triple (cp1For_of_pullback_cover, the functor commuting with the cover), and the inductive input is the stage-n marked family read through the amalgam (amalgam_seq, seq_congr_mark). The tower induction is that of [Kol07, 70]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Tower and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower.

theorem Hironaka.Resolution.cp1For_step2Seq {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) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 H) (hcp1 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → ∀ η' ∈ T'.I.support.genericPoints, (∀ (i : T'.E.ι), η' ∉ (T'.E.component i).support) → T'.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η' → CP1For ((B k).seq T' hT') T'.I T'.E η') {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (BO.step2Seq T hn hmax (fun (m j : ℕ) => BD.bdData N m j Dom B ⋯ hB hsm hbc) ⋯ hH hle) T.I T.E η

CP1 along Step 2 with the data bdData (Step 2 of the proof of [Kol07, Theorem 103]), from cp1For_step21Seq and cp1For_step22 through cp1For_concat.

theorem Hironaka.Resolution.cp1For_step2Seq_of_eq_one {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) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (m : ℕ) (hm1 : m = 1) (hmax' : T.I.maxOrd ≤ ↑m) (hm : 1 ≤ m) (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (hcp1 : ∀ (T' : MarkedTriple k) (hT' : Dom k T'), T'.m = 1 → ∀ η' ∈ T'.I.support.genericPoints, (∀ (i : T'.E.ι), η' ∉ (T'.E.component i).support) → T'.I.stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η' → CP1For ((B k).seq T' hT') T'.I T'.E η') {η : ↥T.X.left} (hη : η ∈ T.I.support.genericPoints) (hηE : ∀ (i : T.E.ι), η ∉ (T.E.component i).support) (hIc : T.I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : CP1For (BO.step2Seq T hn hmax' (fun (m j : ℕ) => BD.bdData N m j Dom B ⋯ hB hsm hbc) hm hH hle') T.I T.E η

cp1For_step2Seq at a mark m = 1 carried as a variable: the form the tuned triple of maxContactCase produces, whose mark is tuningParam 1.

theorem Hironaka.Resolution.cp1BOAt_succ_of_cp1BMOAt (k : Type u) [Field k] [CharZero k] (n : ℕ) (h : CP1BMOAt k n) : CP1BOAt k (n + 1)

The Step 2 descent along the tower (Step 2 of the proof of [Kol07, Theorem 103], [Kol07, Theorem 105], [Kol07, 104]): BO_{n+1,1} on a triple is evaluated through the local cover of Theorem 105, on whose pieces a hypersurface of maximal contact exists and the run is Step 2 on the tuned triple; CP1 there is cp1For_step2Seq with the stage-n marked family as the inductive input, and it descends to the triple along the cover.