Kollár's Corollary 85: going up and down with a boundary

Kollár's Corollary 85 [Kol07, Corollary 85]: with I D-balanced of maximal order m, H a smooth hypersurface of maximal contact and E a simple normal crossing divisor such that E + H is a simple normal crossing divisor, pushing forward from H to X is a one-to-one correspondence between smooth blow-up sequences of order ≥ m starting with (H, I|_H, m, E|_H) and smooth blow-up sequences of order m starting with (X, I, E). This module proves both directions with the boundary E = red F, for F a simple normal crossing family having simple normal crossings with H properly.

Going up, (1) ⇒ (2): a sequence T of order ≥ m for (I|_H, m) with the boundary E|_H pushes forward to a sequence of order exactly m for (I, m) with the boundary E. The order clause is Kollár's induction [Kol07, 90] (le_ordAlong_pushforward, which does not look at the boundary) with [Kol07, Remark 67]; the normal-crossings clause is the argument of GoingUp/Theorem84.lean from the start F instead of the empty family: the boundary E_i^X of the push-forward is the reduced ideal sheaf of the family F_i^X from the start F, which has simple normal crossings with the strict transform H_i properly (the invariant starts from the proper hypothesis F.HasSncWithProper H), its trace on H_i is through e_i : T_i ≃ H_i the boundary of T started with E|_H, and clause (3′) of T lifts stage by stage.

Going down, (2) ⇒ (1): for H in MC(I), i.e. I_H ⊆ D^{m−1}(I) (the static form of maximal contact, [Kol07, Theorem 80]), a sequence of order m for (I, m) with the boundary E has its centres in the strict transforms of H and restricts to a sequence of order ≥ m for (I|_H, m) with the boundary E|_H: the order clause by le_ordAlong_restrictSubmanifold, the normal-crossings clause because the boundary of B|_H is the reduced ideal sheaf of the trace of F_i on H_i and Z_i ∩ H_i has simple normal crossings with that trace (hasSncWith_traceFamily).

• hasSncWithProper_totalTransformSeqFrom_strictTransformSeq_of_forall_lt: the proper invariant from a start family F (hasSncWithProper_totalTransformSeq_strictTransformSeq is the empty start).
• pushforward_hasOnlyNormalCrossingsWith_center_from_of_forall_lt, …_from: clause (3′) of the push-forward from the start F.
• pushforward_isOfOrderGe_of_isOfOrderGe_traceFamily, pushforward_isOfOrder_of_isOfOrderGe_traceFamily: going up, in the ≥ m form and as printed.
• restrictSubmanifold_isOfOrderGe_traceFamily_of_isOfOrderGe, restrictSubmanifold_isOfOrderGe_of_isOfOrder_of_le_iteratedDeriv: going down, for centres in the strict transforms of H and from a hypersurface in MC(I) ([Kol07, Theorem 80]).

Corollary 85 is the dimension reduction of the order-reduction algorithm: order reduction on X is carried out on a hypersurface of maximal contact and pushed forward.

theorem AnalyticManifold.FiniteSuccession.hasSncWithProper_totalTransformSeqFrom_strictTransformSeq_of_forall_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFH : Manifold.HypersurfaceFamily.HasSncWithProper ψ F H s) (i : Fin (S.length + 1)) (h3 : ∀ (i' : Fin S.length), ↑i' < ↑i → (S.boundarySeq F.idealSheaf i'.castSucc).HasOnlyNormalCrossingsWith (S.center i')) : Manifold.HypersurfaceFamily.HasSncWithProper ψ (S.totalTransformSeqFrom F i) (S.strictTransformSeq H i) s

The proper invariant from a start family (the restriction of sequences, [Kol07, 30.2]): along a sequence with centres Z_i ⊆ H_i, starting from a simple normal crossing family F having simple normal crossings with H properly, the strict transform H_i has simple normal crossings with the boundary family F_i from the start F, properly, at every stage i at which clause (3′) for the boundary red F holds at the stages < i. The base is the proper hypothesis on F (a plain HasSncWith base would not start the induction: a component of F could contain H near a point); the step is the transport of the proper invariant by the blowing-up along Z_i ⊆ H_i (hasSncWithProper_totalTransform).

theorem AnalyticManifold.FiniteSuccession.pushforward_hasOnlyNormalCrossingsWith_center_from_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} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) {J : hS.toAnalyticManifold.IdealSheaf} {m : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S s) (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.idealSheaf i'.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i')) : ((pushforward hS T).boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i)

The stage step with a boundary ([Kol07, 30.2–30.3]): if the push-forward Π = j_* T of a sequence T of order ≥ m with the boundary E|_S = red (F|_S) satisfies clause (3′) for the boundary E = red F at every stage < i, it satisfies it at stage i. This is the step of GoingUp/Theorem84.lean from the start F: clause (3′) of T at stage i becomes clause (3′) of Π|_S through e_i⁻¹ (boundarySeq_pushforwardStageIso with the start E|_S, center_pushforwardStageIso), the boundary of Π|_S is the reduced ideal sheaf of the trace of F_i^X on S_i (boundarySeq_restrictSubmanifold_eq_idealSheaf_traceFamilyFrom, with the proper invariant from F), and the lifting hasOnlyNormalCrossingsWith_idealSheaf_of_traceFamily gives clause (3′) of Π.

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

Clause (3′) of the push-forward with the boundary E = red F ([Kol07, 30.2–30.3]), for T of order ≥ m with the boundary E|_S. Induction on a bound for the stage with the stage step.

theorem AnalyticManifold.FiniteSuccession.pushforward_isOfOrderGe_of_isOfOrderGe_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (T : hH.toAnalyticManifold.FiniteSuccession) {I : M.IdealSheaf} {m : ℕ} {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) (hFH : Manifold.HypersurfaceFamily.HasSncWithProper ψ F H 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ I) m (hH.traceFamily F).idealSheaf) : (pushforward hH T).IsOfOrderGe I m F.idealSheaf

Corollary 85 [Kol07, Corollary 85], going up (1) ⇒ (2), the ≥ m form with the boundary: for I D-balanced with ord I ≤ m everywhere and E = red F a simple normal crossing boundary having simple normal crossings with the hypersurface H properly, the push-forward of a sequence of order ≥ m for (I|_H, m) with the boundary E|_H is of order ≥ m for (I, m) with the boundary E. Clause (4′) is Kollár's induction [Kol07, 90] (which does not look at the boundary), clause (3′) is pushforward_hasOnlyNormalCrossingsWith_center_from ([Kol07, 30.2] and the lifting of simple normal crossings).

theorem AnalyticManifold.FiniteSuccession.pushforward_isOfOrder_of_isOfOrderGe_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (T : hH.toAnalyticManifold.FiniteSuccession) {I : M.IdealSheaf} {m : ℕ} {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) (hFH : Manifold.HypersurfaceFamily.HasSncWithProper ψ F H 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ I) m (hH.traceFamily F).idealSheaf) : (pushforward hH T).IsOfOrder I F.idealSheaf m

Corollary 85 [Kol07, Corollary 85], going up (1) ⇒ (2) as printed: the push-forward is of order exactly m with the boundary E ([Kol07, Remark 67], isOfOrder_of_isOfOrderGe_of_ord_le). The maximal-contact and component hypotheses of the printed statement are not needed for this direction and are omitted.

theorem AnalyticManifold.FiniteSuccession.restrictSubmanifold_isOfOrderGe_traceFamily_of_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (B : M.FiniteSuccession) {I : M.IdealSheaf} {m : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFH : Manifold.HypersurfaceFamily.HasSncWithProper ψ F H s) (hge : B.IsOfOrderGe I m F.idealSheaf) (hc : B.CentersIn H) : (B.restrictSubmanifold hH hc).IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ I) m (hH.traceFamily F).idealSheaf

Going down with a boundary ([Kol07, Corollary 85] (2) ⇒ (1), with the restriction of sequences [Kol07, 30.2]): for a sequence B of order ≥ m for (I, m) with the boundary E = red F whose centres lie in the strict transforms of H (F a simple normal crossing family having simple normal crossings with H properly), the restriction B|_H is of order ≥ m for (I|_H, m) with the boundary E|_H. Clause (4′) is le_ordAlong_restrictSubmanifold; clause (3′) is the form from the start F of boundarySeq_restrictSubmanifold_hasOnlyNormalCrossingsWith_center: the boundary of B|_H is the reduced ideal sheaf of the trace of F_i on H_i (boundarySeq_restrictSubmanifold_eq_idealSheaf_traceFamilyFrom), and Z_i ∩ H_i has simple normal crossings with that trace (hasSncWith_traceFamily, from clause (3′) of B and the proper invariant from F).

theorem AnalyticManifold.FiniteSuccession.restrictSubmanifold_isOfOrderGe_of_isOfOrder_of_le_iteratedDeriv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) {I : M.IdealSheaf} {m : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hm : 1 ≤ m) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFH : Manifold.HypersurfaceFamily.HasSncWithProper ψ F H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (B : M.FiniteSuccession) (hB : B.IsOfOrder I F.idealSheaf m) : ∃ (hc : B.CentersIn H), (B.restrictSubmanifold hH hc).IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hH.inclusionMap ⋯ I) m (hH.traceFamily F).idealSheaf

Going down in the static form of [Kol07, Theorem 80 (1)] (IsOfOrder.centersIn_of_idealSheaf_le_iteratedDeriv): with I_H ⊆ D^{m−1}(I) in place of maximal contact, the centres lie in the strict transforms of H and the restriction is of order ≥ m with the boundary E|_H.