Lemma 102 (1)–(2) for m ≥ 1, and the assembly over every field

BD.tunedFunctor hm F hDom' (Assembly.lean) is the tuning device of Step 1 of the proof of [Kol07, Theorem 103] on the class of Lemma 102: F(X, W_{s(m)}(I), E) above the mark, the empty sequence below it. This module shows that the clauses of [Kol07, Lemma 102] pass through it, as the ofTunedClass_* transfers of Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean do for the class-generic OrderSeqAssignment.ofTunedClass, here at C := BDClass n m j with the global hm : 1 ≤ m and max-ord I ≤ m read off BDClass (hT.2.1):

• the two values (tunedFunctor_seq_of_maxOrd_eq, tunedFunctor_seq_of_maxOrd_lt);
• clause (2) (tunedFunctor_commutesWithSmooth, tunedFunctor_commutesWithBaseChange): the case splits of two triples align because max-ord does not rise under a smooth pull-back (maxOrd_comap_le_of_smooth), is preserved by a surjection (maxOrd_le_maxOrd_comap_of_surjective) and by a change of fields (maxOrd_comap_of_isPullback_specMap); in the one mixed case, T above the mark, its smooth pull-back T' below, the pulled-back sequence with its empty blow-ups deleted is an order-m sequence without empty centers for T' (isOrderSeq_eraseEmpty_pullback_of_equidim), hence empty (eq_nil_of_isOrderSeq_of_maxOrd_lt).

For BD.dataFunctor n m j hm B hDom, the tuned functor applied to the functor of Output.lean at order s(m):

• clause (1) (disjoint_cosupp_dataFunctor): above the mark the value is the output of Output.lean for (W_{s(m)}(I), s(m)), whose final cosupport is disjoint from the birational transform of E^j (disjoint_cosupp_eraseEmpty_rawSeq); the same sequence is of order m for (I, E) (isOrderSeq_tuned_iff), and cosupp(I_r, m) = cosupp(W_r, s(m)) at the last stage (le_ord_weakTransformSeq_iff_tuned, Tuned.lean), so the disjointness transfers; below the mark the value is empty and cosupp(I, m) = ∅.
• clause (2) from functor_commutesWithSmooth/functor_commutesWithBaseChange of the two functoriality modules, through the tuning layer.
• totalFunctor_zero/totalFunctor_succ: the case split on the mark.
• bdData, exists_bdData: the assembled BDData n m j from the induction hypothesis BMO_{≤ n−1, s(m)} over every field (given as a Π-bundle over the fields, in the order of BDData's fields), with bdDataZero at the mark 0.

Used by ClauseThree.lean, Indifference.lean and NilAtUnit.lean, and outside this directory by Hironaka/Resolution/Algebraic/Stage/Congr.lean, HironakaExamples/Dimension1.lean and the embedded-resolution modules Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP1Step21.lean, Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP3Step21.lean, Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP3Tower.lean.

theorem Hironaka.BD.tunedFunctor_seq_of_maxOrd_eq {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)) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd = ↑m) : (tunedFunctor hm F hDom').seq T hT = F.seq (T.tuned m hm) ⋯

Above the mark the tuned functor returns F on the tuned triple (Step 1 of the proof of [Kol07, Theorem 103], on the class of Lemma 102).

theorem Hironaka.BD.tunedFunctor_seq_of_maxOrd_lt {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)) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd < ↑m) : (tunedFunctor hm F hDom').seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

Below the mark the tuned functor returns the empty sequence (the convention of [Kol07, Theorem 68]).

theorem Hironaka.BD.tunedFunctor_commutesWithSmooth {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)) (hF : F.CommutesWithSmooth) : (tunedFunctor hm F hDom').CommutesWithSmooth

The tuned functor commutes with smooth morphisms when F does ([Kol07, 34.1]): the argument of Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean on BDClass n m j.

theorem Hironaka.BD.tunedFunctor_commutesWithBaseChange {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)) {L : Type u} [Field L] [CharZero L] {Dom'' : AlgebraicGeometry.Triple L → Prop} (F' : OrderSeqAssignment L (IsLocalRing.tuningParam m) Dom'') (hDom'' : ∀ (T : AlgebraicGeometry.Triple L), AlgebraicGeometry.Triple.BDClass n m j T → T.I.maxOrd = ↑m → Dom'' (T.tuned m hm)) (σ : k →+* L) (hF : F.CommutesWithBaseChange F' σ) : (tunedFunctor hm F hDom').CommutesWithBaseChange (tunedFunctor hm F' hDom'') σ

The tuned functors commute with a change of fields when F and F' do ([Kol07, 34.2]): the argument of Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean on BDClass n m j.

theorem Hironaka.BD.dataFunctor_seq_of_maxOrd_eq {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') (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd = ↑m) : (dataFunctor n m j hm B hDom).seq T hT = (functor n (IsLocalRing.tuningParam m) j B hDom).seq (T.tuned m hm) ⋯

Above the mark BD_{n,m,j} is the functor of Output.lean at order s(m) on the tuned triple (the proof of [Kol07, Lemma 102]).

theorem Hironaka.BD.dataFunctor_seq_of_maxOrd_lt {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') (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (h : T.I.maxOrd < ↑m) : (dataFunctor n m j hm B hDom).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

Below the mark BD_{n,m,j} is the empty sequence (the convention of [Kol07, Theorem 68]).

theorem Hironaka.BD.disjoint_cosupp_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') (hB : ∀ (T' : MarkedTriple k) (hT' : Dom T'), (B.endTriple T' hT').I.maxOrd < ↑T'.m) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T) : Disjoint {x : ↥(((dataFunctor n m j hm B hDom).seq T hT).stage (Fin.last ((dataFunctor n m j hm B hDom).seq T hT).length)) | ↑m ≤ (((dataFunctor n m j hm B hDom).seq T hT).weakTransformSeq T.I (Fin.last ((dataFunctor n m j hm B hDom).seq T hT).length)).ord x} ↑(((dataFunctor n m j hm B hDom).seq T hT).strictTransformSeq (T.E.nth ⟨j, ⋯⟩) (Fin.last ((dataFunctor n m j hm B hDom).seq T hT).length)).support

Clause (1) of [Kol07, Lemma 102] for BD_{n,m,j} from clause (1) of [Kol07, Theorem 69] for B: clause (1) of Output.lean for (W_{s(m)}(I), s(m)) transported to (I, m) at the last stage by le_ord_weakTransformSeq_iff_tuned; below the mark the cosupport is empty.

theorem Hironaka.BD.dataFunctor_commutesWithSmooth {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') (hB : B.CommutesWithSmooth) : (dataFunctor n m j hm B hDom).CommutesWithSmooth

BD_{n,m,j} commutes with smooth morphisms when B does ([Kol07, 34.1]): functor_commutesWithSmooth through the tuning layer.

theorem Hironaka.BD.dataFunctor_commutesWithBaseChange {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') {L : Type u} [Field L] [CharZero L] {Dom' : MarkedTriple L → Prop} (B' : OrderGeSeqAssignment L Dom') (hDom' : ∀ (T' : MarkedTriple L), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom' T') (σ : k →+* L) (hB : B.CommutesWithBaseChange B' σ) : (dataFunctor n m j hm B hDom).CommutesWithBaseChange (dataFunctor n m j hm B' hDom') σ

BD_{n,m,j} over k and over L commute with a change of fields when B and B' do ([Kol07, 34.2]): functor_commutesWithBaseChange through the tuning layer.

theorem Hironaka.BD.totalFunctor_zero {k : Type u} [Field k] [CharZero k] (n j : ℕ) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam 0 → Dom T') : totalFunctor n 0 j B hDom = zeroFunctor n j

The case split at the mark 0.

theorem Hironaka.BD.totalFunctor_succ {k : Type u} [Field k] [CharZero k] (n j : ℕ) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (m : ℕ) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam (m + 1) → Dom T') : totalFunctor n (m + 1) j B hDom = dataFunctor n (m + 1) j ⋯ B hDom

The case split at a mark m + 1.

noncomputable def Hironaka.BD.bdData (n m j : ℕ) (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)) : (∀ (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') → (∀ (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) → (∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) → (∀ (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) σ) → BDData n m j

BD_{n,m,j} over every field of characteristic zero (clauses (1)–(2) of [Kol07, Lemma 102]), from the induction hypothesis BMO_{≤ n−1, s(m)} given as a Π-bundle over the fields (the functors, clause (1) of [Kol07, Theorem 69], commutation with smooth morphisms, commutation with change of fields, in the order of BDData's fields), by a case split on the mark: bdDataZero at 0, the tuned assembly at m + 1.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.BD.bdData n 0 x x_1 x_2 x_6 x_3 x_4 x_5 = Hironaka.BD.bdDataZero n x

theorem Hironaka.BD.exists_bdData (n m j : ℕ) (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 : ∀ (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) σ) : ∃ (D : BDData n m j), ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BDClass n m j T), (D.functor k).seq T hT = (totalFunctor n m j (B k) ⋯).seq T hT

Clauses (1)–(2) of [Kol07, Lemma 102]: a BDData n m j whose functor over k is totalFunctor n m j (B k) (hDom k) (existential form of bdData).