Claim 71.2, the hypersurface case #
Kollár's Claim 71.2 [Kol07, Claim 71.2] says that for a closed embedding τ : Y ↪ X of smooth
schemes with τ_*(𝒪_Y/J) = 𝒪_X/I, BMO_1(X, I, 1, ∅) = τ_* BMO_1(Y, J, 1, ∅). Its proof
[Kol07, 108] reduces it to the case of a hypersurface Y ⊂ X and proves that case in two lines:
every local equation of Y lies in I, so max-ord I = 1; hence
BMO_{dim X,1}(X, I, 1, ∅) = BO_{dim X,1}(X, I, ∅) by (107.3), and (103.3) gives
BO_{dim X,1}(X, I, ∅) = τ_* BMO_{dim Y,1}(Y, J, 1, ∅). This module is that case for the stage
functors of the tower: tower_bmo_one_eq_pushforward_of_isSmoothDivisor_ker, under the hypothesis
that the kernel j.ker of the closed immersion is a smooth divisor (IsSmoothDivisor, which also
admits the empty divisor: an empty Y).
The two printed steps and their forms in the library. (107.3) is eq_BO_of_maxOrd of
Hironaka.MarkedOrderReduction (E = ∅, max-ord I = m), applied at m = 1 to the marked family
of the stage n + 1, which is the assembly of Theorem 107 at BO_{n+1,·} (tower_succ_bmo);
BO_{n+1,1} is the functor of Theorem 103 at the data of Lemma 102 (boOfBMO_functor), evaluated
on the local class by functor_seq_localClass — Y is a hypersurface of maximal contact for
(I, 1) because I = τ_*J contains the equation of Y (isMaximalContact_one_of_eq_map,
bOClass_one_of_eq_map, maxOrd_le_one_of_eq_map_smoothDivisor). (103.3) is
maxContactCase_bdData_eq_pushforward: with E = ∅ Step 2.1 of [Kol07, 104] is empty and Step 2.2
is the push-forward of [Kol07, Lemma 102 (3)], along Y_r ↪ X_r = X, of the amalgam of the
stage-n marked family at the triple (Y_r, J, 1, (F_r − Y_r)|_{Y_r} + ⊤)
(closedEmbeddingTriple); the amalgam at the mark 1 is BMO_{n,1} (amalgam_seq). Below the
mark (max-ord I = 0, i.e. I = 𝒪_X, so J = 𝒪_Y) both sides are the empty sequence
(eq_nil_of_isOrderGeSeq_of_maxOrd_lt).
Three transports, none of them mathematics. (i) The identity is stated along an abstract closed
immersion j : Y ⟶ X, the maximal-contact case along Y.subschemeι; the bridge is Mathlib's
isomorphism j.toImage : Y ≅ V(ker j) of a closed immersion onto its image
(IsClosedImmersion.isIso_of_ker_eq), composed with the identification Y_r = V(ker j)
(subscheme_nth_zero_step22Triple). Along this isomorphism the value of BMO_{n,1} is transported
by the first bullet of [Kol07, 34.1] (the field commutesWithSmooth: an isomorphism is a smooth
surjection), and a push-forward along an isomorphism inverts the pull-back
(pushforward_pullback_of_isIso). (ii) The boundary (F_r − Y_r)|_{Y_r} + ⊤ of the triple of Lemma
102 (3) has every member equal to ⊤ when E = ∅ (the exceptional part F_r of the empty Step 2.1
sequence is empty), whereas Y's triple carries the empty family E|_Y: the two values agree by
the field indifferentToEmptyMembers along the unique order embedding from the empty index type.
(iii) Step 2.1's sequence is the empty sequence only propositionally (step21Seq_val_eq_nil); the
push-forward Lemma 102 (3) produces lives on its last scheme, and the concatenation with the empty
prefix is transported by substituting the equation inside the core lemma.
The general case (a chain of hypersurfaces, the identity being "a local question on X") is
Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingStep and
Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingGeneral; nothing here depends on it.
The core of the hypersurface case ([Kol07, 108]: "(103.3) gives that
BO_{dim X,1}(X, I, ∅) = τ_* BMO_{dim Y,1}(Y, J, 1, ∅)"): the push-forward of
[Kol07, Lemma 102 (3)] of the amalgam of the stage-n marked family at the triple
(Y_r, J, 1, (F_r − Y_r)|_{Y_r} + ⊤), prefixed by the (empty) Step 2.1 sequence, is the
push-forward along j of BMO_{n,1} at Y's marked triple. Stated over an arbitrary Step 2.1
sequence S₁ with e₀ : S₁ = nil (the shape of step22_closedEmbedding_aux) so that the
identification of Y_r with Y, the isomorphism Y ≅ Y_r (j.toImage), the first bullet of
[Kol07, 34.1] along it (the field commutesWithSmooth) and the deletion of the ⊤ boundary members
(the field indifferentToEmptyMembers) are all stated on the empty prefix.
The hypersurface case of Claim 71.2 [Kol07, 108]: for a closed embedding j : Y ↪ X of smooth
k-schemes whose kernel is a smooth divisor (Y a hypersurface of X, or empty),
τ_*(𝒪_Y/J) = 𝒪_X/I (MarkedTriple.ClosedEmbedding), E = ∅ and the mark 1, the stage-(n + 1)
functor of the tower at X is the push-forward along j of its value at Y. Kollár's argument:
every local equation of Y lies in I, so max-ord I = 1, the marked and unmarked functors agree
by (107.3), and (103.3) gives the push-forward. The stage n + 1 is the assembly of Theorem 107 at
BO_{n+1,·} (tower_succ_bmo); Y's value is taken at the stage n (its dimension is ≤ n) and
moved to the stage n + 1 by the coherence of the tower (tower_bmo_coherent). When I = 𝒪_X
(max-ord I = 0) both sides are the empty sequence.