Sequences of order m and of order ≥ m: constructor lemmas and the two recursions

A smooth blow-up sequence of order m is defined by the recursion (1) I_{i+1} := (π_i)^{-1}_* I_i (the birational transform [Kol07, Definition 48]) with the clauses (3) Z_i has normal crossings with E_i and (4) ord_{Z_i} I_i = m, and a sequence of order ≥ m by the marked recursion (1′) (I_{i+1}, m) := (π_i)^{-1}_*(I_i, m) [Kol07, Definition 60] with (4′) ord_{Z_i} I_i ≥ m [Kol07, Definition 66]. This module proves, for IsOfOrder and IsOfOrderGe:

• The empty sequence satisfies both notions vacuously (isOfOrder_nil, isOfOrderGe_nil).
• The constructor form cons ψ hY rest: the clauses at the first step are the clauses of the head (the centre Y = cosupp I_Y, the boundary E_0 = E₀ and the ideal I_0 = I, definitionally), and the clauses at the later steps are those of rest for the induced data. The induced boundary E_1 = (π_0)^{-1}_{tot} E₀ is the reduced transform reducedTransform by the first blow-down (cons_boundarySeq_succ), the induced ideal I_1 = (π_0)^{-1}_* I is the weak transform weakTransform (cons_weakTransformSeq_succ), and the induced marked ideal (I_1, m) is the sequence's own first marked transform (cons_markedTransformSeqAux_succ; birationalTransform runs at the witnesses chosen from isMonoidal, so the constructor form names it through the recursion itself). Each recursion lemma is an induction on the stage, rfl at every step because cons puts the head before the fields of rest by Fin.cases over finStages.
• The projections of the two clauses (hasOnlyNormalCrossingsWith, ordAlong_eq, le_ordAlong).
• The comparison of the recursions (Kollár's "we pretend that ord_Z I = m" of [Kol07, Definition 60]): along a sequence of order m, the marked transforms (I_i, m) are the birational transforms I_i (markedTransformSeq_eq_weakTransformSeq). At each step both are characterized by their colon stalks (π^*I_i)_{a'} : I_{F,a'}^{e(a')} (IsDivExceptional): the marked transform divides by I_F^m everywhere, the weak transform by I_F^{ν} with ν the generic order of I_i along the component of Z_i under the point. Clause (4) makes ν = m over the centre; off the exceptional divisor I_F is the unit ideal and any exponent gives the same colon. The two ideal sheaves therefore satisfy the same stalkwise characterization and coincide (IsDivExceptional.unique); this one-blowing-up comparison is birationalTransform_eq_weakTransformOf_of_ordAlong_eq of BlowUp/Transform/MarkedWeak.lean, while IsDivExceptional.congr_exponent below records the exponent observation on its own and is not used. Hence a sequence of order m is a sequence of order ≥ m (IsOfOrder.isOfOrderGe), the reading Kollár uses in the proof of [Kol07, Theorem 80]; the algebraic counterpart is IsOrderSeq.isOrderGeSeq.

theorem Manifold.IdealSheaf.IsDivExceptional.congr_exponent {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {Itot IF J' : IdealSheaf 𝒪} {e₁ e₂ : ↑X → ℕ} (he : ∀ a ∈ IF.support, e₁ a = e₂ a) (h : Itot.IsDivExceptional IF e₁ J') : Itot.IsDivExceptional IF e₂ J'

The exponent of IsDivExceptional matters only on the cosupport of I_F: off it the stalk of I_F is the unit ideal, whose powers are all the unit ideal, so every exponent gives the same colon stalk. Not in the sources. It records the observation behind the comparison of the two recursions, which the proof below obtains from birationalTransform_eq_weakTransformOf_of_ordAlong_eq of BlowUp/Transform/MarkedWeak.lean; this lemma itself is not used.

The recursions of the boundary and of the marked transforms on cons

theorem AnalyticManifold.FiniteSuccession.cons_boundarySeqAux_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (E₀ : M.IdealSheaf) (k : ℕ) (h : k + 1 < (cons ψ hY rest).length + 1) : (cons ψ hY rest).boundarySeqAux E₀ (k + 1) h = rest.boundarySeqAux (IdealSheaf.reducedTransform (Manifold.blowUpπ ψ hY) E₀ hY.idealSheaf) k ⋯

The boundary recursion E_{i+1} = (π_i)^{-1}_{tot} E_i [Kol07, Definition 66 (1)] on the constructor form: the boundaries of cons ψ hY rest after the first step are those of rest starting from the reduced transform of E₀ by the blow-down with centre I_Y.

theorem AnalyticManifold.FiniteSuccession.cons_boundarySeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (E₀ : M.IdealSheaf) (j : Fin (rest.length + 1)) : (cons ψ hY rest).boundarySeq E₀ j.succ = rest.boundarySeq (IdealSheaf.reducedTransform (Manifold.blowUpπ ψ hY) E₀ hY.idealSheaf) j

The boundary recursion on cons, indexed by Fin.

theorem AnalyticManifold.FiniteSuccession.cons_markedTransformSeqAux_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) (m k : ℕ) (h : k + 1 < (cons ψ hY rest).length + 1) : (cons ψ hY rest).markedTransformSeqAux J m (k + 1) h = rest.markedTransformSeqAux ((cons ψ hY rest).markedTransformSeqAux J m 1 ⋯) m k ⋯

The marked recursion [Kol07, Definition 66 (1′)] on the constructor form: the marked transforms of cons ψ hY rest after the first step are those of rest starting from the first marked transform of the whole sequence (birationalTransform at the witnesses chosen from isMonoidal).

theorem AnalyticManifold.FiniteSuccession.cons_boundarySeq_succ_castSucc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (E₀ : M.IdealSheaf) (i : Fin rest.length) : (cons ψ hY rest).boundarySeq E₀ i.succ.castSucc = rest.boundarySeq (IdealSheaf.reducedTransform (Manifold.blowUpπ ψ hY) E₀ hY.idealSheaf) i.castSucc

The boundary at the stage i + 1 of cons ψ hY rest, indexed as the clause of IsOfOrder indexes it.

theorem AnalyticManifold.FiniteSuccession.cons_weakTransformSeq_succ_castSucc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (I : M.IdealSheaf) (i : Fin rest.length) : (cons ψ hY rest).weakTransformSeq I i.succ.castSucc = rest.weakTransformSeq (IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) I hY.idealSheaf) i.castSucc

The weak transform at the stage i + 1 of cons ψ hY rest (cons_weakTransformSeq_succ), indexed as the clause of IsOfOrder indexes it.

theorem AnalyticManifold.FiniteSuccession.cons_markedTransformSeq_succ_castSucc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (I : M.IdealSheaf) (m : ℕ) (i : Fin rest.length) : (cons ψ hY rest).markedTransformSeq I m i.succ.castSucc = rest.markedTransformSeq ((cons ψ hY rest).markedTransformSeq I m (Fin.succ 0)) m i.castSucc

The marked transform at the stage i + 1 of cons ψ hY rest, indexed as the clause of IsOfOrderGe indexes it.

The empty sequence, the constructor form, the projections

theorem AnalyticManifold.FiniteSuccession.isOfOrder_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I E₀ : M.IdealSheaf) (m : ℕ) : (nil M).IsOfOrder I E₀ m

The empty sequence is of order m for every (M, I, E₀): there is no step to check [Kol07, Definition 66].

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I E₀ : M.IdealSheaf) (m : ℕ) : (nil M).IsOfOrderGe I m E₀

The empty sequence is of order ≥ m for every (M, I, m, E₀) [Kol07, Definition 66].

theorem AnalyticManifold.FiniteSuccession.IsOfOrder.hasOnlyNormalCrossingsWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrder I E₀ m) (i : Fin S.length) : (S.boundarySeq E₀ i.castSucc).HasOnlyNormalCrossingsWith (S.center i)

The normal-crossings clause [Kol07, Definition 66 (3)].

theorem AnalyticManifold.FiniteSuccession.IsOfOrder.ordAlong_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrder I E₀ m) (i : Fin S.length) {a : (S.stage i.castSucc).carrier} (ha : a ∈ Manifold.IdealSheaf.support (S.center i)) : Manifold.IdealSheaf.ordAlongIdeal (S.center i) (S.weakTransformSeq I i.castSucc) a = ↑m

The order clause [Kol07, Definition 66 (4)].

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.hasOnlyNormalCrossingsWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrderGe I m E₀) (i : Fin S.length) : (S.boundarySeq E₀ i.castSucc).HasOnlyNormalCrossingsWith (S.center i)

The normal-crossings clause [Kol07, Definition 66 (3′)].

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.le_ordAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrderGe I m E₀) (i : Fin S.length) {a : (S.stage i.castSucc).carrier} (ha : a ∈ Manifold.IdealSheaf.support (S.center i)) : ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (S.center i) (S.markedTransformSeq I m i.castSucc) a

The order clause [Kol07, Definition 66 (4′)].

theorem AnalyticManifold.FiniteSuccession.isOfOrder_cons_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (I E₀ : M.IdealSheaf) (m : ℕ) (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) : (cons ψ hY rest).IsOfOrder I E₀ m ↔ (E₀.HasOnlyNormalCrossingsWith hY.idealSheaf ∧ ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal I a = ↑m) ∧ rest.IsOfOrder (IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) I hY.idealSheaf) (IdealSheaf.reducedTransform (Manifold.blowUpπ ψ hY) E₀ hY.idealSheaf) m

[Kol07, Definition 66 (1)–(4)] on the constructor form: cons ψ hY rest is of order m for (M, I, E₀) iff the head clauses hold at the first centre Y and rest is of order m for the induced data ((π_0)^{-1}_* I, (π_0)^{-1}_{tot} E₀). The first step's clauses are those at index 0 (definitional, with cosupp I_Y = Y); the later steps' clauses are transported by the three recursion lemmas above.

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_cons_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (I E₀ : M.IdealSheaf) (m : ℕ) (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) : (cons ψ hY rest).IsOfOrderGe I m E₀ ↔ (E₀.HasOnlyNormalCrossingsWith hY.idealSheaf ∧ ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) ∧ rest.IsOfOrderGe ((cons ψ hY rest).markedTransformSeq I m (Fin.succ 0)) m (IdealSheaf.reducedTransform (Manifold.blowUpπ ψ hY) E₀ hY.idealSheaf)

[Kol07, Definition 66 (1′)–(4′)] on the constructor form: cons ψ hY rest is of order ≥ m for (M, I, m, E₀) iff the head clauses hold at Y and rest is of order ≥ m for the induced marked data, the marked transform of the head being written through the sequence's own recursion (since birationalTransform runs at the witnesses chosen from isMonoidal).

The two recursions agree along a sequence of order m

theorem AnalyticManifold.FiniteSuccession.IsOfOrder.markedTransformSeq_eq_weakTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrder I E₀ m) (i : Fin (S.length + 1)) : S.markedTransformSeq I m i = S.weakTransformSeq I i

Along a sequence of order m the marked transforms (I_i, m) are the birational transforms I_i (Kollár's "we pretend that ord_Z I = m" [Kol07, Definition 60], with the birational transform of [Kol07, Definition 48] along the two recursions of [Kol07, Definition 66]). Induction on the stage: at a step both transforms are the ideal sheaf with colon stalks (π^*I_i : I_F^{e}), with the constant exponent m for the marked transform (which needs m ≤ ord_{Z_i} I_i, clause (4)) and the generic order along the centre for the weak transform, which is m over the centre by clause (4) and irrelevant off the exceptional divisor; the colon characterization determines the ideal sheaf.

theorem AnalyticManifold.FiniteSuccession.IsOfOrder.isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrder I E₀ m) : S.IsOfOrderGe I m E₀

A sequence of order m is a sequence of order ≥ m: the marked transforms are the birational transforms, whose order along the centres is m. This is the reading of "a smooth blow-up sequence of order m starting with (X, I)" as a sequence of order ≥ m starting with (X, I, m) used in the proof of [Kol07, Theorem 80]; the algebraic counterpart is IsOrderSeq.isOrderGeSeq.