Blow-up sequence functors on triples and marked triples

A blow-up sequence functor [Kol07, Definition 31] is, after the last paragraph of [Kol07, Definition 66], an assignment (X, I, E) ↦ B(X, I, E) of a smooth blow-up sequence of order m starting with the input, on a class of triples. In this library it is the structure Hironaka.OrderSeqAssignment k m Dom of Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean (a field seq on the class Dom, the order proof isOrderSeq, and the empty blow-up convention of [Kol07, 32] as the field noEmptyCenters), with the marked version OrderGeSeqFunctor k Dom. This module proves the elementary facts about them and defines the induced triples.

• Extensionality (ext): the last two fields are proofs, so a functor is its seq; after destructing both structures the equation between the seq fields is substituted and the remaining proof fields agree by proof irrelevance.
• The induced triples (induced, endTriple): Kollár's "we consider the sheaves I_i and the divisors E_i as part of the functor" is realised by applying Triple.induced (Hironaka/Scheme/BlowUpSequence/Triple.lean) to the functor's own sequence and its own order proof; the end triple Π_*^{-1}(X, I, E) = (X_r, I_r, E_r) is its value at the last index, and its underlying scheme is the first component of the resolution functor's value endResult (endTriple_X, by rfl: both are stage (Fin.last _)).
• The resolution functor (endResult_fst, endResult_snd, isProper_endResult): the value (Π : X_r → X) is ⟨last, composite⟩ by definition; Π is the stage map at the last index, proper as a composite of blow-ups of a locally Noetherian scheme (isProper_stageMap).
• The empty blow-up convention (eraseEmpty_seq, center_ne_top, ofEraseEmpty): the field noEmptyCenters says no center is ⊤, so eraseEmpty_eq_self_iff gives del(B(X, I, E)) = B(X, I, E); the packaging ofEraseEmpty deletes the empty blow-ups of an assignment and takes noEmptyCenters_eraseEmpty for the convention, its order field being the hypothesis that the deleted sequences are of order m (IsOrderSeq.eraseEmpty of Hironaka/Scheme/BlowUpSequence/PullbackEraseEmpty.lean supplies it from the undeleted ones).

theorem Hironaka.OrderSeqAssignment.ext {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} {B B' : OrderSeqAssignment k m Dom} (h : ∀ (T : AlgebraicGeometry.Triple k) (hT : Dom T), B.seq T hT = B'.seq T hT) : B = B'

A blow-up sequence functor is its assignment of sequences [Kol07, Definition 31].

noncomputable def Hironaka.OrderSeqAssignment.induced {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} [CharZero k] (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : AlgebraicGeometry.Triple k

The triple (X_i, I_i, E_i) induced at stage i of B(X, I, E) [Kol07, Definition 66, last paragraph].

Equations

• B.induced T h i = T.induced (B.seq T h) ⋯ i

noncomputable def Hironaka.OrderSeqAssignment.endTriple {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} [CharZero k] (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : AlgebraicGeometry.Triple k

Π_*^{-1}(X, I, E) = (X_r, I_r, E_r), the triple induced at the end of B(X, I, E) [Kol07, Definition 66, last paragraph].

Equations

• B.endTriple T h = B.induced T h (Fin.last (B.seq T h).length)

theorem Hironaka.OrderSeqAssignment.induced_X {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} [CharZero k] (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).X.left = (B.seq T h).stage i

theorem Hironaka.OrderSeqAssignment.induced_I {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} [CharZero k] (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).I = (B.seq T h).weakTransformSeq T.I i

theorem Hironaka.OrderSeqAssignment.induced_E {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} [CharZero k] (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).E = (B.seq T h).totalTransformSeq T.E i

theorem Hironaka.OrderSeqAssignment.endTriple_X {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} [CharZero k] (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : (B.endTriple T h).X.left = (B.endResult T h).fst

The underlying scheme of Π_*^{-1}(X, I, E) is the scheme of the end result R(X, I, E).

theorem Hironaka.OrderSeqAssignment.endResult_fst {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : (B.endResult T h).fst = (B.seq T h).last

The end result of B(X, I, E) is the last stage X_r [Kol07, Definition 31].

theorem Hironaka.OrderSeqAssignment.endResult_snd {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : (B.endResult T h).snd = (B.seq T h).composite

The morphism of the end result is the composite Π : X_r → X [Kol07, Definition 31].

theorem Hironaka.OrderSeqAssignment.isProper_endResult {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : AlgebraicGeometry.IsProper (B.endResult T h).snd

The end result Π : X_r → X of [Kol07, Definition 31] is proper: it is the stage map at the last index, a composite of blow-ups (isProper_stageMap).

theorem Hironaka.OrderSeqAssignment.eraseEmpty_seq {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) : (B.seq T h).eraseEmpty = B.seq T h

Deleting the empty blow-ups of a value of the functor changes nothing [Kol07, 32].

theorem Hironaka.OrderSeqAssignment.center_ne_top {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (h : Dom T) (i : Fin (B.seq T h).length) : (B.seq T h).center i ≠ ⊤

No center of a value of the functor is empty [Kol07, 32].

noncomputable def Hironaka.OrderSeqAssignment.ofEraseEmpty {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (seq : (T : AlgebraicGeometry.Triple k) → Dom T → T.X.left.BlowUpSequence) (h : ∀ (T : AlgebraicGeometry.Triple k) (hT : Dom T), (seq T hT).eraseEmpty.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) : OrderSeqAssignment k m Dom

The functor packaging an assignment of sequences after deleting their empty blow-ups [Kol07, 32], given that the deleted sequences are of order m.

Equations

• Hironaka.OrderSeqAssignment.ofEraseEmpty seq h = { seq := fun (T : AlgebraicGeometry.Triple k) (hT : Dom T) => (seq T hT).eraseEmpty, isOrderSeq := h, noEmptyCenters := ⋯ }

theorem Hironaka.OrderSeqAssignment.ofEraseEmpty_seq {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (seq : (T : AlgebraicGeometry.Triple k) → Dom T → T.X.left.BlowUpSequence) (h : ∀ (T : AlgebraicGeometry.Triple k) (hT : Dom T), (seq T hT).eraseEmpty.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m) (T : AlgebraicGeometry.Triple k) (hT : Dom T) : (ofEraseEmpty seq h).seq T hT = (seq T hT).eraseEmpty

theorem Hironaka.OrderGeSeqAssignment.ext {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} {B B' : OrderGeSeqAssignment k Dom} (h : ∀ (T : MarkedTriple k) (hT : Dom T), B.seq T hT = B'.seq T hT) : B = B'

A marked blow-up sequence functor is its assignment of sequences [Kol07, Definition 66, last paragraph].

noncomputable def Hironaka.OrderGeSeqAssignment.induced {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : MarkedTriple k

The marked triple (X_i, I_i, m, E_i) induced at stage i of B(X, I, m, E) [Kol07, Definition 66, last paragraph].

Equations

• B.induced T h i = T.induced (B.seq T h) ⋯ i

noncomputable def Hironaka.OrderGeSeqAssignment.endTriple {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : MarkedTriple k

Π_*^{-1}(X, I, m, E) = (X_r, I_r, m, E_r), the marked triple induced at the end of B(X, I, m, E) [Kol07, Definition 66, last paragraph].

Equations

• B.endTriple T h = B.induced T h (Fin.last (B.seq T h).length)

theorem Hironaka.OrderGeSeqAssignment.induced_X {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).X.left = (B.seq T h).stage i

theorem Hironaka.OrderGeSeqAssignment.induced_I {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).I = (B.seq T h).markedTransformSeq T.I T.m i

theorem Hironaka.OrderGeSeqAssignment.induced_m {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).m = T.m

theorem Hironaka.OrderGeSeqAssignment.induced_E {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) (i : Fin ((B.seq T h).length + 1)) : (B.induced T h i).E = (B.seq T h).totalTransformSeq T.E i

theorem Hironaka.OrderGeSeqAssignment.endTriple_X {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} [CharZero k] (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : (B.endTriple T h).X.left = (B.endResult T h).fst

The underlying scheme of Π_*^{-1}(X, I, m, E) is the scheme of the end result.

theorem Hironaka.OrderGeSeqAssignment.endResult_fst {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : (B.endResult T h).fst = (B.seq T h).last

The end result of B(X, I, m, E) is the last stage X_r [Kol07, Definition 31].

theorem Hironaka.OrderGeSeqAssignment.endResult_snd {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : (B.endResult T h).snd = (B.seq T h).composite

The morphism of the end result of B(X, I, m, E) is the composite Π : X_r → X [Kol07, Definition 31].

theorem Hironaka.OrderGeSeqAssignment.isProper_endResult {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : AlgebraicGeometry.IsProper (B.endResult T h).snd

The end result of a marked blow-up sequence functor is proper.

theorem Hironaka.OrderGeSeqAssignment.eraseEmpty_seq {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) : (B.seq T h).eraseEmpty = B.seq T h

Deleting the empty blow-ups of a value of a marked functor changes nothing [Kol07, 32].

theorem Hironaka.OrderGeSeqAssignment.center_ne_top {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (h : Dom T) (i : Fin (B.seq T h).length) : (B.seq T h).center i ≠ ⊤

No center of a value of a marked functor is empty [Kol07, 32].

noncomputable def Hironaka.OrderGeSeqAssignment.ofEraseEmpty {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (seq : (T : MarkedTriple k) → Dom T → T.X.left.BlowUpSequence) (h : ∀ (T : MarkedTriple k) (hT : Dom T), (seq T hT).eraseEmpty.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) : OrderGeSeqAssignment k Dom

The marked functor packaging an assignment of sequences after deleting their empty blow-ups [Kol07, 32].

Equations

• Hironaka.OrderGeSeqAssignment.ofEraseEmpty seq h = { seq := fun (T : Hironaka.MarkedTriple k) (hT : Dom T) => (seq T hT).eraseEmpty, isOrderGeSeq := h, noEmptyCenters := ⋯ }

theorem Hironaka.OrderGeSeqAssignment.ofEraseEmpty_seq {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (seq : (T : MarkedTriple k) → Dom T → T.X.left.BlowUpSequence) (h : ∀ (T : MarkedTriple k) (hT : Dom T), (seq T hT).eraseEmpty.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) (T : MarkedTriple k) (hT : Dom T) : (ofEraseEmpty seq h).seq T hT = (seq T hT).eraseEmpty