Clause (3) of Lemma 102

The last paragraph of the proof of [Kol07, Lemma 102]: if O_X/I = τ_*(O_{E^j}/J) with J nonzero on every irreducible component of E^j, then every local equation of E^j is an element of order 1 of I, so max-ord I = 1 and W(I) = W_1(I) = I; no component of E^j is selected, so Z_{-1} = ∅ and I_0 = I; and I|_{E^j} = J. Hence BD_{n,1,j}(X, I, E) = τ_* BMO_{n−1,1}(E^j, J, 1, (E − E^j)|_{E^j}).

• Zminus1_eq_top_of_eq_map: at a generic point η = τ(x) of a component of E^j where I has order ≥ 1, the stalk ideal of the smooth divisor E^j is the maximal ideal (stalkIdeal_eq_maximalIdeal_of_mem_genericPoints) and E^j ⊆ I (I ⊇ ker τ), so I_η is that maximal ideal too; pulling back along τ (stalkIdeal_comap, I.comap τ = J and E^j.comap τ = 0) gives J_x = 0, against J nonzero everywhere. So no component of E^j is selected: Z_{-1} is the unit ideal.
• tuned_one: W_{s(1)}(I) = I (W_tuningParam_one), so the tuned triple is (X, I, E).
• eq_pushforward_of_quotient: above the mark (max-ord I = 1) the value of BD_{n,1,j} is the output of Output.lean for the tuned triple with its empty blow-ups deleted; its first center Z_{-1}|_S is the unit ideal, so the restricted marked triple is the pull-back of hypersurfaceTriple = (E^j, J, 1, ((E − E^j)|_{E^j}).append ⊤) along the isomorphism π_S : blowUp E^j ⊤ → E^j (markedTransform_of_eq_top, totalTransform_of_eq_top, comap_map_of_isClosedImmersion), B commutes with that smooth surjection (the first bullet of [Kol07, 34.1]), the deleted first blow-up transports the tail along π_X⁻¹ (eraseEmpty_cons_of_eq_top), and the push-forward/pull-back exchange along the square blowUp E^j ⊤ → blowUp X ⊤ over E^j → X (pullback_pushforward_of_isPullback; the square is a pull-back since its vertical maps are isomorphisms) cancels π_X⁻¹ against π_X. Below the mark I = O_X, hence J = O_{E^j}, and both sides are empty (eq_nil_of_isOrderGeSeq_of_maxOrd_lt, pushforward_nil).

Kollár's (E − E^j)|_{E^j} carries no empty member; the appended ⊤ is the exceptional member of the trivial blow-up in this library's total-transform convention (Assembly.lean). Used by Hironaka/Resolution/Algebraic/OrderReduction/ClosedEmbedding.lean.

theorem Hironaka.BD.tuned_one {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) : T.tuned 1 ⋯ = T

The tuned triple at the mark 1 is the triple itself (Kollár's W(I) = W_1(I) = I in the proof of [Kol07, Lemma 102]; s(1) = 1 and W_tuningParam_one).

theorem Hironaka.BD.hypersurfaceTriple_X {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : (hypersurfaceTriple T hj J hJ).X.left = (T.E.nth ⟨j, hj⟩).subscheme

The scheme of the marked triple of clause (3) is E^j.

theorem Hironaka.BD.hypersurfaceTriple_I {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : (hypersurfaceTriple T hj J hJ).I = J

Its ideal is J.

theorem Hironaka.BD.hypersurfaceTriple_m {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : (hypersurfaceTriple T hj J hJ).m = 1

Its mark is 1.

theorem Hironaka.BD.hypersurfaceTriple_E {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) : (hypersurfaceTriple T hj J hJ).E = ((T.E.erase (pos T hj)).comap (T.E.nth ⟨j, hj⟩).subschemeι).append ⊤

Its family is (E − E^j)|_{E^j} followed by an empty member.

theorem Hironaka.BD.Zminus1_eq_top_of_eq_map {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) (hIJ : T.I = J.map (T.E.nth ⟨j, hj⟩).subschemeι) : Zminus1 T.I 1 (T.E.nth ⟨j, hj⟩) = ⊤

No component of E^j is selected, Z_{-1} is the unit ideal (Kollár: J nonzero on every irreducible component of E^j gives Z_{-1} = ∅, the proof of [Kol07, Lemma 102]).

theorem Hironaka.BD.eq_pushforward_of_quotient {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hJ : J.IsNonzeroEverywhere) (hIJ : T.I = J.map (T.E.nth ⟨j, hj⟩).subschemeι) {n : ℕ} (hn : T.HasDimLE n) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam 1 → Dom T') (hB : B.CommutesWithSmoothSurjections) : (dataFunctor n 1 j ⋯ B hDom).seq T ⋯ = (B.seq (hypersurfaceTriple T hj J hJ) ⋯).pushforward (T.E.nth ⟨j, hj⟩).subschemeι

Clause (3) of [Kol07, Lemma 102]: if J ⊂ O_{E^j} is nonzero on every irreducible component of E^j and τ_*(O_{E^j}/J) = O_X/I, then BD_{n,1,j}(X, I, E) = τ_* B(E^j, J, 1, (E − E^j)|_{E^j}) (the family with the appended empty member); max-ord I ≤ 1 is derived (maxOrd_le_one_of_eq_map), and at max-ord I = 0 both sides are empty.