The vocabulary of blow-up sequence functors on triples

The notions through which Kollár's functorial principalization and resolution theorems [Kol07, Theorems 35 and 36] are proved, on top of the vocabulary of the statements (divisor families, transforms along a succession, the functors of the main theorems). No main theorem is stated with them.

• MarkedTriple k: the marked triples (X, I, m, E) of [Kol07, Notation 64], a triple AlgebraicGeometry.Triple k with a mark m; Triple.IsOrderBlowUp, MarkedTriple.IsOrderGeBlowUp: the smooth blow-ups of order m, respectively ≥ m, of [Kol07, Definition 65].
• On a succession S : BlowUpSequence X: IsOrderSeq, IsOrderGeSeq, the smooth blow-up sequences of order m, respectively ≥ m, starting with a triple [Kol07, Definition 66], whose induced ideals are the weak transforms, respectively the marked transforms.
• OrderSeqFunctor k m Dom, OrderGeSeqFunctor k Dom: smooth blow-up sequence functors of order m on a class of triples, respectively of order ≥ m on a class of marked triples [Kol07, Definitions 31 and 66, Theorems 68 and 69], with the no-empty-blow-up output convention of [Kol07, 32] as a field, and their endResult (the associated resolution functor R). The functoriality properties of [Kol07, 34] as predicates on them: IsPullbackOf and CommutesWith, CommutesWithSmoothSurjections, CommutesWithSmooth (34.1); IsBaseChangeOf and CommutesWithBaseChange (34.2); ClosedEmbedding and CommutesWithClosedEmbeddings, CommutesWithClosedEmbeddingsOfEmptyDivisor (34.3, and Theorem 35's "whenever E = ∅"); WeaklyCommutesWithClosedEmbeddings and its E = ∅ form (34.4).
• The setting of [Kol07, Proposition 37] (gluing a functor defined on affine schemes): IsSigmaOf and ClosedUnderSigma (a triple is the disjoint union of a family; a class closed under finite disjoint unions, [Kol07, Warning 38]), IsAffineScheme, and for a triple the two auxiliary schemes of the proof, coverScheme (X' = ∐ᵢ Uᵢ over the finite affine cover affineCover) with coverDesc (g : X' → X) and coverPair (X'' = X' ×_X X') with coverFst, coverSnd; and BlowUpSequence.AgreeOnOverlaps, the descent datum of the proof.
• The setting of [Kol07, Theorem 105] (globalization of blow-up sequence functors): IsGlobalizationClass M (a class of smooth morphisms closed under fibre products and coproducts), openImmersionCoprods (the coproducts of open immersions), Triple.GlobalizationData M GT LT (global and local triples), CommutesWithSurjectionsIn, and from its proof Triple.IsLocalCover and Triple.LocalCoversFibreClosed, the closure of the local class under the fibre products the proof forms.

The triples are those of the statement of Theorem 35, AlgebraicGeometry.Triple k (Hironaka.Scheme.Resolution.Defs): an algebraic k-scheme T.X smooth of a single relative dimension over k, an ideal sheaf T.I and a divisor family T.E on its underlying scheme T.X.left. The notions on triples defined here live in the namespace AlgebraicGeometry.Triple, so that dot notation reaches them; the instances on T.X.left (separated, of finite type and smooth over k) are those of Hironaka.Scheme.Resolution.Basic.

Triples and marked triples (Kollár Notation 64)

structure Hironaka.MarkedTriple (k : Type u) [Field k] extends AlgebraicGeometry.Triple k : Type (u + 1)

Kollár's marked triple (X, I, m, E) [Kol07, Notation 64 and its footnote] ("I consider the pair (I, m) as one item, so (X, I, m, E) is still a triple"): a triple whose ideal carries the mark m ∈ ℕ.

• X : AlgScheme k
• smoothOfRelativeDimension : ∃ (n : ℕ), SmoothOfRelativeDimension n (self.X.left ↘ Spec ↧k)
• I : self.X.left.IdealSheafData
• isNonzeroEverywhere : self.I.IsNonzeroEverywhere
• E : self.X.left.DivisorFamily
• isSnc : self.E.IsSnc
• m : ℕ

  The mark m of the marked ideal (I, m).

def AlgebraicGeometry.Triple.IsOrderBlowUp {k : Type u} [Field k] (T : Triple k) (Z : T.X.left.IdealSheafData) (m : ℕ) : Prop

A smooth blow-up of order m of the triple (X, I, E) [Kol07, Definition 65 (1)–(2)], given with max-ord I = m: a centre Z ⊂ X smooth over k [Kol07, Notation 19], having simple normal crossings with E Kol07, Definition 24 (4), HasSncWith, with ord_Z I = m (the order of I at every generic point of Z). The hypothesis max-ord I = m of the definition's preamble is carried by the statements that use it.

Equations

• T.IsOrderBlowUp Z m = (AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι (T.X.left ↘ AlgebraicGeometry.Spec ↧k)) ∧ T.E.HasSncWith Z ∧ T.I.OrdAlongEq Z.support ↑m)

def Hironaka.MarkedTriple.IsOrderGeBlowUp {k : Type u} [Field k] (T : MarkedTriple k) (Z : T.X.left.IdealSheafData) : Prop

A smooth blow-up of the marked triple (X, I, m, E) [Kol07, Definition 65 (1′)–(2′)]: a centre Z ⊂ X smooth over k, having simple normal crossings with E, with ord_Z I ≥ m at every generic point of Z.

Equations

• T.IsOrderGeBlowUp Z = (AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι (T.X.left ↘ AlgebraicGeometry.Spec ↧k)) ∧ T.E.HasSncWith Z ∧ T.I.LeOrdAlong Z.support ↑T.m)

def AlgebraicGeometry.Scheme.BlowUpSequence.IsOrderSeq {k : Type u} [Field k] {X : Scheme} (S : X.BlowUpSequence) (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) : Prop

S is a smooth blow-up sequence of order m starting with (X, I, E) [Kol07, Definition 66], given with max-ord I = m: (2) each π_i is a smooth blow-up (IsSmooth: the centres are smooth over k), and for every i, with the induced data I_i = weakTransformSeq, E_i = totalTransformSeq of clause (1) of the definition: (3) Z_i has simple normal crossings with E_i, and (4) ord_{Z_i} I_i = m. Codimension-one and empty centres are allowed [Kol07, Definition 66 and Warning 20].

Equations

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

def AlgebraicGeometry.Scheme.BlowUpSequence.IsOrderGeSeq {k : Type u} [Field k] {X : Scheme} (S : X.BlowUpSequence) (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) : Prop

S is a smooth blow-up sequence of order ≥ m starting with (X, I, m, E) [Kol07, Definition 66]: (2′) each π_i is a smooth blow-up, and for every i, with the induced marked data (I_i, m) = markedTransformSeq, E_i = totalTransformSeq of clause (1′): (3′) Z_i has simple normal crossings with E_i, and (4′) ord_{Z_i} I_i ≥ m.

Equations

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

Blow-up sequence functors on triples and marked triples

structure Hironaka.OrderSeqAssignment (k : Type u) [Field k] (m : ℕ) (Dom : AlgebraicGeometry.Triple k → Prop) : Type (u + 1)

A smooth blow-up sequence functor of order m on the class Dom of triples: Kollár's blow-up sequence functor [Kol07, Definition 31] enriched as in the last paragraph of [Kol07, Definition 66] (functors B with B(X, I, E) "a blow-up sequence starting with (X, I, E)") and shaped as in [Kol07, Theorem 68] ("a smooth blow-up sequence functor BO_m of order m" defined on triples with max-ord I ≤ m) — an assignment of a smooth blow-up sequence of order m starting with (X, I, E) (IsOrderSeq, Definition 66) to every triple of the class, "with specified centers" (the sequence carries them; "the length of the sequence r, the schemes X_i and the centers Z_i all depend on (X, I, E)"), whose outputs contain no empty blow-ups [Kol07, 32]. The functoriality clauses of [Kol07, 34] are separate predicates below.

• seq (T : AlgebraicGeometry.Triple k) : Dom T → T.X.left.BlowUpSequence

  The blow-up sequence B(X, I, E) assigned to a triple of the class.

• isOrderSeq (T : AlgebraicGeometry.Triple k) (h : Dom T) : (self.seq T h).IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m

  B(X, I, E) is a smooth blow-up sequence of order m starting with (X, I, E).

• noEmptyCenters (T : AlgebraicGeometry.Triple k) (h : Dom T) : (self.seq T h).NoEmptyCenters

  The output contains no empty blow-ups [Kol07, 32].

structure Hironaka.OrderGeSeqAssignment (k : Type u) [Field k] (Dom : MarkedTriple k → Prop) : Type (u + 1)

A smooth blow-up sequence functor of order ≥ m on the class Dom of marked triples: the last paragraph of [Kol07, Definition 66] ("B(X, I, m, E) … a blow-up sequence starting with (X, I, m, E)") in the shape of [Kol07, Theorem 69] ("a smooth blow-up sequence functor BMO_m of order ≥ m" defined on marked triples (X, I, m, E)) — an assignment of a smooth blow-up sequence of order ≥ m starting with (X, I, m, E) (IsOrderGeSeq, with the triple's own mark m) to every marked triple of the class, whose outputs contain no empty blow-ups [Kol07, 32].

• seq (T : MarkedTriple k) : Dom T → T.X.left.BlowUpSequence

  The blow-up sequence B(X, I, m, E) assigned to a marked triple of the class.

• isOrderGeSeq (T : MarkedTriple k) (h : Dom T) : (self.seq T h).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E

  B(X, I, m, E) is a smooth blow-up sequence of order ≥ m starting with (X, I, m, E).

• noEmptyCenters (T : MarkedTriple k) (h : Dom T) : (self.seq T h).NoEmptyCenters

  The output contains no empty blow-ups [Kol07, 32].

noncomputable def Hironaka.OrderSeqAssignment.endResult {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : (Y : AlgebraicGeometry.Scheme) × (Y ⟶ T.X.left)

[Kol07, Definition 31]: the (partial) resolution functor R associated to a blow-up sequence functor B sends (X, I, E) to "the end result of the blow-up sequence", R : (X, I, E) ↦ (Π : X_r → X).

Equations

• B.endResult T h = ⟨(B.seq T h).last, (B.seq T h).composite⟩

noncomputable def Hironaka.OrderGeSeqAssignment.endResult {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : (Y : AlgebraicGeometry.Scheme) × (Y ⟶ T.X.left)

[Kol07, Definition 31] for the marked version: the resolution functor associated to B, (X, I, m, E) ↦ (Π : X_r → X).

Equations

• B.endResult T h = ⟨(B.seq T h).last, (B.seq T h).composite⟩

Disjoint unions of triples (Kollár Warning 38)

def AlgebraicGeometry.Triple.IsSigmaOf {k : Type u} [Field k] (T : Triple k) {σ : Type u} (Ts : σ → Triple k) (ι : (i : σ) → (Ts i).X.left ⟶ T.X.left) : Prop

[Kol07, Warning 38] ("we need to know B for the disconnected affine scheme ∐ᵢ Uᵢ") with [Kol07, Notation 64 (1)] (X "possibly reducible"): the triple T is the disjoint union of the family Ts along the morphisms ι i : (Ts i).X.left ⟶ T.X.left — the cofan (ι i)ᵢ is a coproduct of schemes, each ι i is over Spec k, and the data of T restrict along ι i to the data of Ts i: the ideal by comap, the ordered divisor family componentwise (so every Ts i carries the index set of T, as the restrictions (Uᵢ, g^* I, g^{-1} E) in the proof of [Kol07, Proposition 37] do).

Equations

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

def AlgebraicGeometry.Triple.ClosedUnderSigma {k : Type u} [Field k] (Dom : Triple k → Prop) : Prop

[Kol07, Warning 38]: the class Dom of triples is closed under finite disjoint unions — a triple that is the disjoint union of a finite nonempty family of members of the class is a member. (The domain of a blow-up sequence functor must contain the disconnected schemes ∐ᵢ Uᵢ: a resolution functor on connected schemes extends to disconnected ones automatically, "but for blow-up sequence functors this is not at all the case".)

Equations

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

def Hironaka.MarkedTriple.IsSigmaOf {k : Type u} [Field k] (T : MarkedTriple k) {σ : Type u} (Ts : σ → MarkedTriple k) (ι : (i : σ) → (Ts i).X.left ⟶ T.X.left) : Prop

[Kol07, Warning 38] for marked triples: T is the disjoint union of the family Ts along ι — the underlying triples are (Triple.IsSigmaOf) and the marks agree.

Equations

• T.IsSigmaOf Ts ι = (T.IsSigmaOf (fun (i : σ) => (Ts i).toTriple) ι ∧ ∀ (i : σ), (Ts i).m = T.m)

def Hironaka.MarkedTriple.ClosedUnderSigma {k : Type u} [Field k] (Dom : MarkedTriple k → Prop) : Prop

[Kol07, Warning 38]: the class Dom of marked triples is closed under finite disjoint unions.

Equations

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

Pull-back data and Kollár's 34.1 for blow-up sequence functors

def AlgebraicGeometry.Triple.IsPullbackOf {k : Type u} [Field k] (T' T : Triple k) (h : T'.X.left ⟶ T.X.left) : Prop

[Kol07, 34.1] ("B(Y, h^* I, h^{-1}(E))"): the triple T' carries the pull-back data of T along h : T'.X.left ⟶ T.X.left — h is over Spec k, and the ideal and the ordered divisor family of T' are the inverse images of those of T. The pulled-back triple Triple.pullback of Hironaka.Sequence is the canonical instance.

Equations

• T'.IsPullbackOf T h = (CategoryTheory.CategoryStruct.comp h (T.X.left ↘ AlgebraicGeometry.Spec ↧k) = T'.X.left ↘ AlgebraicGeometry.Spec ↧k ∧ T'.I = T.I.comap h ∧ T'.E = T.E.comap h)

def Hironaka.MarkedTriple.IsPullbackOf {k : Type u} [Field k] (T' T : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) : Prop

[Kol07, 34.1] for marked triples (the footnote of Notation 64): T' carries the pull-back data of T along h and the same mark.

Equations

• T'.IsPullbackOf T h = (T'.IsPullbackOf T.toTriple h ∧ T'.m = T.m)

def Hironaka.OrderSeqAssignment.CommutesWith {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) {T T' : AlgebraicGeometry.Triple k} (h : T'.X.left ⟶ T.X.left) : Prop

[Kol07, 34.1]: a blow-up sequence functor B commutes with h if "B(Y, h^* I, h^{-1}(E)) = h^* B(X, I, E)" — for triples T', T of the class and h : T'.X.left ⟶ T.X.left, the value on T' is the pull-back (BlowUpSequence.pullback, [Kol07, Definition 30.1]) of the value on T; an equality of terms of BlowUpSequence T'.X.left, hence of centres. Used with T'.IsPullbackOf T h and [Smooth h].

Equations

• B.CommutesWith h = ∀ (hT : Dom T) (hT' : Dom T'), B.seq T' hT' = (B.seq T hT).pullback h

def Hironaka.OrderSeqAssignment.CommutesWithSmoothSurjections {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) : Prop

[Kol07, 34.1], first bullet: B commutes with smooth surjections — with every smooth surjective h : T'.X.left ⟶ T.X.left between triples of the class for which T' carries the pull-back data of T.

Equations

• B.CommutesWithSmoothSurjections = ∀ (T T' : AlgebraicGeometry.Triple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h], Function.Surjective ⇑h → T'.IsPullbackOf T h → B.CommutesWith h

def Hironaka.OrderSeqAssignment.CommutesWithSmooth {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) : Prop

[Kol07, 34.1], both bullets: B commutes with smooth morphisms — it commutes with every smooth surjection, and for every smooth h, B(Y, h^* I, h^{-1}(E)) is obtained from the pull-back h^* B(X, I, E) "by deleting every blow-up h^* π_i whose center is empty" and reindexing (BlowUpSequence.eraseEmpty).

Equations

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

def Hironaka.OrderGeSeqAssignment.CommutesWith {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) {T T' : MarkedTriple k} (h : T'.X.left ⟶ T.X.left) : Prop

[Kol07, 34.1] for marked functors: B(Y, h^* I, m, h^{-1}(E)) = h^* B(X, I, m, E).

Equations

• B.CommutesWith h = ∀ (hT : Dom T) (hT' : Dom T'), B.seq T' hT' = (B.seq T hT).pullback h

def Hironaka.OrderGeSeqAssignment.CommutesWithSmoothSurjections {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : Prop

[Kol07, 34.1], first bullet, for marked functors.

Equations

• B.CommutesWithSmoothSurjections = ∀ (T T' : Hironaka.MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h], Function.Surjective ⇑h → T'.IsPullbackOf T h → B.CommutesWith h

def Hironaka.OrderGeSeqAssignment.CommutesWithSmooth {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : Prop

[Kol07, 34.1], both bullets, for marked functors.

Equations

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

Base-change data and Kollár's 34.2 for blow-up sequence functors

def AlgebraicGeometry.Triple.IsBaseChangeOf {k : Type u} [Field k] {L : Type u} [Field L] (T' : Triple L) (T : Triple k) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) : Prop

[Kol07, 34.2] ("take the fiber product X_{L,σ} := X_K ×_{Spec K} Spec L … similarly we get I_{L,σ} and E_{L,σ}"): the triple T' over L carries the base-change data of the triple T over k along the field extension σ : k →+* L through p : T'.X.left ⟶ T.X.left — the square of p, the two structure morphisms and Spec σ is cartesian (T'.X.left = X_{L,σ}), and the ideal and the ordered divisor family of T' are the inverse images of those of T. This is the square of the change-of-fields clause of AlgebraicGeometry.exists_functorial_principalization; the base-changed triple Triple.baseChange of Hironaka.Sequence is the canonical instance.

Equations

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

def Hironaka.MarkedTriple.IsBaseChangeOf {k : Type u} [Field k] {L : Type u} [Field L] (T' : MarkedTriple L) (T : MarkedTriple k) (σ : k →+* L) (p : T'.X.left ⟶ T.X.left) : Prop

[Kol07, 34.2] for marked triples (the footnote of Notation 64): T' carries the base-change data of T along σ through p and the same mark.

Equations

• T'.IsBaseChangeOf T σ p = (T'.IsBaseChangeOf T.toTriple σ p ∧ T'.m = T.m)

def Hironaka.OrderSeqAssignment.CommutesWithBaseChange {k : Type u} [Field k] {L : Type u} [Field L] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} {Dom' : AlgebraicGeometry.Triple L → Prop} (B : OrderSeqAssignment k m Dom) (B' : OrderSeqAssignment L m Dom') (σ : k →+* L) : Prop

[Kol07, 34.2]: "we say that B commutes with σ if B(X_{L,σ}, I_{L,σ}, E_{L,σ}) is the blow-up sequence (π_i)_{L,σ} with centers (Z_i)_{L,σ}" — for the functor B over k and the functor B' over L of the same order (a blow-up sequence functor is given for every field at once in the main theorems): on triples T of B's class and T' of B''s class with T' carrying the base-change data of T along σ through p, the value on T' is the pull-back of the value on T along p (BlowUpSequence.pullback, [Kol07, Definition 30.1]: for the flat p its stages are the fibre products (X_i)_{L,σ} and its centres the (Z_i)_{L,σ}); an equality of terms of BlowUpSequence T'.X.left, hence of centres.

Equations

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

def Hironaka.OrderGeSeqAssignment.CommutesWithBaseChange {k : Type u} [Field k] {L : Type u} [Field L] {Dom : MarkedTriple k → Prop} {Dom' : MarkedTriple L → Prop} (B : OrderGeSeqAssignment k Dom) (B' : OrderGeSeqAssignment L Dom') (σ : k →+* L) : Prop

[Kol07, 34.2] for marked functors: B'(X_{L,σ}, I_{L,σ}, m, E_{L,σ}) = (B(X, I, m, E))_{L,σ}.

Equations

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

Proposition 37's setting: the affine class and the two auxiliary schemes

def AlgebraicGeometry.Triple.IsAffineScheme {k : Type u} [Field k] (T : Triple k) : Prop

[Kol07, Proposition 37] ("a blow-up sequence functor defined on affine schemes over a field k"): the class of triples whose underlying scheme is affine — the proposition's domain, closed under finite disjoint unions (closedUnderSigma_isAffine in Hironaka.Sequence).

Equations

• T.IsAffineScheme = AlgebraicGeometry.IsAffine T.X.left

noncomputable def AlgebraicGeometry.Triple.affineCover {k : Type u} [Field k] (T : Triple k) : T.X.left.OpenCover

The proof of [Kol07, Proposition 37] ("choose an open affine cover X = ∪ Uᵢ"): a finite affine open cover of the underlying scheme of T — Mathlib's affine cover, refined to a finite subcover (T.X.left is quasi-compact over Spec k).

Equations

• T.affineCover = T.X.left.affineCover.finiteSubcover

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Triple.coverScheme {k : Type u} [Field k] (T : Triple k) : Scheme

The proof of [Kol07, Proposition 37]: X' := ∐ᵢ Uᵢ, the disjoint union of the members of the finite affine cover.

Equations

• T.coverScheme = ∐ fun (i : T.affineCover.I₀) => T.affineCover.X i

noncomputable def AlgebraicGeometry.Triple.coverDesc {k : Type u} [Field k] (T : Triple k) : T.coverScheme ⟶ T.X.left

The proof of [Kol07, Proposition 37] ("a smooth surjection g : X' → X"): the morphism induced by the inclusions of the members of the cover.

Equations

• T.coverDesc = CategoryTheory.Limits.Sigma.desc T.affineCover.f

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Triple.instOverCoverScheme {k : Type u} [Field k] (T : Triple k) : T.coverScheme.Over (Spec ↧k)

X' is a scheme over Spec k through g.

Equations

• T.instOverCoverScheme = { hom := CategoryTheory.CategoryStruct.comp T.coverDesc (T.X.left ↘ AlgebraicGeometry.Spec ↧k) }

instance AlgebraicGeometry.Triple.instIsOverCoverDesc {k : Type u} [Field k] (T : Triple k) : Scheme.Hom.IsOver T.coverDesc (Spec ↧k)

g : X' → X is a morphism over Spec k.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Triple.coverPair {k : Type u} [Field k] (T : Triple k) : Scheme

The X'' := ∐_{i ≤ j} Uᵢ ∩ Uⱼ of the proof of [Kol07, Proposition 37], which one may "also think of … as the fiber product X' ×_X X'": the fibre product X' ×_X X'.

Equations

• T.coverPair = CategoryTheory.Limits.pullback T.coverDesc T.coverDesc

noncomputable def AlgebraicGeometry.Triple.coverFst {k : Type u} [Field k] (T : Triple k) : T.coverPair ⟶ T.coverScheme

The proof of [Kol07, Proposition 37]: the first projection τ₁ : X'' → X'.

Equations

• T.coverFst = CategoryTheory.Limits.pullback.fst T.coverDesc T.coverDesc

noncomputable def AlgebraicGeometry.Triple.coverSnd {k : Type u} [Field k] (T : Triple k) : T.coverPair ⟶ T.coverScheme

The proof of [Kol07, Proposition 37]: the second projection τ₂ : X'' → X'.

Equations

• T.coverSnd = CategoryTheory.Limits.pullback.snd T.coverDesc T.coverDesc

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Triple.instOverCoverPair {k : Type u} [Field k] (T : Triple k) : T.coverPair.Over (Spec ↧k)

X'' is a scheme over Spec k through τ₁.

Equations

• T.instOverCoverPair = { hom := CategoryTheory.CategoryStruct.comp T.coverFst (T.coverScheme ↘ AlgebraicGeometry.Spec ↧k) }

instance AlgebraicGeometry.Triple.instIsOverCoverFst {k : Type u} [Field k] (T : Triple k) : Scheme.Hom.IsOver T.coverFst (Spec ↧k)

τ₁ is over Spec k.

instance AlgebraicGeometry.Triple.instIsOverCoverSnd {k : Type u} [Field k] (T : Triple k) : Scheme.Hom.IsOver T.coverSnd (Spec ↧k)

τ₂ is over Spec k: τ₁ ≫ g = τ₂ ≫ g (the fibre-product square).

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

[Kol07, Proposition 37] for marked triples: the class with affine underlying scheme.

Equations

• T.IsAffineScheme = AlgebraicGeometry.IsAffine T.X.left

Closed-embedding situations and Kollár's 34.3 for blow-up sequence functors

def AlgebraicGeometry.Triple.ClosedEmbedding {k : Type u} [Field k] (TX TY : Triple k) (j : TY.X.left ⟶ TX.X.left) : Prop

The closed-embedding situation (Y, I_Y, E|_Y) ↪ (X, I_X, E) along j : Y ↪ X of [Kol07, 34.3] — j is a closed embedding of smooth k-schemes (the closed immersion is an instance argument [IsClosedImmersion j] at the use sites, as [Smooth h] in 34.1; smoothness and 0 ≠ I are the triples' fields; j is a k-morphism), the ideal sheaves satisfy 𝒪_X / I_X = j_*(𝒪_Y / I_Y) — I_X = j_* I_Y, Mathlib's IdealSheafData.map along j, the form of clause (5) of AlgebraicGeometry.exists_functorial_principalization — and E is an snc divisor on X with E|_Y snc on Y: the family of T_Y is the restriction E.comap j of that of T_X, its snc-ness being T_Y.isSnc.

Equations

• TX.ClosedEmbedding TY j = (CategoryTheory.CategoryStruct.comp j (TX.X.left ↘ AlgebraicGeometry.Spec ↧k) = TY.X.left ↘ AlgebraicGeometry.Spec ↧k ∧ TX.I = TY.I.map j ∧ TY.E = TX.E.comap j)

def Hironaka.MarkedTriple.ClosedEmbedding {k : Type u} [Field k] (TX TY : MarkedTriple k) (j : TY.X.left ⟶ TX.X.left) : Prop

[Kol07, 34.3] for marked triples ([Kol07, Claim 71.2]: BMO_1(X, I, 1, ∅) = τ_* BMO_1(Y, J, 1, ∅)): the closed-embedding situation with the same mark.

Equations

• TX.ClosedEmbedding TY j = (TX.ClosedEmbedding TY.toTriple j ∧ TY.m = TX.m)

def Hironaka.OrderSeqAssignment.CommutesWithClosedEmbeddings {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) : Prop

[Kol07, 34.3]: "we say that B commutes with closed embeddings if B(X, I_X, E) = j_* B(Y, I_Y, E|_Y)" in every closed-embedding situation between triples of the class — the value on T_X is the push-forward (BlowUpSequence.pushforward, [Kol07, Definition 30.3]) of the value on T_Y; an equality of terms of BlowUpSequence T_X.X.left, hence of centres.

Equations

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

def Hironaka.OrderSeqAssignment.CommutesWithClosedEmbeddingsOfEmptyDivisor {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) : Prop

[Kol07, Theorem 35 (5)] and [Kol07, Claim 71.2] ("in both of these claims we assume that E = ∅"): B commutes with closed embeddings whenever E = ∅ — 34.3's clause restricted to the situations whose divisor family on X (hence on Y) is empty; the form of clause (5) of AlgebraicGeometry.exists_functorial_principalization (IsEmpty E.ι).

Equations

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

def Hironaka.OrderGeSeqAssignment.CommutesWithClosedEmbeddings {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : Prop

[Kol07, 34.3] for marked functors ([Kol07, Claim 71.2]): B commutes with closed embeddings, B(X, I_X, m, E) = j_* B(Y, I_Y, m, E|_Y).

Equations

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

def Hironaka.OrderGeSeqAssignment.CommutesWithClosedEmbeddingsOfEmptyDivisor {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : Prop

[Kol07, Claim 71.2] for marked functors: B commutes with closed embeddings whenever E = ∅.

Equations

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

Theorem 105's hypotheses: a class of morphisms, global and local triples

structure Hironaka.IsGlobalizationClass (M : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : Prop

[Kol07, Theorem 105 (1)]: "a class of smooth morphisms M" closed under fibre products and coproducts (for instance all smooth morphisms, all étale morphisms or all open immersions) — a property M of morphisms of schemes (Mathlib's MorphismProperty) whose members are smooth, which is stable under base change ("closed under fiber products" as the proof uses it: "the two coordinate projections τ₁, τ₂ : X'' → X' are in M") and which is closed under coproducts (as the proof uses it: for members gᵢ : Uᵢ → X, "let X' := ∐ᵢ Uₓᵢ be the disjoint union and g : X' → X the induced M-morphism"). Kollár's third example is read as the class of coproducts of open immersions (openImmersionCoprods): the open immersions themselves are not closed under coproducts (not_isGlobalizationClass_isOpenImmersion in Hironaka.Sequence).

• smooth {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : M f → AlgebraicGeometry.Smooth f

  Every member of M is smooth.

• isStableUnderBaseChange : M.IsStableUnderBaseChange

  M is closed under fibre products: stable under base change.

• sigmaDesc {σ : Type u} {U : σ → AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} (g : (i : σ) → U i ⟶ X) : (∀ (i : σ), M (g i)) → M (CategoryTheory.Limits.Sigma.desc g)

  M is closed under coproducts: the morphism a coproduct of members induces is a member.

def AlgebraicGeometry.openImmersionCoprods : CategoryTheory.MorphismProperty Scheme

[Kol07, Theorem 105 (1)] ("all open immersions") read as its proof and Step 3 of the proof of [Kol07, Theorem 103] use it ("let g : X* → X be the coproduct of the injections X^(j) ↪ X"; "if M = {open immersions} … this is the only case we need for the proof of (103)"): f : Y ⟶ X is a coproduct of open immersions — Y is a coproduct of schemes Uᵢ (a cofan ιᵢ : Uᵢ ⟶ Y that is a colimit, as in Triple.IsSigmaOf) and every ιᵢ ≫ f : Uᵢ ⟶ X is an open immersion.

Equations

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

structure AlgebraicGeometry.Triple.GlobalizationData {k : Type u} [Field k] (M : CategoryTheory.MorphismProperty Scheme) (GT LT : Triple k → Prop) : Prop

[Kol07, Theorem 105 (2)]: "two classes of triples GT (global triples) and LT (local triples)" such that (i) for every (X, I, E) ∈ GT and x ∈ X some M-morphism gₓ : (x' ∈ Uₓ) → (x ∈ X) has (Uₓ, g^* I, g^{-1} E) in LT, and (ii) LT is closed under disjoint unions — for a class M of morphisms and two classes GT, LT of triples: (i) every point of a global triple lies in the image of an M-morphism from a local triple carrying the pull-back data (IsPullbackOf; (Uₓ, g^* I, g^{-1} E) is a triple in the sense of Notation 64 because it is in LT); (ii) LT is closed under finite disjoint unions (ClosedUnderSigma, [Kol07, Warning 38]). No inclusion LT ⊆ GT is assumed (Kollár states none); Theorem 105's "extension" is agreement on LT ∩ GT.

• exists_isPullbackOf (T : Triple k) : GT T → ∀ (x : ↥T.X.left), ∃ (T' : Triple k) (g : T'.X.left ⟶ T.X.left), M g ∧ x ∈ Set.range ⇑g ∧ T'.IsPullbackOf T g ∧ LT T'

  (i): every point of a global triple has a local triple over it along a member of M.

• closedUnderSigma : ClosedUnderSigma LT

  (ii): LT is closed under finite disjoint unions.

def Hironaka.OrderSeqAssignment.CommutesWithSurjectionsIn {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (M : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : Prop

[Kol07, Theorem 105 (3)]: "a blow-up sequence functor B defined on LT that commutes with surjections in M" — B.CommutesWith h (the equation B(Y, h^* I, h^{-1}(E)) = h^* B(X, I, E) of 34.1) for every surjective h : T'.X.left ⟶ T.X.left in M between triples of which T' carries the pull-back data of T; for M = all smooth morphisms this is CommutesWithSmoothSurjections. The same predicate on GT is the conclusion's clause for the extension B̄.

Equations

• B.CommutesWithSurjectionsIn M = ∀ (T T' : AlgebraicGeometry.Triple k) (h : T'.X.left ⟶ T.X.left), M h → Function.Surjective ⇑h → T'.IsPullbackOf T h → B.CommutesWith h

def Hironaka.OrderGeSeqAssignment.CommutesWithSurjectionsIn {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (M : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : Prop

[Kol07, Theorem 105 (3)] for marked functors: B commutes with every surjection in M between marked triples of which the source carries the pull-back data of the target.

Equations

• B.CommutesWithSurjectionsIn M = ∀ (T T' : Hironaka.MarkedTriple k) (h : T'.X.left ⟶ T.X.left), M h → Function.Surjective ⇑h → T'.IsPullbackOf T h → B.CommutesWith h

Kollár's 34.4: closed embeddings, weak form

def Hironaka.OrderSeqAssignment.WeaklyCommutesWithClosedEmbeddings {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) : Prop

[Kol07, 34.4], in the setting of (34.3): B weakly commutes with closed embeddings if "j^* B(X, I_X, E) = B(Y, I_Y, E|_Y)" — in every closed-embedding situation between triples of the class (Triple.ClosedEmbedding), the restriction to Y of the value on T_X — Kollár's j^* of [Kol07, Definition 30.2], here BlowUpSequence.pullback along the closed immersion j — is the value on T_Y; an equality of terms of BlowUpSequence T_Y.X.left, hence of centres.

Equations

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

def Hironaka.OrderSeqAssignment.WeaklyCommutesWithClosedEmbeddingsOfEmptyDivisor {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) : Prop

[Kol07, 34.4] restricted to the situations with E = ∅ — the weak counterpart of [Kol07, Theorem 35 (5)] and the form in which the proof of Theorem 36 uses the clause ("Using that BP weakly commutes with closed embeddings (34.4)", for BP(A, I_X, ∅)).

Equations

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

def Hironaka.OrderGeSeqAssignment.WeaklyCommutesWithClosedEmbeddings {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : Prop

[Kol07, 34.4] for marked functors (the notation of [Kol07, Claim 71.2], with the mark carried along): B weakly commutes with closed embeddings, j^* B(X, I_X, m, E) = B(Y, I_Y, m, E|_Y).

Equations

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

def Hironaka.OrderGeSeqAssignment.WeaklyCommutesWithClosedEmbeddingsOfEmptyDivisor {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) : Prop

[Kol07, 34.4] for marked functors, restricted to E = ∅ (the standing assumption of [Kol07, Claim 71.2]).

Equations

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

The descent datum of Proposition 37's proof

def AlgebraicGeometry.Scheme.BlowUpSequence.AgreeOnOverlaps {X : Scheme} {σ : Type u} {W : σ → Scheme} (ι : (i : σ) → W i ⟶ X) (S : (i : σ) → (W i).BlowUpSequence) : Prop

The proof of [Kol07, Proposition 37], equations (37.1)–(37.2), for whole sequences: given a family of morphisms ι i : W i ⟶ X (in the proof, the members of an affine open cover), a family of blow-up sequences S i on the W i agree on the overlaps when the pull-backs of S i and S j to the fibre product W i ×_X W j agree, for all i, j — the descent datum from which the proof reconstructs a sequence on X.

Equations

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

Theorem 105's proof: local covers and the fibre-product hypothesis

def AlgebraicGeometry.Triple.IsLocalCover {k : Type u} [Field k] (M : CategoryTheory.MorphismProperty Scheme) (GT LT : Triple k → Prop) (T T' : Triple k) (g : T'.X.left ⟶ T.X.left) : Prop

The proof of [Kol07, Theorem 105] chooses M-morphisms gₓᵢ : Uₓᵢ → X whose images cover X and forms the disjoint union X' := ∐ᵢ Uₓᵢ with "the induced M-morphism" g : X' → X, so that (X', g^* I, g^{-1} E) ∈ LT: g : T'.X.left ⟶ T.X.left is a local M-cover of the global triple T by the local triple T' — T ∈ GT, T' ∈ LT, g ∈ M, g surjective, and T' carries the pull-back data of T along g (IsPullbackOf).

Equations

• AlgebraicGeometry.Triple.IsLocalCover M GT LT T T' g = (GT T ∧ LT T' ∧ M g ∧ Function.Surjective ⇑g ∧ T'.IsPullbackOf T g)

def AlgebraicGeometry.Triple.LocalCoversFibreClosed {k : Type u} [Field k] (M : CategoryTheory.MorphismProperty Scheme) (GT LT : Triple k → Prop) : Prop

A hypothesis implicit in the proof of [Kol07, Theorem 105]: Kollár applies B to X'' := X' ×_X X' ("the blow-up sequence B for X'' starts with blowing up Z₀''; since B commutes with the τᵢ …"), which requires (X'', τ₁^* g^* I, …) ∈ LT although clauses (1)–(3) of the theorem state no such condition; the commutation and the uniqueness of the extension use Y' ×_X X' for local covers Y' → Y → X and X' → X in the same way. The class LT is closed under fibre products of local covers: for two local M-covers g₁ : T₁.X.left ⟶ T.X.left, g₂ : T₂.X.left ⟶ T.X.left of a global triple T, a triple T₁₂ whose scheme is the fibre product T₁.X.left ×_{T.X.left} T₂.X.left (IsPullback p₁ p₂ g₁ g₂) and which carries the pull-back data of T₁ along p₁ is in LT. This is closure of LT under base change along the M-morphism g₁ restricted to local covers over a common global triple; the unrestricted closure ("LT closed under base change along every M-morphism") fails for the affine class of Proposition 37 (an open subscheme of an affine scheme need not be affine, and every open immersion is a coproduct of open immersions), while this form holds in both instances used in the library (affine: X is separated, so the fibre product of affines over it is affine; maximal contact: the hypersurface restricts).

Equations

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