Going up: dropping the boundary divisor

A sequence of order ≥ m for (I, m) starting with a simple normal crossing boundary E is a sequence of order ≥ m for (I, m) starting with the empty boundary ([Kol07, Definition 66] read with the chart-wise normal crossings of [Kol07, Definition 24 (4)]). Kollár's Theorem 84 and Corollary 85 carry a boundary E, while the push-forward theorem of this library (pushforward_isOfOrderGe) is stated with the empty boundary; this module bridges the two.

• totalTransformSeqFrom F i (defined in Hironaka/Manifold/FiniteSuccession/BoundaryFamily.lean): the boundary family at stage i starting from the family F, Kollár's family of exceptional divisors [Kol07, Definition 25] along the sequence from an arbitrary start.
• isSnc_totalTransformSeqFrom_and_boundarySeq_eq: from a simple normal crossing start F, under the normal-crossings clause (3′) for the boundary red(π⁻¹E_i ∪ π⁻¹Z_i) starting with E = red F, the family F_i is a simple normal crossing family at every stage and the boundary E_i is its reduced ideal sheaf, by the induction of Hironaka/Manifold/FiniteSuccession/BoundaryFamily.lean.
• exceptionalEmb, hyp_exceptionalEmb: the exceptional divisors F_i^∅ (the family from the empty start) form a sub-family of F_i^F.
• HypersurfaceFamily.HasSncWith.of_subfamily: simple normal crossings with a family pass to a sub-family (the simple-normal-crossing chart with its component coordinates restricted).
• IsOfOrderGe.unit_of_idealSheaf: dropping the boundary. Clause (3′) for the boundary starting with red F gives (3′) for the boundary starting with 𝒪, by a joint induction carrying the invariant for the exceptional family; the order clause (4′) does not mention the boundary.

Not in the sources as a separate statement; it is what allows the going-up theorem to be applied to sequences with a boundary.

theorem Manifold.HypersurfaceFamily.HasSncWith.of_subfamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F G : HypersurfaceFamily M} (e : F.ι → G.ι) (he : Function.Injective e) (hhyp : ∀ (k : F.ι), G.hyp (e k) = F.hyp k) {Y : Set M} {c : ℕ} (h : HasSncWith ψ G Y c) : HasSncWith ψ F Y c

Simple normal crossings with a family pass to a sub-family: the simple-normal-crossing chart of G at a point, with its component coordinates restricted along the embedding of the components of F.

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

The exceptional divisors (the family from the empty start) as components of the family from the start F, by recursion on the stage.

Equations

• S.exceptionalEmb F 0 x_2 = fun (k : (S.totalTransformSeqAux 0 x_2).ι) => PEmpty.elim k
• S.exceptionalEmb F i.succ h = fun (k : (S.totalTransformSeqAux (i + 1) h).ι) => toLex (Sum.map (S.exceptionalEmb F i ⋯) id (ofLex k))

theorem AnalyticManifold.FiniteSuccession.exceptionalEmb_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : ℕ) (h : i < S.length + 1) : Function.Injective (S.exceptionalEmb F i h)

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

theorem AnalyticManifold.FiniteSuccession.isSnc_totalTransformSeqFrom_and_boundarySeq_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (h3 : ∀ (i : Fin S.length), (S.boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith (S.center i)) (i : Fin (S.length + 1)) : Manifold.HypersurfaceFamily.IsSnc ψ (S.totalTransformSeqFrom F i) ∧ S.boundarySeq F.idealSheaf i = (S.totalTransformSeqFrom F i).idealSheaf

From a simple normal crossing start F: under the normal-crossings clause (3′) for the boundary starting with red F, the family F_i from the start F is a simple normal crossing family at every stage and the boundary E_i is its reduced ideal sheaf. Clause (3′) at stage i says that E_i has only normal crossings with Z_i, which by the dictionary hasOnlyNormalCrossingsWith_idealSheaf_iff is "Z_i has simple normal crossings with F_i"; isSnc_totalTransform makes F_{i+1} a simple normal crossing family and reducedTransform_eq_idealSheaf_totalTransform identifies red(π_i⁻¹E_i ∪ π_i⁻¹Z_i) with the reduced ideal sheaf of the total transform.

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.unit_of_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {m : ℕ} (F : Manifold.HypersurfaceFamily M.carrier) (B : M.FiniteSuccession) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hge : B.IsOfOrderGe I m F.idealSheaf) : B.IsOfOrderGe I m ⊤

Dropping the boundary: a sequence of order ≥ m for (I, m) starting with the simple normal crossing boundary E = red F is of order ≥ m for (I, m) starting with the empty boundary ([Kol07, Definition 66] with [Kol07, Definition 24 (4)]). Clause (4′) does not mention the boundary. For clause (3′): the boundary E_i^F is the reduced ideal sheaf of the boundary family F_i^F from the start F (isSnc_totalTransformSeqFrom_and_boundarySeq_eq), Z_i has simple normal crossings with F_i^F, hence with the sub-family F_i^∅ of exceptional divisors (exceptionalEmb), whose reduced ideal sheaf is the boundary E_i^∅ from the empty start; this last identification is carried along the same induction, since it needs (3′) for 𝒪 at the earlier stages.