Step 2.2 of order reduction: its values and the order condition for the original boundary

The unfoldings of the definitions of Hironaka/Resolution/Algebraic/OrderReduction/Step22RestrictToHypersurface.lean and the two facts about the boundary of Step 2.2 that the construction needs.

• The re-tuning (step22Functor_seq_of_maxOrd_eq, step22Functor_seq_of_maxOrd_lt): at the mark, the boundary-clearing functor of [Kol07, Lemma 102] through the re-tuning is the functor at s(m) on the tuned triple; below the mark it is the empty sequence (ofTunedClass_seq_of_maxOrd_eq, ofTunedClass_seq_of_maxOrd_lt instantiated).
• The values of Step 2.2 (step22Triple_X, step22Triple_I, step22Triple_E, step22_eq, step22_of_maxOrd_eq, step22_of_maxOrd_lt) and the two fields of the functor (isOrderSeq_step22, a smooth blow-up sequence of order m for (I_r, F_r + H_r); noEmptyCenters_step22).
• The original boundary sees the same centres ([Kol07, 104, Step 2.2]): at a point of cosupp(I_r, m) no birational transform of an original member of E passes (notOriginal_of_mem_cosupp_step21, from Hironaka/Resolution/Algebraic/OrderReduction/Step21Disjoint.lean), so every member of E_r through the point is a member of F_r: E_r subdivides F_r + H_r along the cosupport (subdividesOn_cosupp_exceptionalFamily_append), and Step 2.2 is a smooth blow-up sequence of order m for the original (I_r, E_r) (isOrderSeq_step22_totalTransformSeq, through isOrderSeq_of_subdividesOn_cosupp). This is what makes Step 2 a sequence of order m for (X, I, E) in Hironaka/Resolution/Algebraic/OrderReduction/Step22Assembly.lean.

theorem Hironaka.BO.step22Functor_seq_of_maxOrd_eq {k : Type u} [Field k] [CharZero k] {n : ℕ} (bd : (m j : ℕ) → BDData n m j) (m j : ℕ) (hm : 1 ≤ m) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd = ↑m) : (step22Functor bd m j hm).seq T hT = ((bd (IsLocalRing.tuningParam m) j).functor k).seq (T.tuned m hm) ⋯

At the mark, the re-tuned boundary-clearing functor is the functor at s(m) on the tuned triple ([Kol07, 104, Step 2.2]: "we can again replace I by W(I)").

theorem Hironaka.BO.step22Functor_seq_of_maxOrd_lt {k : Type u} [Field k] [CharZero k] {n : ℕ} (bd : (m j : ℕ) → BDData n m j) (m j : ℕ) (hm : 1 ≤ m) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd < ↑m) : (step22Functor bd m j hm).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

Below the mark, the re-tuned boundary-clearing functor is the empty sequence (the remark after [Kol07, Theorem 68]).

theorem Hironaka.BO.notOriginal_of_mem_cosupp_step21 {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) {x : ↥((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).stage (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length))} (hx : ↑m ≤ ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).weakTransformSeq T.I (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)).ord x) {b : ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).totalTransformSeq T.E (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)).ι} (hb : x ∈ (((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).totalTransformSeq T.E (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)).component b).support) (a : T.E.ι) : b ≠ (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).originalIdx T.E (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length) a

At a point of cosupp(I_r, m) no member of E_r through the point is the birational transform of an original member of E: these transforms are disjoint from the cosupport after Step 2.1 (disjoint_cosupp_step21_final).

theorem Hironaka.BO.step22Triple_X {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : (step22Triple T hn hmax bd hm hH hle).X.left = (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).stage (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)

The Step 2.2 input triple lives on the end result X_r of Step 2.1.

theorem Hironaka.BO.step22Triple_I {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : (step22Triple T hn hmax bd hm hH hle).I = (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).weakTransformSeq T.I (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)

The ideal of the Step 2.2 input triple is I_r = Π⁻¹_* I.

theorem Hironaka.BO.step22Triple_E {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : (step22Triple T hn hmax bd hm hH hle).E = ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).exceptionalFamily T.E).append ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).strictTransformSeq H (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length))

The boundary of the Step 2.2 input triple is the exceptional sub-family of E_r with H_r appended last.

theorem Hironaka.BO.step22_eq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : step22 T hn hmax bd hm hH hle = (step22Functor bd m (Fintype.card ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).exceptionalFamily T.E).ι) hm).seq (step22Triple T hn hmax bd hm hH hle) ⋯

Step 2.2 is the re-tuned boundary-clearing functor at the position of H_r applied to the input triple (definitional).

theorem Hironaka.BO.step22_of_maxOrd_eq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (h : (step22Triple T hn hmax bd hm hH hle).I.maxOrd = ↑m) : step22 T hn hmax bd hm hH hle = ((bd (IsLocalRing.tuningParam m) (Fintype.card ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).exceptionalFamily T.E).ι)).functor k).seq ((step22Triple T hn hmax bd hm hH hle).tuned m hm) ⋯

At the mark, Step 2.2 is the boundary-clearing functor at s(m) on the tuned input triple ([Kol07, 104, Step 2.2]).

theorem Hironaka.BO.step22_of_maxOrd_lt {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (h : (step22Triple T hn hmax bd hm hH hle).I.maxOrd < ↑m) : step22 T hn hmax bd hm hH hle = AlgebraicGeometry.Scheme.BlowUpSequence.nil (step22Triple T hn hmax bd hm hH hle).X.left

Below the mark, the cosupport being already empty after Step 2.1, Step 2.2 is the empty sequence.

theorem Hironaka.BO.isOrderSeq_step22 {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : (step22 T hn hmax bd hm hH hle).IsOrderSeq ((step22Triple T hn hmax bd hm hH hle).X.left ↘ AlgebraicGeometry.Spec ↧k) (step22Triple T hn hmax bd hm hH hle).I (step22Triple T hn hmax bd hm hH hle).E m

Step 2.2 is a smooth blow-up sequence of order m starting with the input triple (X_r, I_r, F_r + H_r) (the functor's field).

theorem Hironaka.BO.noEmptyCenters_step22 {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : (step22 T hn hmax bd hm hH hle).NoEmptyCenters

Step 2.2 has no empty blow-up ([Kol07, 32]; the functor's field).

theorem Hironaka.BO.subdividesOn_cosupp_exceptionalFamily_append {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) {H : T.X.left.IdealSheafData} : ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).totalTransformSeq T.E (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)).SubdividesOn (((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).exceptionalFamily T.E).append ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).strictTransformSeq H (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length))) {x : ↥((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).stage (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)) | ↑m ≤ ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).weakTransformSeq T.I (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)).ord x}

Along cosupp(I_r, m) the boundary E_r subdivides F_r + H_r: every member of E_r through a point of the cosupport is exceptional (notOriginal_of_mem_cosupp_step21), hence a member of F_r, assigned to itself.

theorem Hironaka.BO.isOrderSeq_step22_totalTransformSeq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hn : T.HasDimLE n) (hmax : T.I.maxOrd ≤ ↑m) (bd : (m j : ℕ) → BDData n m j) (hm : 1 ≤ m) {H : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) : (step22 T hn hmax bd hm hH hle).IsOrderSeq ((step22Triple T hn hmax bd hm hH hle).X.left ↘ AlgebraicGeometry.Spec ↧k) (step22Triple T hn hmax bd hm hH hle).I ((↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).totalTransformSeq T.E (Fin.last (↑(step21Seq T hn hmax (bd m) (Fintype.card T.E.ι))).length)) m

Step 2.2 is a smooth blow-up sequence of order m for the original boundary (I_r, E_r): the normal-crossings clause of [Kol07, Definition 66] at its centres sees only the exceptional members (isOrderSeq_of_subdividesOn_cosupp).