Step 2.3 of order reduction: independence of the hypersurface of maximal contact

Step 2.3 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.3]) addresses the choice made in Step 2.2: the hypersurface of maximal contact H is not unique, and for two of them, H and H', with H + E and H' + E having simple normal crossings, either boundary-clearing sequence BD_{n,m,0}(X, I, H + E), BD_{n,m,0}(X, I, H' + E) could serve to construct BO_{n,m}(X, I, E). Kollár's argument uses that I is MC-invariant: by [Kol07, Theorem 92] the triples (X, I, H + E) and (X, I, H' + E) are then étale equivalent, hence so are the two blow-up sequences, and by [Kol07, Theorem 97] étale equivalent blow-up sequences are identical.

Here the two Step 2.2 sequences are the boundary-clearing functor of [Kol07, Lemma 102] (bd (s m) j, at the position j of the hypersurface, last in the boundary) applied to the tuned Step 2.2 triples (step22Triple T … H).tuned m hm and (step22Triple T … H').tuned m hm: the same X_r, the same tuned ideal W_{s(m)}(I_r), MC-invariant by isMCInvariant_tuned, the same exceptional sub-family F_r, and the transforms H_r, H'_r of the two hypersurfaces, both of maximal contact for the tuned ideal at the mark s(m) (isMaximalContact_step21_H re-tuned by retune_keeps_maxContact); both boundaries F_r + H_r, F_r + H'_r have normal crossings everywhere (the field of step22Triple). Kollár's argument is then functor_independent_of_maximalContact_of_closed of Hironaka/Resolution/Algebraic/MaximalContact/FunctorIndependence.lean ([Kol07, Theorem 92] with an affine étale cover, the étale equivalence of the two functor outputs, [Kol07, Theorem 97]), applied to (bd (s m) j).functor k on the boundary-clearing class BDClass n (s m) j, which is closed under étale pull-backs covering the cosupport (bdClass_closedUnderEtalePullbackOverCosupp):

• step22_etaleEquivSeq_of_two_H: at the mark, the two boundary-clearing sequences are étale equivalent in the sense of [Kol07, Definition 96], the first half of that argument;
• step22_indep: Step 2.2 does not depend on the choice of H; at the mark by the argument above (the second Step 2.2 triple is the first with its last member replaced, a definitional identification up to structure eta), below the mark both sides are empty;
• step2Seq_indep, maxContactCase_indep: Step 2 and BO^H_{n,m} likewise, through the unfoldings step2Seq_eq, maxContactCase_of_maxOrd_eq and maxContactCase_of_maxOrd_lt.

Kollár's separate hypothesis "H + E and H' + E have simple normal crossings" is not needed: Step 2.1 supplies a boundary with normal crossings for every smooth hypersurface of maximal contact (Hironaka/Resolution/Algebraic/OrderReduction/Step21MaximalContact.lean). The independence makes BO_{n,m} well defined on the triples admitting a hypersurface of maximal contact, which Step 3 globalises (Hironaka/Resolution/Algebraic/OrderReduction/Step3Globalization.lean).

theorem Hironaka.BO.step22_etaleEquivSeq_of_two_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 H' : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (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) : Nonempty (AlgebraicGeometry.Scheme.IdealSheafData.EtaleEquivSeq ((step22Triple T hn hmax bd hm hH hle).X.left ↘ AlgebraicGeometry.Spec ↧k) ((step22Triple T hn hmax bd hm hH hle).tuned m hm).I (IsLocalRing.tuningParam m) (((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) ⋯) (((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, the two boundary-clearing sequences of Step 2.2 for H and H' are étale equivalent in the sense of [Kol07, Definition 96] ([Kol07, 104, Step 2.3]: the triples (X, I, H + E) and (X, I, H' + E) are étale equivalent by [Kol07, Theorem 92], hence so are their blow-up sequences): [Kol07, Theorem 92] on the tuned input with an affine étale cover (exists_etaleEquiv_isAffine), through etaleEquivSeq_of_functor and the closure of the boundary-clearing class under étale pull-backs covering the cosupport.

theorem Hironaka.BO.step22_indep {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 H' : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (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 = step22 T hn hmax bd hm hH' hle'

Step 2.2 does not depend on the choice of the hypersurface of maximal contact ([Kol07, 104, Step 2.3]: "by (97) … these blow-up sequences are identical"): at the mark by functor_independent_of_maximalContact_of_closed on the tuned Step 2.2 triple (the second triple is the first with its last member replaced), below the mark both sides are empty.

theorem Hironaka.BO.step2Seq_indep {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 H' : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (hH' : AlgebraicGeometry.IsSmoothDivisor H') (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H') : step2Seq T hn hmax bd hm hH hle = step2Seq T hn hmax bd hm hH' hle'

Step 2 does not depend on the choice of the hypersurface of maximal contact (step2Seq = S₁.concat step22).

theorem Hironaka.BO.maxContactCase_indep {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) {H H' : T.X.left.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hle : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H) (hH' : AlgebraicGeometry.IsSmoothDivisor H') (hle' : AlgebraicGeometry.Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m H') (bd : (m j : ℕ) → BDData n m j) : maxContactCase T hT hH hle bd = maxContactCase T hT hH' hle' bd

BO^H_{n,m}(X, I, E) = BO^{H'}_{n,m}(X, I, E) for any two smooth hypersurfaces of maximal contact ([Kol07, 104, Step 2.3]): BO_{n,m} is well defined on the triples admitting one. At the mark, Step 2 on the tuned triple with the re-tuned hypersurfaces (step2Seq_indep); below the mark both sides are empty.