Corollary 85 with the hypersurface in the boundary

In the proof of [Kol07, Lemma 102] the going-up theorem gives a blow-up sequence of order m starting with (X_0, I_0, E - E^j), and, S being E^j, "every blow-up center is a smooth subvariety" of the transform of E^j, so that one has in fact a blow-up sequence of order m starting with (X_0, I_0, E). This module is that sentence: the going-up statement [Kol07, Corollary 85] for the push-forward along a closed hypersurface S, with the boundary F + S (HypersurfaceFamily.append) in place of F.

• HypersurfaceFamily.support_append, FiniteSuccession.isClosed_hyp_totalTransformSeqFrom, FiniteSuccession.support_totalTransformSeqFrom_append — the support of the boundary family from the start F + S at stage i is the support from the start F together with the strict transform S_i (the exceptional divisors already lie in the family from F, and the preimage of S_i is S_{i+1} up to the exceptional divisor).
• FiniteSuccession.pushforward_hasOnlyNormalCrossingsWith_center_append_of_forall_lt — the normal-crossings clause of the push-forward with the boundary F + S at stage i, from the clause of the sequence on S with the boundary F|_S: the boundary at stage i is the reduced ideal sheaf of F_i + S_i, and the lifting with the hypersurface appended (BDLift.lean) lifts the clause through the identification of the stages of the restricted sequence.
• FiniteSuccession.pushforward_isOfOrderGe_append — [Kol07, Corollary 85] with S in the boundary: for I D-balanced with ord I ≤ m everywhere, the push-forward of a sequence of order ≥ m for (I|_S, m) with the boundary F|_S is of order ≥ m for (I, m) with the boundary F + S; the order clause does not involve the boundary (le_ordAlong_pushforward).

It is used in BDCore.lean for the order clause of Lemma 102 and in BDCosupp.lean for its clause (1).

theorem Manifold.HypersurfaceFamily.support_append {M : Type u} (F : HypersurfaceFamily M) (H : Set M) : (F.append H).support = F.support ∪ H

The support of F + H is the support of F together with H.

theorem AnalyticManifold.FiniteSuccession.isClosed_hyp_totalTransformSeqFrom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : ∀ (j : F.ι), IsClosed (F.hyp j)) (i : Fin (B.length + 1)) (k : (B.totalTransformSeqFrom F i).ι) : IsClosed ((B.totalTransformSeqFrom F i).hyp k)

Along any succession of blow-ups the members of the boundary family from a start with closed members stay closed.

theorem AnalyticManifold.FiniteSuccession.support_totalTransformSeqFrom_append {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : ∀ (j : F.ι), IsClosed (F.hyp j)) {S : Set M.carrier} (hS : IsClosed S) (i : Fin (B.length + 1)) : (B.totalTransformSeqFrom (F.append S) i).support = (B.totalTransformSeqFrom F i).support ∪ B.strictTransformSeq S i

[Kol07, Definition 25] with the hypersurface appended: the support of the boundary family from the start F + S at stage i is the support from the start F together with the strict transform S_i, since the preimage of S_i is S_{i+1} together with the exceptional divisor, which the family from F already carries.

theorem AnalyticManifold.FiniteSuccession.pushforward_hasOnlyNormalCrossingsWith_center_append_of_forall_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {m : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) {J : hS.toAnalyticManifold.IdealSheaf} (hge : T.IsOfOrderGe J m (hS.traceFamily F).idealSheaf) (i : Fin T.length) (h3 : ∀ (i' : Fin T.length), ↑i' < ↑i → ((pushforward hS T).boundarySeq (F.append S).idealSheaf i'.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i')) : ((pushforward hS T).boundarySeq (F.append S).idealSheaf i.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i)

The normal-crossings clause of the push-forward with the boundary F + S at stage i, given it at the stages < i: the boundary at stage i is the reduced ideal sheaf of F_i + S_i, and the clause of the sequence T on S lifts through the identification of the stages of T with those of the restriction of the push-forward to S by hasOnlyNormalCrossingsWith_idealSheaf_append_of_traceFamily (the proof of [Kol07, Lemma 102], "every blow-up center is a smooth subvariety" of the transform of E^j).

theorem AnalyticManifold.FiniteSuccession.pushforward_isOfOrderGe_append {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {I : M.IdealSheaf} {m : ℕ} [FiniteDimensional 𝕜 E] {F : Manifold.HypersurfaceFamily M.carrier} (hI : Manifold.IdealSheaf.IsDBalanced I m) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I) m (hS.traceFamily F).idealSheaf) : (pushforward hS T).IsOfOrderGe I m (F.append S).idealSheaf

[Kol07, Corollary 85] with the hypersurface in the boundary (the proof of [Kol07, Lemma 102]): for I D-balanced with ord I ≤ m everywhere and F with simple normal crossings having simple normal crossings with the closed hypersurface S properly, the push-forward of a sequence of order ≥ m for (I|_S, m) with the boundary F|_S is of order ≥ m for (I, m) with the boundary F + S. The order clause is le_ordAlong_pushforward and does not involve the boundary; the normal-crossings clause is pushforward_hasOnlyNormalCrossingsWith_center_append_of_forall_lt, stage by stage.