Claim 71.2: the induction step through a hypersurface

Kollár's proof of Claim 71.2 [Kol07, 108] reduces, locally on X, to a chain of hypersurfaces Y = Y₀ ⊂ Y₁ ⊂ ⋯ ⊂ Y_c = X and treats one hypersurface at a time. Here the chain is walked by induction on the stage of the tower: at stage n + 1, one step of the chain (HypersurfaceCover, a smooth hypersurface H ⊂ X' containing Y' on a surjective coproduct of open subschemes) reduces the identity for Y ⊂ X to the hypersurface case for H ⊂ X' (Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingHypersurface) and to the identity for Y' ⊂ H at stage n (dim H ≤ n, the coherence of the tower moving the value between the stages), then descends along the cover. This module holds:

• seq_eq_pushforward_of_isEmpty — the trivial case Y = ∅: then J = 𝒪_Y, I = 𝒪_X, and both sides are the empty sequence (every stage).
• seq_eq_pushforward_of_hasDimLE_zero — the base of the induction, stage 0: both sides are empty (seq_eq_nil_of_hasDimLE_zero).
• seq_eq_pushforward_of_hypersurfaceCover — the induction step: given the identity at stage n for every closed embedding of marked triples with E = ∅, and a hypersurface cover of Y ⊂ X, the identity holds for Y ⊂ X at stage n + 1.
• seq_eq_pushforward_of_maxOrd_ker_le_one — the step assembled with the cover's existence: for Y nowhere dense (max-ord(ker j) ≤ 1) the identity at stage n + 1 follows from the identity at stage n.

The remaining case of the induction step — max-ord(ker j) = ⊤, a component of X inside Y — is Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingCodimZero.

theorem Hironaka.Stage.seq_eq_pushforward_of_isEmpty {k : Type u} [Field k] [CharZero k] (base : OrderReductionStage 0) (n : ℕ) (TX TY : MarkedTriple k) (j : TY.X.left ⟶ TX.X.left) [AlgebraicGeometry.IsClosedImmersion j] (hj : TX.ClosedEmbedding TY j) (hTX : MarkedTriple.BMOClass n 1 TX) (hY : IsEmpty ↥TY.X.left) : (((tower base n).bmo 1).functor k).seq TX hTX = ((((tower base n).bmo 1).functor k).seq TY ⋯).pushforward j

The boundary case Y = ∅ of Claim 71.2, at every stage: with Y empty, J = 𝒪_Y and I = τ_* J = 𝒪_X, so both BMO_1(X, I, 1, ∅) and τ_* BMO_1(Y, J, 1, ∅) are the empty sequence (eq_nil_of_isOrderGeSeq_of_maxOrd_lt, pushforward_nil).

theorem Hironaka.Stage.seq_eq_pushforward_of_hasDimLE_zero {k : Type u} [Field k] [CharZero k] (base : OrderReductionStage 0) (TX TY : MarkedTriple k) (j : TY.X.left ⟶ TX.X.left) [AlgebraicGeometry.IsClosedImmersion j] (hj : TX.ClosedEmbedding TY j) (hTX : MarkedTriple.BMOClass 0 1 TX) : (((tower base 0).bmo 1).functor k).seq TX hTX = ((((tower base 0).bmo 1).functor k).seq TY ⋯).pushforward j

The base of the induction ([Kol07, 70], dimension 0): at stage 0 both sides of Claim 71.2 are the empty sequence.

theorem Hironaka.Stage.seq_eq_pushforward_of_hypersurfaceCover {k : Type u} [Field k] [CharZero k] (base : OrderReductionStage 0) {n : ℕ} (ih : ∀ (TX₀ TY₀ : MarkedTriple k) (j₀ : TY₀.X.left ⟶ TX₀.X.left) [inst : AlgebraicGeometry.IsClosedImmersion j₀] (hj₀ : TX₀.ClosedEmbedding TY₀ j₀), IsEmpty TX₀.E.ι → ∀ (hTX₀ : MarkedTriple.BMOClass n 1 TX₀), (((tower base n).bmo 1).functor k).seq TX₀ hTX₀ = ((((tower base n).bmo 1).functor k).seq TY₀ ⋯).pushforward j₀) (TX TY : MarkedTriple k) (j : TY.X.left ⟶ TX.X.left) [AlgebraicGeometry.IsClosedImmersion j] (hj : TX.ClosedEmbedding TY j) (hTX : MarkedTriple.BMOClass (n + 1) 1 TX) (c : HypersurfaceCover n TX TY j) : (((tower base (n + 1)).bmo 1).functor k).seq TX hTX = ((((tower base (n + 1)).bmo 1).functor k).seq TY ⋯).pushforward j

One step of the chain of [Kol07, 108]: given the identity of Claim 71.2 at stage n for every closed embedding of marked triples with E = ∅, and a hypersurface cover of Y ⊂ X (a smooth hypersurface H ⊂ X' containing Y' on a surjective coproduct of open subschemes X' → X), the identity holds for Y ⊂ X at stage n + 1: on X' it is the hypersurface case for H ⊂ X' composed with the identity for Y' ⊂ H at stage n (dim H ≤ n; the values at H and Y' moved between the stages by tower_bmo_coherent), push-forwards composing along j' = ℓ ≫ (H ↪ X') [Kol07, Definition 30.3]; then it descends along the cover (seq_eq_pushforward_of_cover).

theorem Hironaka.Stage.seq_eq_pushforward_of_maxOrd_ker_le_one {k : Type u} [Field k] [CharZero k] (base : OrderReductionStage 0) {n : ℕ} (ih : ∀ (TX₀ TY₀ : MarkedTriple k) (j₀ : TY₀.X.left ⟶ TX₀.X.left) [inst : AlgebraicGeometry.IsClosedImmersion j₀] (hj₀ : TX₀.ClosedEmbedding TY₀ j₀), IsEmpty TX₀.E.ι → ∀ (hTX₀ : MarkedTriple.BMOClass n 1 TX₀), (((tower base n).bmo 1).functor k).seq TX₀ hTX₀ = ((((tower base n).bmo 1).functor k).seq TY₀ ⋯).pushforward j₀) (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) : (((tower base (n + 1)).bmo 1).functor k).seq TX hTX = ((((tower base (n + 1)).bmo 1).functor k).seq TY ⋯).pushforward j

[Kol07, 108]: for Y nowhere dense in X (max-ord(ker j) ≤ 1), the identity of Claim 71.2 at stage n + 1 follows from the identity at stage n — the hypersurface cover exists (exists_hypersurfaceCover) and the step applies; an empty X is the boundary case.