Truncation of a blow-up sequence

The proof of the going-up theorem for D-balanced ideals [Kol07, 90, the proof of Theorem 84] proceeds "by induction, assum[ing] that this already holds for blow-up sequences of length < r", and applies the hypothesis to the prefix Π_{r−1} : X_{r−1} → X of the pushed-forward sequence. BlowUpSequence is a list of centers built from the front, so the prefix has to be built: S.take k keeps the first k blow-ups (all of them if k ≥ S.length). This module records its bookkeeping:

• take, with length_take and pushforward_take ((T.take k).pushforward j = (T.pushforward j).take k);
• the prefix has the same stages, centers, structure maps and induced data as the sequence at every index it has: stage_take_mk (an equality of schemes), and HEq transports of markedTransformSeq, weakTransformSeq, totalTransformSeq, strictTransformSeq, center, stageMap and of the stage inclusions pushforwardStageHom of Hironaka/Scheme/BlowUpSequence/Pushforward.lean; heterogeneous because the stage types differ syntactically; stated on explicit indices ⟨j, hj⟩;
• the prefix of a smooth sequence is smooth, the prefix of a sequence of order ≥ m is of order ≥ m, and, in the form the induction of the going-up theorem uses, the prefix of length k is of order ≥ m as soon as the smoothness, normal-crossing and order clauses hold at the stages < k (isOrderGeSeq_take_of_forall_lt);
• two transport helpers for points and orders along an equality of schemes (ord_cast_of_heq, apply_cast_of_heq).

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.take {X : Scheme} : X.BlowUpSequence → ℕ → X.BlowUpSequence

The first k blow-ups of a sequence (all of them if k ≥ length): the prefix Π_{r−1} of [Kol07, 90, the proof of Theorem 84].

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹).take x✝ = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).take 0 = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).take k.succ = AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D (rest.take k)

@[simp]

theorem AlgebraicGeometry.Scheme.BlowUpSequence.take_nil {X : Scheme} (k : ℕ) : (nil X).take k = nil X

@[simp]

theorem AlgebraicGeometry.Scheme.BlowUpSequence.take_cons_zero {X : Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) : (cons X D rest).take 0 = nil X

@[simp]

theorem AlgebraicGeometry.Scheme.BlowUpSequence.take_cons_succ {X : Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (k : ℕ) : (cons X D rest).take (k + 1) = cons X D (rest.take k)

Length and pushforward

theorem AlgebraicGeometry.length_take {X : Scheme} (S : X.BlowUpSequence) (k : ℕ) : (S.take k).length = min k S.length

theorem AlgebraicGeometry.length_take_of_le {X : Scheme} (S : X.BlowUpSequence) {k : ℕ} (hk : k ≤ S.length) : (S.take k).length = k

theorem AlgebraicGeometry.take_of_length_le {X : Scheme} (S : X.BlowUpSequence) {k : ℕ} (hk : S.length ≤ k) : S.take k = S

theorem AlgebraicGeometry.pushforward_take {X Y : Scheme} (T : Y.BlowUpSequence) (j : Y ⟶ X) [IsClosedImmersion j] (k : ℕ) : (T.take k).pushforward j = (T.pushforward j).take k

Truncation commutes with the pushforward along a closed immersion.

The prefix has the same stages and induced data

theorem AlgebraicGeometry.stage_take_mk {X : Scheme} (S : X.BlowUpSequence) (k j : ℕ) (hj : j < (S.take k).length + 1) (hj' : j < S.length + 1) : (S.take k).stage ⟨j, hj⟩ = S.stage ⟨j, hj'⟩

theorem AlgebraicGeometry.markedTransformSeq_take_heq_mk {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (c k j : ℕ) (hj : j < (S.take k).length + 1) (hj' : j < S.length + 1) : (S.take k).markedTransformSeq J c ⟨j, hj⟩ ≍ S.markedTransformSeq J c ⟨j, hj'⟩

theorem AlgebraicGeometry.weakTransformSeq_take_heq_mk {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (k j : ℕ) (hj : j < (S.take k).length + 1) (hj' : j < S.length + 1) : (S.take k).weakTransformSeq J ⟨j, hj⟩ ≍ S.weakTransformSeq J ⟨j, hj'⟩

theorem AlgebraicGeometry.totalTransformSeq_take_heq_mk {X : Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (k j : ℕ) (hj : j < (S.take k).length + 1) (hj' : j < S.length + 1) : (S.take k).totalTransformSeq E ⟨j, hj⟩ ≍ S.totalTransformSeq E ⟨j, hj'⟩

theorem AlgebraicGeometry.strictTransformSeq_take_heq_mk {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (k j : ℕ) (hj : j < (S.take k).length + 1) (hj' : j < S.length + 1) : (S.take k).strictTransformSeq J ⟨j, hj⟩ ≍ S.strictTransformSeq J ⟨j, hj'⟩

theorem AlgebraicGeometry.center_take_heq_mk {X : Scheme} (S : X.BlowUpSequence) (k j : ℕ) (hj : j < (S.take k).length) (hj' : j < S.length) : (S.take k).center ⟨j, hj⟩ ≍ S.center ⟨j, hj'⟩

theorem AlgebraicGeometry.heq_comp_right {A B Y Z : Scheme} (e : A = B) {a : A ⟶ Y} {b : B ⟶ Y} (h : a ≍ b) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp a g ≍ CategoryTheory.CategoryStruct.comp b g

Heterogeneously equal morphisms stay heterogeneously equal after composing with a fixed morphism (the sources are equal schemes).

theorem AlgebraicGeometry.stageMap_take_heq_mk {X : Scheme} (S : X.BlowUpSequence) (k j : ℕ) (hj : j < (S.take k).length + 1) (hj' : j < S.length + 1) : (S.take k).stageMap ⟨j, hj⟩ ≍ S.stageMap ⟨j, hj'⟩

theorem AlgebraicGeometry.pushforwardStageHom_take_heq_mk {X Y : Scheme} (T : Y.BlowUpSequence) (j : Y ⟶ X) [IsClosedImmersion j] (k n : ℕ) (hn : n < (T.take k).length + 1) (hn' : n < T.length + 1) : (T.take k).pushforwardStageHom j ⟨n, hn⟩ ≍ T.pushforwardStageHom j ⟨n, hn'⟩

The stage inclusions of the prefix into the pushed-forward stages are those of the sequence.

Smoothness and order pass to the prefix

theorem AlgebraicGeometry.isSmooth_take {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) {S : X.BlowUpSequence} (h : S.IsSmooth f) (l : ℕ) : (S.take l).IsSmooth f

theorem AlgebraicGeometry.isOrderGeSeq_take_of_forall_lt {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (S : X.BlowUpSequence) (hsm : S.IsSmooth f) (l : ℕ) (hlt : ∀ (i : Fin S.length), ↑i < l → (S.totalTransformSeq E i.castSucc).HasSncWith (S.center i) ∧ (S.markedTransformSeq I m i.castSucc).LeOrdAlong (S.center i).support ↑m) : (S.take l).IsOrderGeSeq f I m E

The prefix of length l is a smooth blow-up sequence of order ≥ m for (X, I, m, E) as soon as the sequence is smooth and its normal-crossing and order clauses hold at the stages < l; the form in which the induction hypothesis of [Kol07, 90] is applied.

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

The prefix of a sequence of order ≥ m is of order ≥ m.

Transport along an equality of schemes

theorem AlgebraicGeometry.ord_cast_of_heq {X X' : Scheme} (e : X = X') {J : X.IdealSheafData} {J' : X'.IdealSheafData} (h : J ≍ J') (x : ↥X) : J'.ord (cast ⋯ x) = J.ord x

The order of heterogeneously equal ideal sheaves at corresponding points.

theorem AlgebraicGeometry.apply_cast_of_heq {X X' Y Y' : Scheme} (eX : X = X') (eY : Y = Y') {φ : X ⟶ Y} {φ' : X' ⟶ Y'} (h : φ ≍ φ') (x : ↥X) : φ' (cast ⋯ x) = cast ⋯ (φ x)

Heterogeneously equal morphisms agree at corresponding points.