Assembly of BD_{n,m,j}: the tuning layer, the mark 0, and the data of clause (3)

[Kol07, Lemma 102] asserts, for every m, j, a smooth blow-up sequence functor BD_{n,m,j} of order m on triples with dim X ≤ n and max-ord I ≤ m, with clauses (1)–(3). Its proof first reduces to a D-balanced ideal (replace I by W_{s(m)}(I), Tuned.lean), then builds the sequence (Center.lean to Output.lean), proves its functoriality (FunctorialityPullback.lean, FunctorialityBaseChange.lean), and ends with clause (3). This module defines the pieces of the assembly and discharges the obligations they carry.

• BD.zeroFunctor n j, the functor at the mark m = 0. The class BDClass n 0 j is not empty (Kollár's m is a mark, ≥ 1; BDClass does not exclude 0): max-ord I ≤ 0 makes I the unit ideal, every component of E^j lies in cosupp(I, 0), so Z_{-1} = E^j, π_{-1} is the blow-up of E^j and the birational transform of E^j is empty. The functor is π_{-1} with its empty blow-up deleted ([Kol07, 32]); no inductive input is needed.
• BD.tunedFunctor hm F hDom', the tuning device of Step 1 of the proof of [Kol07, Theorem 103] for Lemma 102's class: from a functor F of order s(m) on a class containing the tuned triples of BDClass n m j, the functor of order m on BDClass n m j whose value is F(X, W_{s(m)}(I), E) when max-ord I = m and the empty sequence when max-ord I < m (the convention of [Kol07, Theorem 68]: "the case max-ord I < m is trivial, that is, X_r = X"). It is the instance at C := BDClass n m j of the class-generic OrderSeqAssignment.ofTunedClass (whose instance OrderSeqAssignment.ofTuned is the same device on the class of Theorem 103); the order condition is isOrderSeq_iff_tuned (Tuned.lean, [Kol07, Corollary 101] at this library's tuning parameter).
• BD.domain_tuned: the tuned triple of a triple of BDClass n m j above the mark lies in Lemma 102's standing class Domain n (s(m)) j (isDBalanced_tuned, maxOrd_tuned of Hironaka/Resolution/Algebraic/OrderReduction/Tuned.lean).
• BD.dataFunctor n m j hm B hDom, the functor BD_{n,m,j} over one field, for m ≥ 1: tunedFunctor applied to functor n (s(m)) j B hDom of Output.lean, for a marked functor B of the shape of [Kol07, Theorem 69] at mark s(m) in dimensions ≤ n − 1 (the induction hypothesis BMO_{≤ n−1, s(m)}). Lemma 102's data BDData n m j, the functor over every field with clauses (1)–(2), is assembled from it in AssemblyTuned.lean (bdData) and from zeroFunctor in AssemblyZero.lean (bdDataZero).
• BD.hypersurfaceTriple T hj J hJ, the marked triple (E^j, J, 1, (E − E^j)|_{E^j}) of clause (3), for J nonzero on every component of E^j. Its family is the members of E − E^j restricted to E^j, followed by an EMPTY member (the unit ideal): the exceptional member that the restricted marked triple of Restriction.lean carries at Z_{-1} = ∅, so that the latter is exactly its pull-back along the trivial blow-up; Kollár's (E − E^j)|_{E^j} has no such member (the total-transform convention of this library, as for E_0 of BD.piMinusOne). The obligations: E^j is smooth of relative dimension one less (isSmoothDivisor_component), the family is snc (isSnc_restrictedFamily and isSnc_append_top).
• BD.maxOrd_le_one_of_eq_map, BD.bdClass_one_of_eq_map: the hypothesis of clause (3), τ_*(O_{E^j}/J) = O_X/I, i.e. I = J.map τ, puts (X, I, E) in the class of BD_{n,1,j}: "every local equation of E^j is an order 1 element in I" (the proof of [Kol07, Lemma 102]), so max-ord I ≤ 1.

Used by AssemblyZero.lean, and outside this directory by Hironaka/Resolution/Algebraic/OrderReduction/Step24ClosedEmbedding.lean (Hironaka/Resolution/Algebraic/OrderReduction/Step21BoundaryClearing.lean imports it and uses only BDData).

noncomputable def Hironaka.BD.zeroFunctor {k : Type u} [Field k] [CharZero k] (n j : ℕ) : OrderSeqAssignment k 0 (AlgebraicGeometry.Triple.BDClass n 0 j)

BD_{n,0,j}, the functor of [Kol07, Lemma 102] at the mark 0: on BDClass n 0 j (where max-ord I ≤ 0 forces I to be the unit ideal), the trivial blow-up π_{-1} of Z_{-1} = E^j with its empty blow-up deleted ([Kol07, 32]); a smooth blow-up sequence of order 0 starting with (X, I, E) by isOrderSeq_piMinusOne (Center.lean).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hironaka.BD.tunedFunctor {k : Type u} [Field k] [CharZero k] {n m j : ℕ} (hm : 1 ≤ m) {Dom' : AlgebraicGeometry.Triple k → Prop} (F : OrderSeqAssignment k (IsLocalRing.tuningParam m) Dom') (hDom' : ∀ (T : AlgebraicGeometry.Triple k), AlgebraicGeometry.Triple.BDClass n m j T → T.I.maxOrd = ↑m → Dom' (T.tuned m hm)) : OrderSeqAssignment k m (AlgebraicGeometry.Triple.BDClass n m j)

The reduction to the tuned ideal on BDClass n m j (the first paragraph of the proof of [Kol07, Lemma 102]; the convention of [Kol07, Theorem 68] below the mark): from a smooth blow-up sequence functor F of order s(m) on a class containing the tuned triples of BDClass n m j, the functor of order m on BDClass n m j whose value on (X, I, E) is F(X, W_{s(m)}(I), E) when max-ord I = m and the empty sequence when max-ord I < m. The instance of OrderSeqAssignment.ofTunedClass at C := BDClass n m j (the mark bound is the global hm).

Equations

• Hironaka.BD.tunedFunctor hm F hDom' = F.ofTunedClass ⋯ hDom'

theorem Hironaka.BD.domain_tuned {k : Type u} [Field k] [CharZero k] {n m j : ℕ} (hm : 1 ≤ m) {T : AlgebraicGeometry.Triple k} (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd = ↑m) : Domain n (IsLocalRing.tuningParam m) j (T.tuned m hm)

The tuned triple of a triple of BDClass n m j with max-ord I = m lies in the standing class Domain n (s(m)) j of Restriction.lean (the first paragraph of the proof of [Kol07, Lemma 102]): W_{s(m)}(I) is D-balanced of maximal order s(m) (isDBalanced_tuned, maxOrd_tuned), the dimension and the members of E are unchanged.

noncomputable def Hironaka.BD.dataFunctor {k : Type u} [Field k] [CharZero k] (n m j : ℕ) (hm : 1 ≤ m) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom T') : OrderSeqAssignment k m (AlgebraicGeometry.Triple.BDClass n m j)

The functor BD_{n,m,j} over one field ([Kol07, Lemma 102] with the first paragraph of its proof), for a mark m ≥ 1 and a marked functor B of the shape of [Kol07, Theorem 69] at mark s(m) in dimensions ≤ n − 1 (the inductive hypothesis): the functor of Output.lean at order s(m) on the tuned triple, and the empty sequence below the mark. Lemma 102's data BDData n m j over every field is assembled from it in AssemblyTuned.lean (bdData).

Equations

• Hironaka.BD.dataFunctor n m j hm B hDom = Hironaka.BD.tunedFunctor hm (Hironaka.BD.functor n (IsLocalRing.tuningParam m) j B hDom) ⋯

noncomputable def Hironaka.BD.totalFunctor {k : Type u} [Field k] [CharZero k] (n m j : ℕ) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : (∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom T') → OrderSeqAssignment k m (AlgebraicGeometry.Triple.BDClass n m j)

The functor BD_{n,m,j} over one field for every mark ([Kol07, Lemma 102], "for every m, j"), by a case split on the mark: zeroFunctor at m = 0 and dataFunctor at m ≥ 1. The inductive input B, a marked functor at mark s(m) in dimensions ≤ n − 1, is an argument at every mark so that the functor has one signature, Kollár's BD_{n,m,j} for every m; the definition does not need it at m = 0, because there I is the unit ideal and the value is the trivial blow-up π_{-1} alone, without any inductive input (zeroFunctor).

Equations

• Hironaka.BD.totalFunctor n 0 x x_2 x_3 = Hironaka.BD.zeroFunctor n x
• Hironaka.BD.totalFunctor n m.succ x x_2 x_3 = Hironaka.BD.dataFunctor n (m + 1) x ⋯ x_2 x_3

noncomputable def Hironaka.BD.hypersurfaceTriple {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) : MarkedTriple k

The marked triple (E^j, J, 1, (E − E^j)|_{E^j}) of clause (3) of [Kol07, Lemma 102], for an ideal J ⊂ O_{E^j} nonzero on every irreducible component of E^j; its family is the members of E − E^j restricted to E^j, followed by an empty member (see the module docstring). E^j is smooth over k of relative dimension one less than X (isSmoothDivisor_component, Restriction.lean), J is nonzero on every component by hypothesis, and the family is snc (isSnc_restrictedFamily, isSnc_append_top).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.BD.hasDimLE_hypersurfaceTriple {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) {n : ℕ} (hn : T.HasDimLE n) : (hypersurfaceTriple T hj J hJ).HasDimLE (n - 1)

The marked triple of clause (3) has dimension ≤ n − 1 when (X, I, E) has dimension ≤ n (Kollár's BMO_{n−1,1}, [Kol07, Lemma 102]).

theorem Hironaka.BD.maxOrd_le_one_of_eq_map {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hIJ : T.I = J.map (T.E.nth ⟨j, hj⟩).subschemeι) : T.I.maxOrd ≤ ↑1

If O_X/I = τ_*(O_{E^j}/J), i.e. I = J.map τ, then max-ord I ≤ 1 ("Every local equation of E^j is an order 1 element in I", the proof of [Kol07, Lemma 102]): I contains the ideal of E^j (ker τ = ⊥.map τ ≤ J.map τ), which has order 1 along E^j (a smooth divisor), and I is the unit ideal off E^j (its support lies in the closed image of τ).

theorem Hironaka.BD.bdClass_one_of_eq_map {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) {j : ℕ} (hj : j < Fintype.card T.E.ι) (J : (T.E.nth ⟨j, hj⟩).subscheme.IdealSheafData) (hIJ : T.I = J.map (T.E.nth ⟨j, hj⟩).subschemeι) {n : ℕ} (hn : T.HasDimLE n) : AlgebraicGeometry.Triple.BDClass n 1 j T

Under the hypothesis of clause (3) of [Kol07, Lemma 102], (X, I, E) lies in the class of BD_{n,1,j} when dim X ≤ n.