Step 2.2 of order reduction: the cosupport is emptied

Step 2.2 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.2]) ends with a sequence Π : X_r → X whose cosupport cosupp Π⁻¹_*(I, m) is disjoint from Π⁻¹_* H; as H is a smooth hypersurface of maximal contact, the cosupport lies in Π⁻¹_* H, hence is empty.

• Clause (1) of [Kol07, Lemma 102] at the position of H_r (disjoint_cosupp_step22): at the mark, the disjointness field of the boundary-clearing data for the tuned input triple at s(m), with H_r the last member (nth_append_last), read back to the mark m for I_r by Hironaka.BD.le_ord_weakTransformSeq_iff_tuned (the cosupports agree stage by stage); below the mark the sequence is empty and cosupp(I_r, m) is already empty.
• The containment (isMaximalContact_step22_H, cosupp_step22_subset_H): Kollár's "by definition" is the maximal contact of the final transform of H_r (IsOrderSeq.isMaximalContact_strictTransformSeq along Step 2.2, from the maximal contact of H_r for I_r established in Hironaka/Resolution/Algebraic/OrderReduction/Step21MaximalContact.lean), read through Kol07, Definition 79 (mem_support_MC_iff: cosupp MC(I) = cosupp(I, m)) and the antitonicity of supports in the ideal at the stalks.
• The conclusion (cosupp_step22_eq_empty, maxOrd_step22_lt): a set disjoint from a set containing it is empty, and max-ord < m is maxOrd_lt_iff_forall_ord_lt. This is clause (1) of [Kol07, Theorem 103] for Step 2.

theorem Hironaka.BO.disjoint_cosupp_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) : Disjoint {x : ↥((step22 T hn hmax bd hm hH hle).stage (Fin.last (step22 T hn hmax bd hm hH hle).length)) | ↑m ≤ ((step22 T hn hmax bd hm hH hle).weakTransformSeq (step22Triple T hn hmax bd hm hH hle).I (Fin.last (step22 T hn hmax bd hm hH hle).length)).ord x} ↑((step22 T hn hmax bd hm hH hle).strictTransformSeq ((↑(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)) (Fin.last (step22 T hn hmax bd hm hH hle).length)).support

Clause (1) of [Kol07, Lemma 102] at the position of H_r, read back to the mark m ([Kol07, 104, Step 2.2]: "cosupp Π⁻¹_*(I, m) is disjoint from Π⁻¹_* H").

theorem Hironaka.BO.isMaximalContact_step22_H {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) : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (CategoryTheory.CategoryStruct.comp ((step22 T hn hmax bd hm hH hle).stageMap (Fin.last (step22 T hn hmax bd hm hH hle).length)) ((step22Triple T hn hmax bd hm hH hle).X.left ↘ AlgebraicGeometry.Spec ↧k)) ((step22 T hn hmax bd hm hH hle).weakTransformSeq (step22Triple T hn hmax bd hm hH hle).I (Fin.last (step22 T hn hmax bd hm hH hle).length)) m ((step22 T hn hmax bd hm hH hle).strictTransformSeq ((↑(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)) (Fin.last (step22 T hn hmax bd hm hH hle).length))

The transform of H_r at the end of Step 2.2 is of maximal contact for the final ideal ([Kol07, 104, Step 2.2]: "H is a smooth hypersurface of maximal contact"), by IsOrderSeq.isMaximalContact_strictTransformSeq from the maximal contact of H_r for I_r.

theorem Hironaka.BO.cosupp_step22_subset_H {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) : {x : ↥((step22 T hn hmax bd hm hH hle).stage (Fin.last (step22 T hn hmax bd hm hH hle).length)) | ↑m ≤ ((step22 T hn hmax bd hm hH hle).weakTransformSeq (step22Triple T hn hmax bd hm hH hle).I (Fin.last (step22 T hn hmax bd hm hH hle).length)).ord x} ⊆ ↑((step22 T hn hmax bd hm hH hle).strictTransformSeq ((↑(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)) (Fin.last (step22 T hn hmax bd hm hH hle).length)).support

The cosupport of the final ideal lies in the transform of H_r ([Kol07, 104, Step 2.2]: "hence, by definition, cosupp Π⁻¹_*(I, m) ⊂ Π⁻¹_* H"; [Kol07, Definition 79]).

theorem Hironaka.BO.cosupp_step22_eq_empty {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) : {x : ↥((step22 T hn hmax bd hm hH hle).stage (Fin.last (step22 T hn hmax bd hm hH hle).length)) | ↑m ≤ ((step22 T hn hmax bd hm hH hle).weakTransformSeq (step22Triple T hn hmax bd hm hH hle).I (Fin.last (step22 T hn hmax bd hm hH hle).length)).ord x} = ∅

The cosupport of the final ideal of Step 2.2 is empty ([Kol07, 104, Step 2.2]: "thus cosupp Π⁻¹_*(I, m) = ∅").

theorem Hironaka.BO.maxOrd_step22_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) : ((step22 T hn hmax bd hm hH hle).weakTransformSeq (step22Triple T hn hmax bd hm hH hle).I (Fin.last (step22 T hn hmax bd hm hH hle).length)).maxOrd < ↑m

The final ideal of Step 2.2 has max-ord < m: clause (1) of [Kol07, Theorem 103] after Step 2.2 ("as we wanted").