The amalgam of a stage's marked functors

Kollár's induction [Kol07, 70] ("(69) in dimensions ≤ n − 1 ⇒ (68) in dimension n"; Lemma 102 and Theorem 103 "assume (69) holds in dimensions < n") feeds the marked order-reduction functors of the lower dimension into Lemma 102 and Theorem 103 — one functor BMO_{n−1,m'} for EVERY mark m', since the marks needed depend on the data. The library's Lemma 102 (Hironaka.BD.bdData) and Theorem 103 (Hironaka.BO.data) take that hypothesis as ONE marked functor B k : OrderGeSeqFunctor k (Dom k) over every field, defined on a class Dom k that contains every marked triple of dimension ≤ n − 1 and mark tuningParam m (hDom), together with clause (1) of Theorem 69 (hB), functoriality for smooth morphisms [Kol07, 34.1] (hsm), change of fields [Kol07, 34.2] (hbc) and the indifference to empty boundary members (hBind). The stage package OrderReductionStage n (Hironaka.Resolution.Algebraic.Stage.Tower) holds the family bmo : ∀ m, BMOData n m instead. This module is the bridge: the amalgam of the family — the marked functor on the class of marked triples of dimension ≤ n with mark ≥ 1 whose value at T is the value of bmo T.m — and the transports of the family's fields to the hypotheses of bdData and data. The two triples of a pull-back pair (MarkedTriple.IsPullbackOf), of a base-change pair (MarkedTriple.IsBaseChangeOf) and of an indifference pair carry the SAME mark, so each transport is the corresponding field of bmo T.m read through the mark congruence seq_congr_mark.

def Hironaka.MarkedTriple.AmalgamClass (n : ℕ) {k : Type u} [Field k] (T : MarkedTriple k) : Prop

The class of the amalgam: the marked triples of dimension ≤ n (every irreducible component of dimension ≤ n, Triple.HasDimLE) with mark ≥ 1 (Kollár's marks are ≥ 1), all marks at once — the class "in dimensions ≤ n" of the inductive hypothesis of [Kol07, Lemma 102 and Theorem 103], where the theorems assume (69) "in dimensions < n".

Equations

• Hironaka.MarkedTriple.AmalgamClass n T = (1 ≤ T.m ∧ T.HasDimLE n)

theorem Hironaka.Stage.amalgamClass_iff {n : ℕ} (k : Type u) [Field k] (T : MarkedTriple k) : MarkedTriple.AmalgamClass n T ↔ 1 ≤ T.m ∧ T.HasDimLE n

A marked triple lies in MarkedTriple.AmalgamClass n iff its mark is ≥ 1 and its dimension is ≤ n.

theorem Hironaka.Stage.bmoClass_of_amalgamClass {n : ℕ} (k : Type u) [Field k] {T : MarkedTriple k} (hT : MarkedTriple.AmalgamClass n T) : MarkedTriple.BMOClass n T.m T

A marked triple of the amalgam's class lies in the class of BMO_{n, T.m}.

noncomputable def Hironaka.Stage.amalgam {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] : OrderGeSeqAssignment k (MarkedTriple.AmalgamClass n)

The amalgam of the stage's marked functors (the inductive hypothesis of [Kol07, 70] in one functor): the marked functor on the marked triples of dimension ≤ n with mark ≥ 1 whose value at (X, I, m, E) is BMO_{n,m}(X, I, m, E), the value of the family member at the triple's own mark; the sequence is of order ≥ m for the marked triple and has no empty blow-ups by the fields of bmo T.m.

Equations

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

theorem Hironaka.Stage.amalgam_seq {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.AmalgamClass n T) : (amalgam bmo k).seq T hT = ((bmo T.m).functor k).seq T ⋯

The value of the amalgam is the value of the family member at the triple's mark.

theorem Hironaka.Stage.seq_congr_mark {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] {m₁ m₂ : ℕ} (h : m₁ = m₂) (T : MarkedTriple k) (h₁ : MarkedTriple.BMOClass n m₁ T) (h₂ : MarkedTriple.BMOClass n m₂ T) : ((bmo m₁).functor k).seq T h₁ = ((bmo m₂).functor k).seq T h₂

Two members of the family at equal marks take the same value (the class proofs are irrelevant).

theorem Hironaka.Stage.amalgamClass_of_tuningParam {n : ℕ} (k : Type u) [Field k] (m : ℕ) (T : MarkedTriple k) (hd : T.HasDimLE n) (hm : T.m = IsLocalRing.tuningParam m) : MarkedTriple.AmalgamClass n T

A marked triple of dimension ≤ n and mark tuningParam m lies in the amalgam's class (the tuning parameter is ≥ 1, one_le_tuningParam); this is the hypothesis hDom of bdData.

theorem Hironaka.Stage.amalgam_maxOrd_endTriple_lt {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.AmalgamClass n T) : ((amalgam bmo k).endTriple T hT).I.maxOrd < ↑T.m

[Kol07, Theorem 69 (1)] for the amalgam: its value ends below its mark — the field maxOrd_lt of bmo T.m (BMOData.maxOrd_endTriple_lt); the hypothesis hB of bdData.

theorem Hironaka.Stage.amalgam_commutesWithSmooth {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] : (amalgam bmo k).CommutesWithSmooth

The amalgam commutes with smooth morphisms, both bullets of [Kol07, 34.1], from the field of bmo T.m (a pull-back pair has equal marks); the hypothesis hsm of bdData.

theorem Hironaka.Stage.amalgam_commutesWithBaseChange {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (σ : k →+* L) : (amalgam bmo k).CommutesWithBaseChange (amalgam bmo L) σ

The amalgams over k and L commute with change of fields along σ [Kol07, 34.2], from the field of bmo T.m (a base-change pair has equal marks); the hypothesis hbc of bdData.

theorem Hironaka.Stage.amalgam_indifferentToEmptyMembers {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (k : Type u) [Field k] [CharZero k] : (amalgam bmo k).IndifferentToEmptyMembers

The amalgam is indifferent to empty boundary members (deleting ⊤ members of the boundary does not change its value, Kollár's reindexing of [Kol07, 34.1] and the convention of [Kol07, 32]), from the field of bmo T.m (deleting members keeps the mark); the hypothesis hBind of data.