Claim 71.2: the local reduction to a hypersurface

Kollár's proof of Claim 71.2 [Kol07, 108]: the identity is "a local question on X", so one may assume a chain of smooth subvarieties Y = Y₀ ⊂ Y₁ ⊂ ⋯ ⊂ Y_c = X, each a hypersurface in the next. This module produces ONE step of that chain, on a surjective coproduct of open subschemes of X (the "local question"), for a closed embedding j : Y ↪ X of smooth schemes with Y nowhere dense — the case max-ord(ker j) ≤ 1, i.e. ker j is nonzero on every component and of order 1 along Y:

• HypersurfaceCover TX TY j packages the data: a coproduct of open immersions g : X' → X (surjective, smooth), the cartesian square Y' = Y ×_X X' with its closed immersion j' and restriction h_S, the pulled-back marked triples TX', TY', a smooth hypersurface H ⊂ X' containing Y' with its marked triple TH' = (H, ℓ_* J', 1, ∅), and the factorization j' = ℓ ≫ (H ↪ X') — both H ⊂ X' and Y' ⊂ H being closed embeddings of marked triples with E = ∅, and dim H ≤ dim X − 1.
• exists_hypersurfaceCover builds it: the hypersurface is a hypersurface of maximal contact for (ker j, 1) — [Kol07, Theorem 80] for the ideal of Y itself at the mark 1, where MC(ker j, 1) = ker j (MC_one), so that H ≤ ker j says exactly Y ⊆ H. The local cover of the triple (X, ker j, ∅) for the class BO_{n,1} (exists_isLocalCover at globalizationData_localClass, Step 3 of the proof of [Kol07, Theorem 103]) supplies at once the surjective coproduct of open immersions g, the pulled-back triple, and such an H on the coproduct. The square is Mathlib's fibre product Y ×_X X' (pullback.fst, a closed immersion by base change, with kernel (ker j).comap g — ker_fst_of_isClosedImmersion); ℓ is the lift of j' through H ↪ X' (IsClosedImmersion.lift, since H ≤ ker j'); TH''s ideal ℓ_* J' is nonzero on every component by isNonzeroEverywhere_map_of_isClosedImmersion, its boundary is empty, and its dimension is one less than X''s (smoothOfRelativeDimension_of_isSmoothDivisor).

Kollár's sentence, read with Theorem 80 at (ker j, 1), is the whole content; every ingredient is a general lemma of the library.

structure Hironaka.Stage.HypersurfaceCover {k : Type u} [Field k] (n : ℕ) (TX TY : MarkedTriple k) (j : TY.X.left ⟶ TX.X.left) : Type (u + 1)

The data of one step of the local chain of [Kol07, 108]: on a surjective coproduct of open immersions g : X' → X, the pulled-back closed embedding j' : Y' → X' (a cartesian square over j) factors through a smooth hypersurface H ⊂ X' of X', j' = ℓ ≫ (H ↪ X'), both factors closed embeddings of marked triples with empty boundary.

• TX' : MarkedTriple k

  The marked triple of X'.

• TY' : MarkedTriple k

  The marked triple of Y' = Y ×_X X'.

• TH' : MarkedTriple k

  The marked triple of the hypersurface H, with the ideal ℓ_* J'.

• g : self.TX'.X.left ⟶ TX.X.left

  The cover g : X' → X, a coproduct of open immersions.

• smooth_g : AlgebraicGeometry.Smooth self.g
• surjective_g : Function.Surjective ⇑self.g
• j' : self.TY'.X.left ⟶ self.TX'.X.left

  The closed immersion Y' → X'.

• isClosedImmersion_j' : AlgebraicGeometry.IsClosedImmersion self.j'
• hS : self.TY'.X.left ⟶ TY.X.left

  The restriction Y' → Y of the cover.

• smooth_hS : AlgebraicGeometry.Smooth self.hS
• surjective_hS : Function.Surjective ⇑self.hS
• sq : CategoryTheory.IsPullback self.j' self.hS self.g j

  The cartesian square j' ≫ g = hS ≫ j.

• pullback_TX' : self.TX'.IsPullbackOf TX self.g
• pullback_TY' : self.TY'.IsPullbackOf TY self.hS
• Hι : self.TH'.X.left ⟶ self.TX'.X.left

  The hypersurface H ↪ X'.

• isClosedImmersion_Hι : AlgebraicGeometry.IsClosedImmersion self.Hι
• isSmoothDivisor_ker : AlgebraicGeometry.IsSmoothDivisor (AlgebraicGeometry.Scheme.Hom.ker self.Hι)
• ℓ : self.TY'.X.left ⟶ self.TH'.X.left

  The lift Y' → H of j'.

• isClosedImmersion_ℓ : AlgebraicGeometry.IsClosedImmersion self.ℓ
• fac : CategoryTheory.CategoryStruct.comp self.ℓ self.Hι = self.j'
• closedEmbedding_X' : self.TX'.ClosedEmbedding self.TH' self.Hι
• closedEmbedding_H : self.TH'.ClosedEmbedding self.TY' self.ℓ
• isEmpty_E' : IsEmpty self.TX'.E.ι
• hasDimLE_X' : self.TX'.HasDimLE (n + 1)

  X' has the dimension bound ≤ n + 1 of X.

• hasDimLE_H : self.TH'.HasDimLE n

  H has dimension ≤ n, one less than X.

theorem Hironaka.Stage.exists_hypersurfaceCover {k : Type u} [Field k] [CharZero k] {n : ℕ} (TX TY : MarkedTriple k) (j : TY.X.left ⟶ TX.X.left) [AlgebraicGeometry.IsClosedImmersion j] (hj : TX.ClosedEmbedding TY j) (hE : IsEmpty TX.E.ι) (hTX : MarkedTriple.BMOClass (n + 1) 1 TX) (hK : (AlgebraicGeometry.Scheme.Hom.ker j).maxOrd ≤ ↑1) [Nonempty ↥TX.X.left] : Nonempty (HypersurfaceCover n TX TY j)

[Kol07, 108] with [Kol07, Theorem 80] at (ker j, 1): for a closed embedding j : Y ↪ X of marked triples with E = ∅ and max-ord(ker j) ≤ 1 (Y nowhere dense in X, Y possibly empty), the data of one step of the local chain exist.