The data of Lemma 102 are nil at a unit member

Kollár's convention deletes the empty blow-ups ([Kol07, 32]); the proof of [Kol07, Lemma 102] blows up Z_{-1} ⊂ E^j, the union of the components of E^j inside the cosupport, and then runs the inductive hypothesis on S := E^j. When the distinguished member E^j is the unit ideal, the empty divisor, Z_{-1} is the unit ideal (E^j ⊆ Z_{-1}, component_le_Zminus1 of Center.lean), its blow-up is the empty blow-up, deleted, and S is the empty scheme, on which every centre is the unit ideal, so the inductive functor's value is nil (eq_nil_of_noEmptyCenters) and its push-forward to X is nil. So bdData (AssemblyTuned.lean) is nil at a unit member at every mark: at mark 0 through the deleted π_{-1} of bdDataZero; at mark m + 1 through dataFunctor, the empty sequence below the mark and, at the mark, the deleted rawSeq of Output.lean on the tuned triple. A bookkeeping property of the construction, not in the sources.

• rawSeq_eraseEmpty_eq_nil_of_eq_top: the output of Output.lean with its empty blow-ups deleted is nil when the distinguished member is the unit ideal;
• bdData_nilAtUnitMember: BDFamily.NilAtUnitMember for bdData at every mark.

Used by Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentGlobal.lean.

theorem Hironaka.BD.rawSeq_eraseEmpty_eq_nil_of_eq_top {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m) (hmax : T.I.maxOrd = ↑m) {n : ℕ} (hn : T.HasDimLE n) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = m → Dom T') (hj : T.E.component j = ⊤) : (rawSeq T m j hI hmax hn B hDom).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

When the distinguished member E^j is the unit ideal, the output of Output.lean with its empty blow-ups deleted is the empty sequence ([Kol07, 32]): S = E^j is the empty scheme, the inductive functor's value on the restricted triple is nil (no empty centres on an empty scheme), and the first blow-up π_{-1} is empty, hence deleted.

theorem Hironaka.BD.bdData_nilAtUnitMember (n : ℕ) (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (m : ℕ) : BDFamily.NilAtUnitMember fun (j : ℕ) => bdData n m j Dom B ⋯ hB hsm hbc

bdData is nil at a unit member at every mark ([Kol07, 32]): at mark 0, Z_{-1} of the unit ideal is the unit ideal (component_le_Zminus1) and the empty blow-up π_{-1} is deleted; at mark m + 1, below the mark the value is nil by the convention of [Kol07, Theorem 68], and at the mark the output on the tuned triple reduces to nil (rawSeq_eraseEmpty_eq_nil_of_eq_top).