The restriction to S = E^j: the restricted marked triple and the output sequence

The proof of [Kol07, Lemma 102] continues on S := E^j, with injection τ : S ↪ X and E_S := (E − E^j)|_S: by the going-up theorem [Kol07, Theorem 84], the blow-up sequences of order ≥ m starting with the marked triple (S, I_0|_S, m, E_S) correspond to the blow-up sequences of order m starting with (X_0, I_0, E − E^j), and Kollár sets BD_{n,m,j}(X, I, E) := τ_* BMO_{n−1,m}(S, I_0|_S, m, E_S) ∘ π_{-1}: the output of order reduction for marked ideals in dimension n − 1, pushed forward along τ ([Kol07, 30.3]) and composed on the right with the first blow-up π_{-1}.

This module defines the restricted marked triple and the output sequence, and proves exactly what the definitions need: the four obligations of a marked triple (smooth, equidimensional, ideal nonzero on every component, family snc) with their supporting lemmas, and the dimension bound that rawSeq needs to apply the inductive functor. The remaining properties are proved in Composite.lean and Output.lean.

• Kollár's E − E^j is DivisorFamily.erase E j (Hironaka/Scheme/Snc/EraseFamily.lean).
• BD.centerS T m j: Z_{-1} viewed on S = E^j, the pull-back Z_{-1}.comap S.subschemeι; since Z_{-1} ⊆ S, it is Z_{-1} itself (its push-forward back to X is Z_{-1}), and as an ideal on S it is locally the zero ideal (on the components of S inside cosupp(I, m)) or the unit ideal.
• BD.restrictedTriple T m j hI hmax: the marked triple (S, I_0|_S, m, E_S). Where it lives. Kollár's S is E^j on X_0, i.e. the birational transform of E^j under the trivial blow-up π_{-1}, which drops the components inside Z_{-1}. Here this is the first stage of the blow-up sequence ON S whose first center is Z_{-1}|_S: X_S := blowUp S (Z_{-1}|_S) (= S minus those components), and the marked triple is the one induced after that step (the last paragraph of [Kol07, Definition 66]): I_S is the marked transform of I|_S with control m (= I_0|_S; the degenerate analogue of [Kol07, Lemma 62], see markedTransform_centerS_eq), E_S the total transform of (E − E^j)|_S (= (E_0 − E^j)|_S member by member, plus the exceptional member of Z_{-1}|_S, which is empty on X_S; the total-transform convention of this library, as for X_0). The closed immersion τ : X_S ⟶ X_0 = blowUp X Z_{-1} is blowUpMap S.subschemeι Z_{-1} (Hironaka/Scheme/BlowUp/BlowUpMap.lean), with kernel the birational transform of E^j. Why on the S-side. Kollár applies the going-up theorem to (X_0, I_0, E − E^j); Theorem 84 as printed needs the ideal D-balanced, and I_0 is not known to be. Kollár's own reading is the Warning in [Kol07, 104]: the consequences of Theorem 84 hold for any sequence of blow-ups of order m starting from the D-balanced I, here the COMPOSITE sequence on S starting with (S, I|_S, m, E_S), first center Z_{-1}|_S, then the BMO output. That is the going-up statement of Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean; the marked triple is the induced one after the first step because (S, I|_S, m, (E − E^j)|_S) itself is not a marked triple (I|_S vanishes on the components of S inside cosupp(I, m)). Its fields are proof obligations, discharged here: X_S is smooth over k of relative dimension n' − 1 when X has relative dimension n' (through τ: the birational transform of E^j is a smooth divisor of X_0, and τ is an isomorphism onto it), I_S is nonzero on every component (Transform.lean through markedTransform_centerS_eq and τ), E_S is snc (restriction of the snc family E − E^j + E^j to E^j, then the total transform of a family having snc with the center). The triple is restrictedTripleD (and the output below rawSeqD) at D = E^j, F = E − E^j: the same constructions for an arbitrary member D and family F satisfying RestrictedHyps, which Indifference.lean varies.
• BD.tailSeq T m j hI hmax hn B hDom: Kollár's τ_* BMO_{n−1,m}(S, I_0|_S, m, E_S), the push-forward along τ of B's sequence on the restricted marked triple (a sequence on X_0).
• BD.rawSeq T m j hI hmax hn B hDom: the output before the deletion of empty blow-ups ([Kol07, 32]): the composite sequence on S (first center Z_{-1}|_S, then B(S, I_0|_S, m, E_S) for the given marked functor B of the shape of [Kol07, Theorem 69] in dimensions ≤ n − 1) pushed forward to X along S ↪ X ([Kol07, 30.3]). Its first blow-up is the blow-up of X along (Z_{-1}|_S).map ι = Z_{-1}, i.e. π_{-1}, and its tail is τ_* B(…); the functor BD_{n,m,j} is this with the empty blow-ups deleted (OrderSeqAssignment.ofEraseEmpty, Hironaka/Scheme/BlowUpSequence/Functor.lean), defined in Output.lean once Composite.lean gives its order condition.
• BD.Domain n m j: Lemma 102's standing assumptions after its first paragraph ("from now on we assume that I is D-balanced"): dim X ≤ n, I D-balanced, max-ord I = m, and a j-th member of E (positions as in BDClass). The extension to BDClass by tuning (Tuned.lean) and by the convention of [Kol07, Theorem 68] for max-ord I < m (the sequence is empty) is Assembly.lean.

theorem Hironaka.BD.hasSncWith_component_self {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) : T.E.HasSncWith (T.E.component j)

E has simple normal crossings with its member E^j ([Kol07, Definition 24, (4)]).

theorem Hironaka.BD.smooth_component {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (T.E.component j).subschemeι (T.X.left ↘ AlgebraicGeometry.Spec ↧k))

E^j is smooth over k ("each E^i is smooth", [Kol07, Definition 24]).

theorem Hironaka.BD.isSmoothDivisor_component {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) : AlgebraicGeometry.IsSmoothDivisor (T.E.component j)

E^j is a smooth divisor ([Kol07, Definition 24, (1)–(2)]): regular, and locally (z_{c(j)} = 0) for a member of a regular system of parameters. The case F = T.E of Hironaka.Snc.isSmoothDivisor_component_of_isSnc (Hironaka/Resolution/Algebraic/Snc/SncInvertible.lean).

theorem Hironaka.BD.isSnc_restrictedFamily {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (j : T.E.ι) : ((T.E.erase j).comap (T.E.component j).subschemeι).IsSnc

The restriction of E − E^j to E^j is snc (Kollár's E_S := (E − E^j)|_S in the proof of [Kol07, Lemma 102]; the last sentence of [Kol07, Definition 24]): the snc coordinates of E at a point of E^j restrict to snc coordinates of the other members (the restriction lemma applied with Z := E^j itself), and each restricted member is regular, being a smooth center of the restricted family.

noncomputable def Hironaka.BD.centerS {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : (T.E.component j).subscheme.IdealSheafData

The center Z_{-1} viewed on Kollár's S = E^j (the proof of [Kol07, Lemma 102]): its pull-back along S ↪ X. Since Z_{-1} ⊆ E^j, pushing it forward returns Z_{-1} (map_centerS, Composite.lean).

Equations

• Hironaka.BD.centerS T m j = (Hironaka.BD.Zminus1 T.I m (T.E.component j)).comap (T.E.component j).subschemeι

theorem Hironaka.BD.stalkIdeal_centerS_eq_bot {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) {y : ↥(T.E.component j).subscheme} (hy : y ∈ (centerS T m j).support) : (centerS T m j).stalkIdeal y = ⊥

On S, the ideal Z_{-1}|_S is locally the zero ideal: at a point of Z_{-1} the stalk of Z_{-1} is the stalk of E^j (Center.lean), whose image in the stalk of S is zero.

theorem Hironaka.BD.hasSncWith_centerS {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : ((T.E.erase j).comap (T.E.component j).subschemeι).HasSncWith (centerS T m j)

Z_{-1}|_S has simple normal crossings with E_S = (E − E^j)|_S ([Kol07, Definition 65]; [Kol07, Definition 24, (4)]): its stalks are zero where it lives (the empty set of coordinates).

theorem Hironaka.BD.exceptionalDivisor_pow_dvd_comap {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) : (Zminus1 T.I m (T.E.component j)).exceptionalDivisor ^ m ∣ T.I.comap (Zminus1 T.I m (T.E.component j)).blowUpπ

F^m divides π_{-1}^* I (Kollár's formula (58.1), [Kol07, 58]; F^m · I_0 = π_{-1}^* I in Transform.lean).

theorem Hironaka.BD.markedTransform_centerS_eq {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) : (T.I.comap (T.E.component j).subschemeι).markedTransform (centerS T m j) m = (T.I.weakTransform (Zminus1 T.I m (T.E.component j))).comap (AlgebraicGeometry.Scheme.Hom.blowUpMap (T.E.component j).subschemeι (Zminus1 T.I m (T.E.component j)))

The marked transform of I|_S along Z_{-1}|_S is the restriction of I_0 = (π_{-1})^{-1}_* I along τ = blowUpMap S.subschemeι Z_{-1}, Kollár's I_0|_S: the degenerate analogue of [Kol07, Lemma 62] (marked transforms commute with restriction to a hypersurface H ⊋ Z containing the center), whose hypothesis Z ⊊ H excludes this case, as Kollár notes after its proof; here Z_{-1}|_S is locally S itself or empty, and the equality is proved directly ([Kol07, Remark 67] for the marked form).

theorem Hironaka.BD.ker_blowUpMap_component {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : AlgebraicGeometry.Scheme.Hom.ker (AlgebraicGeometry.Scheme.Hom.blowUpMap (T.E.component j).subschemeι (Zminus1 T.I m (T.E.component j))) = (T.E.component j).strictTransform (Zminus1 T.I m (T.E.component j))

τ = blowUpMap S.subschemeι Z_{-1} is a closed immersion into X_0 whose kernel is the birational transform (π_{-1})^{-1}_* E^j of E^j: its image is Kollár's S on X_0 (the proof of [Kol07, Lemma 102]).

theorem Hironaka.BD.smoothOfRelativeDimension_blowUpπ_centerS {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n (T.X.left ↘ AlgebraicGeometry.Spec ↧k)] : AlgebraicGeometry.SmoothOfRelativeDimension (n - 1) (CategoryTheory.CategoryStruct.comp (centerS T m j).blowUpπ (CategoryTheory.CategoryStruct.comp (T.E.component j).subschemeι (T.X.left ↘ AlgebraicGeometry.Spec ↧k)))

If X is smooth of relative dimension n over k, then X_S = blowUp S (Z_{-1}|_S) is smooth of relative dimension n − 1 (Kollár's S, of dimension n − 1, in the proof of [Kol07, Lemma 102]): through τ, an isomorphism onto the birational transform of E^j, a smooth divisor of X_0, which has relative dimension n − 1.

theorem Hironaka.BD.isSnc_totalTransform_centerS {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : (((T.E.erase j).comap (T.E.component j).subschemeι).totalTransform (centerS T m j)).IsSnc

The family of the restricted marked triple, the total transform of (E − E^j)|_S along Z_{-1}|_S, is snc (Kollár's E_S in the proof of [Kol07, Lemma 102]): AlgebraicGeometry.totalTransform_isSnc (Hironaka/Scheme/BlowUpSequence/Triple.lean), E_S being snc and having snc with the center.

theorem Hironaka.BD.isNonzeroEverywhere_markedTransform_centerS {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) : ((T.I.comap (T.E.component j).subschemeι).markedTransform (centerS T m j) m).IsNonzeroEverywhere

The marked transform of I|_S along Z_{-1}|_S is nonzero on every irreducible component of X_S: it is I_0|_S (markedTransform_centerS_eq), and τ is an isomorphism onto the birational transform of E^j, on whose components I_0 is nonzero (Transform.lean).

The restricted marked triple with the member and the family as parameters

noncomputable def Hironaka.BD.centerSD {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) : D.subscheme.IdealSheafData

The centre Z_{-1}|_D of the restricted triple, for an arbitrary member D (centerS T m j is this at D = E^j).

Equations

• Hironaka.BD.centerSD I m D = (Hironaka.BD.Zminus1 I m D).comap D.subschemeι

structure Hironaka.BD.RestrictedHyps {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) (F : X.DivisorFamily) : Prop

The facts about (D, F) that make the restricted marked triple a marked triple: they hold for D = E^j, F = E − E^j (restrictedHyps_component) and are transported along equalities of D (Indifference.lean).

• smooth : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (centerSD I m D).blowUpπ (CategoryTheory.CategoryStruct.comp D.subschemeι f))
• equidim : ∃ (n' : ℕ), AlgebraicGeometry.SmoothOfRelativeDimension n' (CategoryTheory.CategoryStruct.comp (centerSD I m D).blowUpπ (CategoryTheory.CategoryStruct.comp D.subschemeι f))
• isNonzeroEverywhere : ((I.comap D.subschemeι).markedTransform (centerSD I m D) m).IsNonzeroEverywhere
• isSnc : ((F.comap D.subschemeι).totalTransform (centerSD I m D)).IsSnc

noncomputable def Hironaka.BD.restrictedTripleD {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsSeparated f] (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) (F : X.DivisorFamily) (h : RestrictedHyps f I m D F) : MarkedTriple k

The restricted marked triple (D, I|_D, m, F_D) for a member D and a family F: the scheme blowUp D (Z_{-1}|_D), the marked transform of I|_D with control m, the mark m, and the total transform of F|_D.

Equations

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

noncomputable def Hironaka.BD.rawSeqD {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsSeparated f] (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) (F : X.DivisorFamily) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (h : RestrictedHyps f I m D F) (hdom : Dom (restrictedTripleD f I m D F h)) : X.BlowUpSequence

The raw output with the member and the family as parameters: π_{-1} on D followed by B on the restricted triple, pushed forward along D ↪ X.

Equations

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

theorem Hironaka.BD.restrictedHyps_component {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) : RestrictedHyps (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m (T.E.component j) (T.E.erase j)

The facts making the restricted marked triple a marked triple hold at D = E^j, F = E − E^j, for a D-balanced I with max-ord I = m: X_S is smooth over k of relative dimension one less than X; the ideal is nonzero on every component (Transform.lean); the family is snc.

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

The restricted marked triple (S, I_0|_S, m, E_S) of the proof of [Kol07, Lemma 102], S := E^j, E_S := (E − E^j)|_S, for a D-balanced I with max-ord I = m: the marked triple induced after the first step of the sequence on S with center Z_{-1}|_S (see the module docstring), i.e. the scheme X_S = blowUp S (Z_{-1}|_S), the marked transform of I|_S with control m (= I_0|_S, markedTransform_centerS_eq), the mark m, and the total transform of (E − E^j)|_S: restrictedTripleD at D = E^j, F = E − E^j.

Equations

• Hironaka.BD.restrictedTriple T m j hI hmax = Hironaka.BD.restrictedTripleD (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m (T.E.component j) (T.E.erase j) ⋯

theorem Hironaka.BD.hasDimLE_restrictedTriple {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) : (restrictedTriple T m j hI hmax).HasDimLE (n - 1)

The restricted marked triple has dimension ≤ n − 1 when (X, I, E) has dimension ≤ n.

noncomputable def Hironaka.BD.rawSeq {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') : T.X.left.BlowUpSequence

The output sequence on X before the deletion of empty blow-ups: the composite sequence on S = E^j whose first center is Z_{-1}|_S and whose tail is B(S, I_0|_S, m, E_S), for a marked functor B (the shape of [Kol07, Theorem 69], defined on the marked triples of dimension ≤ n − 1 and mark m; the inductive hypothesis BMO_{n−1,m}), pushed forward to X along S ↪ X ([Kol07, 30.3]). Its first blow-up is the blow-up of X along (Z_{-1}|_S).map ι = Z_{-1}, Kollár's π_{-1}, and its tail is τ_* B(…) (the proof of [Kol07, Lemma 102]). The functor BD_{n,m,j} deletes the empty blow-ups ([Kol07, 32]). This is rawSeqD at D = E^j, F = E − E^j.

Equations

• Hironaka.BD.rawSeq T m j hI hmax hn B hDom = Hironaka.BD.rawSeqD (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m (T.E.component j) (T.E.erase j) B ⋯ ⋯

noncomputable def Hironaka.BD.tailSeq {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') : ((centerS T m j).map (T.E.component j).subschemeι).blowUp.BlowUpSequence

The tail of the output, Kollár's τ_* BMO_{n−1,m}(S, I_0|_S, m, E_S) (the proof of [Kol07, Lemma 102]): the push-forward along τ (pushforwardBlowUp, the closed immersion X_S ⟶ X_0 over S ↪ X) of B's sequence on the restricted marked triple; a blow-up sequence on X_0, the blow-up of X along (Z_{-1}|_S).map ι = Z_{-1}. rawSeq is π_{-1} followed by it (pushforward_cons, Hironaka/Scheme/BlowUpSequence/Pushforward.lean).

Equations

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

def Hironaka.BD.Domain {k : Type u} [Field k] (n m j : ℕ) (T : AlgebraicGeometry.Triple k) : Prop

The standing assumptions of [Kol07, Lemma 102] after its first paragraph ("from now on we assume that I is D-balanced"): the domain of the construction of BD_{n,m,j}, the triples with dim X ≤ n, I D-balanced with max-ord I = m, and a j-th member of E (positions as in BDClass). The extension to BDClass n m j (tuning, Tuned.lean; the empty sequence for max-ord I < m, the convention of [Kol07, Theorem 68]) is Assembly.lean.

Equations

• Hironaka.BD.Domain n m j T = (T.HasDimLE n ∧ AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m ∧ T.I.maxOrd = ↑m ∧ j < Fintype.card T.E.ι)