Step 2.4 of order reduction: closed embeddings #
Step 2.4 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.4]) proves clause (3): for a
smooth hypersurface τ : Y ↪ X and an ideal sheaf J ⊂ 𝒪_Y, nonzero on every irreducible
component of Y, with τ_*(𝒪_Y/J) = 𝒪_X/I, the ideal I contains the local equations of Y and
so has order 1, whence I = W(I); for E = ∅, Step 2.1 does nothing and Step 2.2 may take
H = Y, so that clause (3) of Theorem 103 follows from clause (3) of [Kol07, Lemma 102].
This module proves that clause for the maximal-contact case,
BO^Y_{n,1}(X, I, ∅) = τ_* BMO_{n−1,1}(Y, J, 1, ∅), in the form
maxContactCase_bdData_eq_pushforward, following Kollár's three observations.
"I = W(I)." At the mark 1, BO^Y_{n,1}(X, I, ∅) is Step 2 on the tuned triple
(X, W_{s(1)}(I), ∅) at the mark s(1); since s(1) = 1 and W_1(I) = I (tuningParam_one,
W_tuningParam_one), it is Step 2 on (X, I, ∅) at the mark 1. The transport
step2Seq_congr_mark generalises the mark and the tuned ideal and substitutes
(maxContactCase_one_eq_step2Seq).
"Step 2.1 does nothing." For E = ∅ the Step 2.1 sequence is nil (card E.ι = 0,
step21Seq_val_eq_nil), and the whole Step 2.2 data is generalised over a sequence S₁ with
S₁ = nil and substituted (step22_closedEmbedding_aux), so that the Step 2.2 triple becomes
(X, I, ∅ + Y) with Y at position 0 (card F_r.ι = 0, nth_append_last), and I = τ_*J
transports to it through the identification e of the position-0 member with Y
(map_comap_eqToHom).
"(103.3) follows from (102.3)." Step 2.2 at the mark is the boundary-clearing functor at s(1)
on the re-tuned triple, again with s(1) = 1 and W_1 = id (functor_seq_congr_mark); for the
boundary-clearing data Hironaka.BD.bdData at the mark 1 that is Hironaka.BD.dataFunctor,
whose clause (3) is Hironaka.BD.eq_pushforward_of_quotient: τ_* B(Y, J, 1, (F − Y)|_Y + ⊤) on
the Step 2.2 triple. Below the mark (max-ord I = 0, so I = 𝒪_X) both sides are empty:
maxContactCase is nil by the remark after [Kol07, Theorem 68] and the Step 2.2 functor is nil
(step22Functor_seq_of_maxOrd_lt), while clause (3) of Lemma 102 still identifies the pushforward
with the empty value.
The globalised form of clause (3), for BO_{n,1} itself, is assembled in
Hironaka/Resolution/Algebraic/Stage/ClosedEmbeddingHypersurface.lean.
Transport of Step 2 along the identification of the mark and of the tuned ideal at m = 1:
s(1) = 1 and W_1(I) = I are propositional equalities, so the mark and the ideal are generalised
and substituted (structure eta identifies {T with I := T.I} with T).
At the mark 1, BO^H_{n,1}(X, I, E) is Step 2 on (X, I, E) itself ([Kol07, 104, Step 2.4]:
"in particular, I = W(I)"): the tuning W_{s(1)}(I) = W_1(I) = I is the identity
(tuningParam_one, W_tuningParam_one).
Transport of the boundary-clearing functor's value along the identification of the mark and of
the tuned ideal at m = 1 (the re-tuning inside Step 2.2).
I = τ_*J transported along an identification of the hypersurface: for A = B and J on
V(B), (J ∘ eqToHom) on V(A) pushes forward to the same ideal.
For an empty boundary the Step 2.1 sequence is empty ([Kol07, 104, Step 2.4]: "if E = ∅ then
Step 2.1 does nothing").
Generalised over the Step 2.1 sequence: for S₁ = nil, Step 2.2 with the boundary-clearing
data at the mark 1 on the Step 2.2 triple of Y is the pushforward
τ_* B(Y_r, J, 1, (F_r − Y_r)|_{Y_r} + ⊤) of clause (3) of [Kol07, Lemma 102]
([Kol07, 104, Step 2.4]: "in Step 2.2 we can choose H = Y; thus (103.3) follows from (102.3)"):
at the mark through the re-tuning identity (functor_seq_congr_mark) and
Hironaka.BD.eq_pushforward_of_quotient; below the mark both sides are empty.
Step 2 is empty below the mark for an empty boundary: Step 2.1 is nil and Step 2.2 is nil
by the remark after [Kol07, Theorem 68].
Clause (3) of [Kol07, Theorem 103] in the maximal-contact case ([Kol07, 104, Step 2.4];
clause (3) of [Kol07, Lemma 102]): for the boundary-clearing data bdData built from the inductive
input B, E = ∅ and I = τ_*J, BO^Y_{n,1}(X, I, ∅) = τ_* B(Y_r, J, 1, (F_r − Y_r)|_{Y_r} + ⊤),
the marked triple of clause (3) on the Step 2.2 triple of Y at the mark 1, Y_r at position
0, J transported, preceded by the empty Step 2.1 sequence.