Theorem 103 (3): preparatory lemmas

[Kol07, Theorem 103 (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, one has BO_{n,1}(X, I, ∅) = τ_* BMO_{n-1,1}(Y, J, 1, ∅). Its proof is [Kol07, 104, Step 2.4]: I contains the local equations of Y, so it has order 1 and equals its tuning; with E = ∅ Step 2.1 does nothing, and in Step 2.2 one may take H = Y, so that the clause follows from Lemma 102 (3). The assembly of this argument for the analytic functor is ClosedEmbedding.lean; this module proves the facts it needs:

• BD.Zminus1_one_eq_empty_of_isNonzeroEverywhere — the first centre Z_{-1} of the proof of [Kol07, Lemma 102] at the member Y and the mark 1 is empty when the restriction I|_Y is nonzero at every point. A connected component of Y contained in cosupp(I, 1) is open in Y (a manifold is locally connected); the generators of I|_Y vanish on it, so their germs at its points are zero and the stalk of I|_Y there is ⊥, against the hypothesis. This is the analytic reading of Kollár's "J is nonzero on every irreducible component of Y".
• HypersurfaceFamily.nonemptyList_empty — the empty boundary has no nonempty member, so Step 2.1 is idle.
• HypersurfaceFamily.eq_toLex_inr_of_append_empty — the boundary ∅ + Y has the single member Y.
• AnalyticTriple.tuned_one — at the mark 1 the tuning is the identity on triples.

The first centre at the mark 1 for a nonzero restriction

theorem Hironaka.Manifold.BD.Zminus1_one_eq_empty_of_isNonzeroEverywhere {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (I : M.IdealSheaf) (hJ : (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I).IsNonzeroEverywhere) : Zminus1 I 1 S = ∅

The hypothesis "J is nonzero on every irreducible component of Y" of [Kol07, Theorem 103 (3)], read for J = 𝓘|_Y as IsNonzeroEverywhere, makes the first centre Z_{-1} of the proof of [Kol07, Lemma 102] at the member Y and the mark 1 empty. A connected component of Y contained in cosupp(𝓘, 1) is open in Y, the generators of 𝓘|_Y vanish on it, so their germs at its points are 0 and the stalk of 𝓘|_Y there is ⊥, against the hypothesis. Not in the sources as a separate statement.

The empty boundary and the boundary ∅ + Y

theorem Manifold.HypersurfaceFamily.nonemptyList_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (hF : Finite { j : (empty M.carrier).ι // (empty M.carrier).hyp j ≠ ∅ }) : (empty M.carrier).nonemptyList hF = []

The empty boundary has no nonempty member, so Step 2.1 of the proof of [Kol07, Theorem 103] is idle on it ("if E = ∅ then Step 2.1 does nothing", [Kol07, 104, Step 2.4]).

theorem Manifold.HypersurfaceFamily.eq_toLex_inr_of_append_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (Y : Set M.carrier) (k : ((empty M.carrier).append Y).ι) : k = toLex (Sum.inr PUnit.unit)

The boundary ∅ + Y has exactly one member, the appended one.

The tuning at the mark 1

theorem Manifold.AnalyticTriple.tuned_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] (T : AnalyticTriple ψ₀ M) : T.tuned 1 ⋯ = T

At the mark 1 the tuning is the identity on triples (tuning_one_tuningParam; Kollár's "I has order 1, in particular I = W(I)" in [Kol07, 104, Step 2.4]).