The induced triple at the last stage of a blow-up sequence

Step 2.1 of the proof of Theorem 103 applies Lemma 102 to one boundary member after another ([Kol07, 104, Step 2.1.j]: given the sequence constructed so far, with end result Π_{r(j-1)} : X_{r(j-1)} → ⋯ → X_0, "apply (102) to (X_{r(j-1)}, I_{r(j-1)}, E_{r(j-1)})"). After a sequence of centres L of order ≥ m starting with (M, 𝓘, E), the data at the last stage, the controlled transform I_r of (𝓘, m) (markedTransformSeq; Kollár's birational transform of the marked ideal, [Kol07, Definition 60]) and the total transform E_r of the boundary ([Kol07, Definition 25]), form again an analytic triple, the induced triple, and it lies in the class BOClass m when (M, 𝓘, E) does.

• isNonzeroEverywhere_markedTransformSeq — the controlled transforms of an ideal sheaf nonzero everywhere are nonzero everywhere: the stalk of a controlled transform is the colon of the total transform's stalk by a power of the exceptional ideal ([Kol07, Definition 60]), which contains it, and the total transform's stalk is the image of a nonzero ideal under the injective germ map of the blowing-up.
• finite_nonempty_totalTransform, finite_nonempty_totalTransformSeqFrom — only finitely many members of the boundary stay nonempty along the sequence: the strict transform of an empty member is empty, and one exceptional divisor is added per blow-up.
• AnalyticTriple.induced T m L hL, boClass_induced, boundarySeq_last_eq_idealSheaf — the induced triple, its class (the order bound persists along a sequence of order ≥ m), and the identification of the boundary ideal sheaf at the last stage with the ideal sheaf of the induced boundary.
• FiniteSuccession.originalIdx — the index of the strict transform of an original member E^j in the boundary at a stage (hyp_originalIdx), the exceptional divisors being appended after the original members at every step.

The induced triple is the input of the next application of Lemma 102 in Step21Defs.lean.

The controlled transforms of a nonzero ideal sheaf are nonzero

theorem Hironaka.Manifold.isNonzeroEverywhere_markedTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (h : S.IsOfOrderGe I m E₀) (i : Fin (S.length + 1)) : Manifold.IdealSheaf.IsNonzeroEverywhere (S.markedTransformSeq I m i)

Along a sequence of order ≥ m for (𝓘, m) ([Kol07, Definition 66 (1′)] with the transform of [Kol07, Definition 60]), every controlled transform of an ideal sheaf nonzero everywhere is nonzero everywhere: the stalk of the controlled transform at a' is the colon of the total transform's stalk by a power of the exceptional ideal, which contains the total transform's stalk, the image of the nonzero stalk of I_i at π a' under the injective germ map of the blowing-up. Not in the sources; the hypothesis of [Kol07, Definition 31 (1)] for the induced triple.

Finitely many nonempty members along the sequence

theorem Hironaka.Manifold.strictTransformSet_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {M' : Type u} [TopologicalSpace M'] (π : M' → M.carrier) (Y : Set M.carrier) : Manifold.strictTransformSet π Y ∅ = ∅

The strict transform of the empty set is empty.

theorem Hironaka.Manifold.finite_nonempty_totalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {M' : Type u} [TopologicalSpace M'] (π : M' → M.carrier) (Y : Set M.carrier) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) : Finite { k : (Manifold.HypersurfaceFamily.totalTransform π Y F).ι // (Manifold.HypersurfaceFamily.totalTransform π Y F).hyp k ≠ ∅ }

The total transform ([Kol07, Definition 25]) of a family with finitely many nonempty members has finitely many nonempty members: the strict transform of an empty member is empty, and one exceptional divisor is added.

theorem Hironaka.Manifold.finite_nonempty_totalTransformSeqFrom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) (i : Fin (S.length + 1)) : Finite { k : (S.totalTransformSeqFrom F i).ι // (S.totalTransformSeqFrom F i).hyp k ≠ ∅ }

Along any sequence, the boundary from a start with finitely many nonempty members has finitely many nonempty members at every stage.

The induced triple

noncomputable def Manifold.AnalyticTriple.induced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : AnalyticTriple ψ₀ (L.stage (Fin.last L.length))

The induced triple (X_j, I_j, E_j) of [Kol07, 104, Step 2.1.j] at the last stage of a sequence L of order ≥ m starting with (M, 𝓘, E): the controlled transform I_r, nonzero everywhere (isNonzeroEverywhere_markedTransformSeq), and the total transform E_r of the boundary ([Kol07, Definition 25]), which has simple normal crossings by clause (3′) of [Kol07, Definition 66].

Equations

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

@[simp]

theorem Manifold.AnalyticTriple.induced_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : (T.induced m L hL).I = L.toSuccession.markedTransformSeq T.I m (Fin.last L.toSuccession.length)

@[simp]

theorem Manifold.AnalyticTriple.induced_F {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : (T.induced m L hL).F = L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)

theorem Manifold.AnalyticTriple.boundarySeq_last_eq_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : L.toSuccession.boundarySeq T.F.idealSheaf (Fin.last L.toSuccession.length) = (T.induced m L hL).F.idealSheaf

The boundary ideal sheaf of L at its last stage is the ideal sheaf of the induced boundary family.

theorem Manifold.AnalyticTriple.boClass_induced {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (m : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (hT : BOClass m T) : BOClass m (T.induced m L hL)

The induced triple of a triple of the class BOClass m lies in the class: the mark is kept, the controlled transform has order ≤ m everywhere (ord_markedTransformSeq_le), and finitely many members of the boundary are nonempty.

The index of an original member along the sequence

def AnalyticManifold.FiniteSuccession.originalIdxAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (k : ℕ) (h : k < S.length + 1) : F.ι → (S.totalTransformSeqFromAux F k h).ι

The index of the strict transform of the original member j in the boundary at stage k, by recursion on k (the exceptional divisors are appended after the original members at every step); the applications of Lemma 102 in Step 2.1 of the proof of [Kol07, Theorem 103] are to these strict transforms.

Equations

• S.originalIdxAux F 0 x_3 x = x
• S.originalIdxAux F k.succ h x = toLex (Sum.inl (S.originalIdxAux F k ⋯ x))

def AnalyticManifold.FiniteSuccession.originalIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : Fin (S.length + 1)) (j : F.ι) : (S.totalTransformSeqFrom F i).ι

The index of the strict transform of the original member j in the boundary at stage i.

Equations

• S.originalIdx F i j = S.originalIdxAux F ↑i ⋯ j

theorem AnalyticManifold.FiniteSuccession.hyp_originalIdxAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (k : ℕ) (h : k < S.length + 1) (j : F.ι) : (S.totalTransformSeqFromAux F k h).hyp (S.originalIdxAux F k h j) = S.strictTransformSeqAux (F.hyp j) k h

The member indexed by originalIdxAux is the strict transform of the original member ([Kol07, Definition 25]).

theorem AnalyticManifold.FiniteSuccession.hyp_originalIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : Fin (S.length + 1)) (j : F.ι) : (S.totalTransformSeqFrom F i).hyp (S.originalIdx F i j) = S.strictTransformSeq (F.hyp j) i

The member indexed by originalIdx is the strict transform of the original member.